{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{- |
Module      :  ./CASL/ColimSign.hs
Description :  CASL signatures colimits
Copyright   :  (c) Mihai Codescu, and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  mcodescu@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable

CASL signature colimits, computed component-wise.
Supposed to be working for CASL extensions as well.
based on
<http://www.informatik.uni-bremen.de/~till/papers/colimits.ps>

-}

module CASL.ColimSign (signColimit, extCASLColimit) where

import CASL.Sign
import CASL.Morphism
import CASL.Overload
import CASL.AS_Basic_CASL

import Common.Id
import Common.SetColimit
import Common.Utils (number, nubOrd)
import Common.Lib.Graph
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet

import Data.Graph.Inductive.Graph as Graph
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List

import Logic.Logic

extCASLColimit :: Gr () (Int, ()) ->
                  Map.Map Int CASLMor ->
                  ((), Map.Map Int ())
extCASLColimit :: Gr () (Int, ()) -> Map Int CASLMor -> ((), Map Int ())
extCASLColimit graph :: Gr () (Int, ())
graph _ = ((), [(Int, ())] -> Map Int ()
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, ())] -> Map Int ()) -> [(Int, ())] -> Map Int ()
forall a b. (a -> b) -> a -> b
$ [Int] -> [()] -> [(Int, ())]
forall a b. [a] -> [b] -> [(a, b)]
zip (Gr () (Int, ()) -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Int]
nodes Gr () (Int, ())
graph) (() -> [()]
forall a. a -> [a]
repeat ()))

-- central function for computing CASL signature colimits
signColimit :: (Category (Sign f e) (Morphism f e m)) =>
               Gr (Sign f e) (Int, Morphism f e m) ->
               ( Gr e (Int, m) ->
                 Map.Map Int (Morphism f e m)
                 -> (e, Map.Map Int m)
               )
               ->
               (Sign f e, Map.Map Int (Morphism f e m))
signColimit :: Gr (Sign f e) (Int, Morphism f e m)
-> (Gr e (Int, m) -> Map Int (Morphism f e m) -> (e, Map Int m))
-> (Sign f e, Map Int (Morphism f e m))
signColimit graph :: Gr (Sign f e) (Int, Morphism f e m)
graph extColimit :: Gr e (Int, m) -> Map Int (Morphism f e m) -> (e, Map Int m)
extColimit =
 case Gr (Sign f e) (Int, Morphism f e m) -> [LNode (Sign f e)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr (Sign f e) (Int, Morphism f e m)
graph of
  [] -> [Char] -> (Sign f e, Map Int (Morphism f e m))
forall a. HasCallStack => [Char] -> a
error "empty graph"
  (n :: Int
n, sig :: Sign f e
sig) : [] -> (Sign f e
sig, [(Int, Morphism f e m)] -> Map Int (Morphism f e m)
forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList [(Int
n, Sign f e -> Morphism f e m
forall object morphism.
Category object morphism =>
object -> morphism
ide Sign f e
sig)])
  _ -> let
   getSortMap :: (a, Morphism f e m) -> (a, Sort_map)
getSortMap (x :: a
x, phi :: Morphism f e m
phi) = (a
x, Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
phi)
   sortGraph :: Gr (Set SORT) (Int, Sort_map)
sortGraph = ((Int, Morphism f e m) -> (Int, Sort_map))
-> Gr (Set SORT) (Int, Morphism f e m)
-> Gr (Set SORT) (Int, Sort_map)
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
emap (Int, Morphism f e m) -> (Int, Sort_map)
forall a f e m. (a, Morphism f e m) -> (a, Sort_map)
getSortMap (Gr (Set SORT) (Int, Morphism f e m)
 -> Gr (Set SORT) (Int, Sort_map))
-> Gr (Set SORT) (Int, Morphism f e m)
-> Gr (Set SORT) (Int, Sort_map)
forall a b. (a -> b) -> a -> b
$ (Sign f e -> Set SORT)
-> Gr (Sign f e) (Int, Morphism f e m)
-> Gr (Set SORT) (Int, Morphism f e m)
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
nmap Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Gr (Sign f e) (Int, Morphism f e m)
graph
   (setSort0 :: Set (SORT, Int)
setSort0, funSort0 :: Map Int (Map SORT (SORT, Int))
funSort0) = Gr (Set SORT) (Int, Sort_map)
-> (Set (SORT, Int), Map Int (Map SORT (SORT, Int)))
forall a.
Ord a =>
Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map a (a, Int)))
computeColimitSet Gr (Set SORT) (Int, Sort_map)
sortGraph
   (setSort :: Set SORT
setSort, funSort :: Map Int Sort_map
funSort) = (Set (SORT, Int), Map Int (Map SORT (SORT, Int)))
-> (Set SORT, Map Int Sort_map)
forall a.
SymbolName a =>
(Set (a, Int), Map Int (Map a (a, Int)))
-> (Set a, Map Int (Map a a))
addIntToSymbols (Set (SORT, Int)
setSort0, Map Int (Map SORT (SORT, Int))
funSort0)
   sigmaSort :: Sign f e
sigmaSort = (e -> Sign f e
forall e f. e -> Sign f e
emptySign (e -> Sign f e) -> e -> Sign f e
forall a b. (a -> b) -> a -> b
$ [Char] -> e
forall a. HasCallStack => [Char] -> a
error "err")
     { sortRel :: Rel SORT
sortRel = Set SORT -> Rel SORT
forall a. Ord a => Set a -> Rel a
Rel.fromKeysSet Set SORT
setSort }
   phiSort :: Map Int (Morphism f e m)
phiSort = [(Int, Morphism f e m)] -> Map Int (Morphism f e m)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    ([(Int, Morphism f e m)] -> Map Int (Morphism f e m))
-> [(Int, Morphism f e m)] -> Map Int (Morphism f e m)
forall a b. (a -> b) -> a -> b
$ (LNode (Sign f e) -> (Int, Morphism f e m))
-> [LNode (Sign f e)] -> [(Int, Morphism f e m)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (node :: Int
node, s :: Sign f e
s) -> (Int
node, (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 ([Char] -> m
forall a. HasCallStack => [Char] -> a
error "err") Sign f e
s Sign f e
forall f e. Sign f e
sigmaSort)
           {sort_map :: Sort_map
sort_map = Sort_map -> Int -> Map Int Sort_map -> Sort_map
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Sort_map
forall a. HasCallStack => [Char] -> a
error "sort_map") Int
node Map Int Sort_map
funSort}))
    ([LNode (Sign f e)] -> [(Int, Morphism f e m)])
-> [LNode (Sign f e)] -> [(Int, Morphism f e m)]
forall a b. (a -> b) -> a -> b
$ Gr (Sign f e) (Int, Morphism f e m) -> [LNode (Sign f e)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr (Sign f e) (Int, Morphism f e m)
graph
   relS :: Rel SORT
relS = Gr (Sign f e) (Int, Morphism f e m) -> Map Int Sort_map -> Rel SORT
forall f e m.
Gr (Sign f e) (Int, Morphism f e m) -> Map Int Sort_map -> Rel SORT
computeSubsorts Gr (Sign f e) (Int, Morphism f e m)
graph Map Int Sort_map
funSort
   sigmaRel :: Sign f e
sigmaRel = Sign f e
forall f e. Sign f e
sigmaSort {sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union Rel SORT
relS (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign Any Any -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign Any Any
forall f e. Sign f e
sigmaSort }
   phiRel :: Map Int (Morphism f e m)
phiRel = (Morphism f e m -> Morphism f e m)
-> Map Int (Morphism f e m) -> Map Int (Morphism f e m)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ phi :: Morphism f e m
phi -> Morphism f e m
phi {mtarget :: Sign f e
mtarget = Sign f e
forall f e. Sign f e
sigmaRel}) Map Int (Morphism f e m)
forall m. Map Int (Morphism f e m)
phiSort
   (sigmaOp :: Sign f e
sigmaOp, phiOp :: Map Int (Morphism f e m)
phiOp) = Gr (Sign f e) (Int, Morphism f e m)
-> Sign f e
-> Map Int (Morphism f e m)
-> (Sign f e, Map Int (Morphism f e m))
forall f e m.
Gr (Sign f e) (Int, Morphism f e m)
-> Sign f e
-> Map Int (Morphism f e m)
-> (Sign f e, Map Int (Morphism f e m))
computeColimitOp Gr (Sign f e) (Int, Morphism f e m)
graph Sign f e
forall f e. Sign f e
sigmaRel Map Int (Morphism f e m)
forall m. Map Int (Morphism f e m)
phiRel
   (sigmaPred :: Sign f e
sigmaPred, phiPred :: Map Int (Morphism f e m)
phiPred) = Gr (Sign f e) (Int, Morphism f e m)
-> Sign f e
-> Map Int (Morphism f e m)
-> (Sign f e, Map Int (Morphism f e m))
forall f e m.
Gr (Sign f e) (Int, Morphism f e m)
-> Sign f e
-> Map Int (Morphism f e m)
-> (Sign f e, Map Int (Morphism f e m))
computeColimitPred Gr (Sign f e) (Int, Morphism f e m)
graph Sign f e
sigmaOp Map Int (Morphism f e m)
phiOp
   (sigAssoc :: Sign f e
sigAssoc, phiAssoc :: Map Int (Morphism f e m)
phiAssoc) = Gr (Sign f e) (Int, Morphism f e m)
-> Sign f e
-> Map Int (Morphism f e m)
-> (Sign f e, Map Int (Morphism f e m))
forall f e m.
Gr (Sign f e) (Int, Morphism f e m)
-> Sign f e
-> Map Int (Morphism f e m)
-> (Sign f e, Map Int (Morphism f e m))
colimitAssoc Gr (Sign f e) (Int, Morphism f e m)
graph Sign f e
sigmaPred Map Int (Morphism f e m)
phiPred
   extGraph :: Gr e (Int, m)
extGraph = ((Int, Morphism f e m) -> (Int, m))
-> Gr e (Int, Morphism f e m) -> Gr e (Int, m)
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
emap (\ (i :: Int
i, phi :: Morphism f e m
phi) -> (Int
i, Morphism f e m -> m
forall f e m. Morphism f e m -> m
extended_map Morphism f e m
phi)) (Gr e (Int, Morphism f e m) -> Gr e (Int, m))
-> Gr e (Int, Morphism f e m) -> Gr e (Int, m)
forall a b. (a -> b) -> a -> b
$
              (Sign f e -> e)
-> Gr (Sign f e) (Int, Morphism f e m)
-> Gr e (Int, Morphism f e m)
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
nmap Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Gr (Sign f e) (Int, Morphism f e m)
graph
   (extInfo :: e
extInfo, extMaps :: Map Int m
extMaps) = Gr e (Int, m) -> Map Int (Morphism f e m) -> (e, Map Int m)
extColimit Gr e (Int, m)
extGraph Map Int (Morphism f e m)
phiAssoc
   sigmaExt :: Sign f e
sigmaExt = Sign f e
sigAssoc {extendedInfo :: e
extendedInfo = e
extInfo}
   phiExt :: Map Int (Morphism f e m)
phiExt = (Int -> Morphism f e m -> Morphism f e m)
-> Map Int (Morphism f e m) -> Map Int (Morphism f e m)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey
     (\ node :: Int
node phi :: Morphism f e m
phi -> Morphism f e m
phi {mtarget :: Sign f e
mtarget = Sign f e
sigmaExt,
                       sort_map :: Sort_map
sort_map = (SORT -> SORT -> Bool) -> Sort_map -> Sort_map
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Sort_map -> Sort_map) -> Sort_map -> Sort_map
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
phi,
                       extended_map :: m
extended_map = m -> Int -> Map Int m -> m
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> m
forall a. HasCallStack => [Char] -> a
error "ext_map")
                                         Int
node Map Int m
extMaps})
     Map Int (Morphism f e m)
phiAssoc
   in (Sign f e
sigmaExt, Map Int (Morphism f e m)
phiExt)

{- computing subsorts in the colimit
the subsort relation in the colimit is the transitive closure
of the subsort relations in the diagram
mapped along the structural morphisms of the colimit -}
computeSubsorts :: Gr (Sign f e) (Int, Morphism f e m) ->
    Map.Map Node (EndoMap Id) -> Rel.Rel Id
computeSubsorts :: Gr (Sign f e) (Int, Morphism f e m) -> Map Int Sort_map -> Rel SORT
computeSubsorts graph :: Gr (Sign f e) (Int, Morphism f e m)
graph funSort :: Map Int Sort_map
funSort = let
  getPhiSort :: (a, Morphism f e m) -> (a, Sort_map)
getPhiSort (x :: a
x, phi :: Morphism f e m
phi) = (a
x, Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
phi)
  graph1 :: Gr (Set SORT) (Int, Sort_map)
graph1 = (Sign f e -> Set SORT)
-> Gr (Sign f e) (Int, Sort_map) -> Gr (Set SORT) (Int, Sort_map)
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
nmap Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet (Gr (Sign f e) (Int, Sort_map) -> Gr (Set SORT) (Int, Sort_map))
-> Gr (Sign f e) (Int, Sort_map) -> Gr (Set SORT) (Int, Sort_map)
forall a b. (a -> b) -> a -> b
$ ((Int, Morphism f e m) -> (Int, Sort_map))
-> Gr (Sign f e) (Int, Morphism f e m)
-> Gr (Sign f e) (Int, Sort_map)
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
emap (Int, Morphism f e m) -> (Int, Sort_map)
forall a f e m. (a, Morphism f e m) -> (a, Sort_map)
getPhiSort Gr (Sign f e) (Int, Morphism f e m)
graph
  rels :: Map Int (Rel SORT)
rels = [(Int, Rel SORT)] -> Map Int (Rel SORT)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Rel SORT)] -> Map Int (Rel SORT))
-> [(Int, Rel SORT)] -> Map Int (Rel SORT)
forall a b. (a -> b) -> a -> b
$ ((Int, Sign f e) -> (Int, Rel SORT))
-> [(Int, Sign f e)] -> [(Int, Rel SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (node :: Int
node, sign :: Sign f e
sign) -> (Int
node, Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sign)) ([(Int, Sign f e)] -> [(Int, Rel SORT)])
-> [(Int, Sign f e)] -> [(Int, Rel SORT)]
forall a b. (a -> b) -> a -> b
$
         Gr (Sign f e) (Int, Morphism f e m) -> [(Int, Sign f e)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr (Sign f e) (Int, Morphism f e m)
graph
 in [Int]
-> Gr (Set SORT) (Int, Sort_map)
-> Map Int (Rel SORT)
-> Map Int Sort_map
-> Rel SORT
-> Rel SORT
subsorts (Gr (Set SORT) (Int, Sort_map) -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Int]
nodes Gr (Set SORT) (Int, Sort_map)
graph1) Gr (Set SORT) (Int, Sort_map)
graph1 Map Int (Rel SORT)
rels Map Int Sort_map
funSort Rel SORT
forall a. Rel a
Rel.empty

{- rels is a function assigning to each node
the subsort relation of its label's elements -}

subsorts :: [Node] -> Gr (Set.Set SORT) (Int, Sort_map) ->
   Map.Map Node (Rel.Rel SORT) -> Map.Map Node (EndoMap Id) -> Rel.Rel SORT ->
   Rel.Rel SORT
subsorts :: [Int]
-> Gr (Set SORT) (Int, Sort_map)
-> Map Int (Rel SORT)
-> Map Int Sort_map
-> Rel SORT
-> Rel SORT
subsorts listNode :: [Int]
listNode graph :: Gr (Set SORT) (Int, Sort_map)
graph rels :: Map Int (Rel SORT)
rels colimF :: Map Int Sort_map
colimF rel :: Rel SORT
rel =
 case [Int]
listNode of
  [] -> Rel SORT
rel
  x :: Int
x : xs :: [Int]
xs -> case Gr (Set SORT) (Int, Sort_map) -> Int -> Maybe (Set SORT)
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Maybe a
lab Gr (Set SORT) (Int, Sort_map)
graph Int
x of
    Nothing -> [Int]
-> Gr (Set SORT) (Int, Sort_map)
-> Map Int (Rel SORT)
-> Map Int Sort_map
-> Rel SORT
-> Rel SORT
subsorts [Int]
xs Gr (Set SORT) (Int, Sort_map)
graph Map Int (Rel SORT)
rels Map Int Sort_map
colimF Rel SORT
rel
    Just set :: Set SORT
set -> let
                  f :: Sort_map
f = Sort_map -> Int -> Map Int Sort_map -> Sort_map
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Sort_map
forall a. HasCallStack => [Char] -> a
error "subsorts") Int
x Map Int Sort_map
colimF
                  genRel :: Rel SORT
genRel = [(SORT, SORT)] -> Rel SORT
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList [ (
                             SORT -> SORT -> Sort_map -> SORT
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> SORT
forall a. HasCallStack => [Char] -> a
error "f(m)") SORT
m Sort_map
f,
                             SORT -> SORT -> Sort_map -> SORT
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> SORT
forall a. HasCallStack => [Char] -> a
error "f(n)") SORT
n Sort_map
f
                                           )
                            | SORT
m <- Set SORT -> [SORT]
forall a. Set a -> [a]
Set.elems Set SORT
set, SORT
n <- Set SORT -> [SORT]
forall a. Set a -> [a]
Set.elems Set SORT
set,
                              SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.member SORT
m SORT
n (Rel SORT -> Int -> Map Int (Rel SORT) -> Rel SORT
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                               ([Char] -> Rel SORT
forall a. HasCallStack => [Char] -> a
error "rels(x)") Int
x Map Int (Rel SORT)
rels) ]
                in [Int]
-> Gr (Set SORT) (Int, Sort_map)
-> Map Int (Rel SORT)
-> Map Int Sort_map
-> Rel SORT
-> Rel SORT
subsorts [Int]
xs Gr (Set SORT) (Int, Sort_map)
graph Map Int (Rel SORT)
rels Map Int Sort_map
colimF (Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$
                   Rel SORT -> Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union Rel SORT
rel Rel SORT
genRel)

-- CASL signatures colimit on operation symbols

{- algorithm description:
1. project the graph on operation symbols
i.e. set of (Id, OpType)s in nodes and corresponding maps on edges
2. compute colimit in Set of the graph => a set of ((Id, OpType), Node)
3. build the overloading relation in colimit
two symbols are overloaded in the colimit
if there is some node and two opsymbols there
that are mapped in them and are overloaded
collect the names entering each symbol (try to keep names)
collect information about totality: a symbol must be total in the colimit
if we have a total symbol in the graph which is mapped to it
4. assign names to each partition, in order of size
(i.e. the equivalence class with most symbols
will be prefered to keep name):
if there is available a name of a symbol entering the class,
then assign that name to the class, otherwise generate a name
also the morphisms have to be built -}

computeColimitOp :: Gr (Sign f e) (Int, Morphism f e m) ->
                    Sign f e -> Map.Map Node (Morphism f e m) ->
                    (Sign f e, Map.Map Node (Morphism f e m))
computeColimitOp :: Gr (Sign f e) (Int, Morphism f e m)
-> Sign f e
-> Map Int (Morphism f e m)
-> (Sign f e, Map Int (Morphism f e m))
computeColimitOp graph :: Gr (Sign f e) (Int, Morphism f e m)
graph sigmaRel :: Sign f e
sigmaRel phiSRel :: Map Int (Morphism f e m)
phiSRel = let
 graph' :: Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph' = Gr (Sign f e) (Int, Morphism f e m)
-> Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
forall f e m.
Gr (Sign f e) (Int, Morphism f e m)
-> Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
buildOpGraph Gr (Sign f e) (Int, Morphism f e m)
graph
 (colim :: Set ((SORT, OpType), Int)
colim, morMap' :: Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap') = Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> (Set ((SORT, OpType), Int),
    Map Int (Map (SORT, OpType) ((SORT, OpType), Int)))
forall a.
Ord a =>
Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map a (a, Int)))
computeColimitSet Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph'
 (ovrl :: Rel ((SORT, OpType), Int)
ovrl, names :: Map ((SORT, OpType), Int) (Map SORT Int)
names, totalOps :: Map ((SORT, OpType), Int) Bool
totalOps) = Gr (Sign f e) (Int, Morphism f e m)
-> Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Set ((SORT, OpType), Int)
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> (Rel ((SORT, OpType), Int),
    Map ((SORT, OpType), Int) (Map SORT Int),
    Map ((SORT, OpType), Int) Bool)
forall f e m.
Gr (Sign f e) (Int, Morphism f e m)
-> Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Set ((SORT, OpType), Int)
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> (Rel ((SORT, OpType), Int),
    Map ((SORT, OpType), Int) (Map SORT Int),
    Map ((SORT, OpType), Int) Bool)
buildColimOvrl Gr (Sign f e) (Int, Morphism f e m)
graph Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph' Set ((SORT, OpType), Int)
colim Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap'
 (colim1 :: OpMap
colim1, morMap1 :: Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap1) = Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Map Int (Morphism f e m)
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> Rel ((SORT, OpType), Int)
-> Map ((SORT, OpType), Int) Bool
-> (OpMap, Map Int (Map (SORT, OpType) ((SORT, OpType), Int)))
forall f e m.
Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Map Int (Morphism f e m)
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> Rel ((SORT, OpType), Int)
-> Map ((SORT, OpType), Int) Bool
-> (OpMap, Map Int (Map (SORT, OpType) ((SORT, OpType), Int)))
nameSymbols Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph' Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap' Map Int (Morphism f e m)
phiSRel Map ((SORT, OpType), Int) (Map SORT Int)
names Rel ((SORT, OpType), Int)
ovrl Map ((SORT, OpType), Int) Bool
totalOps
 morMap2 :: Map Int (Map (SORT, OpType) (SORT, OpKind))
morMap2 = (Map (SORT, OpType) ((SORT, OpType), Int)
 -> Map (SORT, OpType) (SORT, OpKind))
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Map Int (Map (SORT, OpType) (SORT, OpKind))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((((SORT, OpType), Int) -> (SORT, OpKind))
-> Map (SORT, OpType) ((SORT, OpType), Int)
-> Map (SORT, OpType) (SORT, OpKind)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ ((i :: SORT
i, o :: OpType
o), _) -> (SORT
i, OpType -> OpKind
opKind OpType
o))) Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap1
 morMap3 :: Map Int (Map (SORT, OpType) (SORT, OpKind))
morMap3 = (Map (SORT, OpType) (SORT, OpKind)
 -> Map (SORT, OpType) (SORT, OpKind))
-> Map Int (Map (SORT, OpType) (SORT, OpKind))
-> Map Int (Map (SORT, OpType) (SORT, OpKind))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ([((SORT, OpType), (SORT, OpKind))]
-> Map (SORT, OpType) (SORT, OpKind)
forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList ([((SORT, OpType), (SORT, OpKind))]
 -> Map (SORT, OpType) (SORT, OpKind))
-> (Map (SORT, OpType) (SORT, OpKind)
    -> [((SORT, OpType), (SORT, OpKind))])
-> Map (SORT, OpType) (SORT, OpKind)
-> Map (SORT, OpType) (SORT, OpKind)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((SORT, OpType), (SORT, OpKind))
 -> ((SORT, OpType), (SORT, OpKind)))
-> [((SORT, OpType), (SORT, OpKind))]
-> [((SORT, OpType), (SORT, OpKind))]
forall a b. (a -> b) -> [a] -> [b]
map
            (\ ((i :: SORT
i, o :: OpType
o), y :: (SORT, OpKind)
y) -> ((SORT
i, OpType -> OpType
mkPartial OpType
o), (SORT, OpKind)
y)) ([((SORT, OpType), (SORT, OpKind))]
 -> [((SORT, OpType), (SORT, OpKind))])
-> (Map (SORT, OpType) (SORT, OpKind)
    -> [((SORT, OpType), (SORT, OpKind))])
-> Map (SORT, OpType) (SORT, OpKind)
-> [((SORT, OpType), (SORT, OpKind))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (SORT, OpType) (SORT, OpKind)
-> [((SORT, OpType), (SORT, OpKind))]
forall k a. Map k a -> [(k, a)]
Map.toList) Map Int (Map (SORT, OpType) (SORT, OpKind))
morMap2
 sigmaOps :: Sign f e
sigmaOps = Sign f e
sigmaRel {opMap :: OpMap
opMap = OpMap
colim1}
 phiOps :: Map Int (Morphism f e m)
phiOps = (Int -> Morphism f e m -> Morphism f e m)
-> Map Int (Morphism f e m) -> Map Int (Morphism f e m)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey
          (\ n :: Int
n phi :: Morphism f e m
phi -> Morphism f e m
phi {op_map :: Map (SORT, OpType) (SORT, OpKind)
op_map =
                         Map (SORT, OpType) (SORT, OpKind)
-> Int
-> Map Int (Map (SORT, OpType) (SORT, OpKind))
-> Map (SORT, OpType) (SORT, OpKind)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Map (SORT, OpType) (SORT, OpKind)
forall a. HasCallStack => [Char] -> a
error "op_map") Int
n Map Int (Map (SORT, OpType) (SORT, OpKind))
morMap3})
          Map Int (Morphism f e m)
phiSRel
 in (Sign f e
sigmaOps, Map Int (Morphism f e m)
phiOps)

buildOpGraph :: Gr (Sign f e) (Int, Morphism f e m) ->
                Gr (Set.Set (Id, OpType))
                   (Int, Map.Map (Id, OpType) (Id, OpType))
buildOpGraph :: Gr (Sign f e) (Int, Morphism f e m)
-> Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
buildOpGraph graph :: Gr (Sign f e) (Int, Morphism f e m)
graph = let
  getOps :: Sign f e -> [(SORT, OpType)]
getOps = OpMap -> [(SORT, OpType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (OpMap -> [(SORT, OpType)])
-> (Sign f e -> OpMap) -> Sign f e -> [(SORT, OpType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap
  getOpFun :: Morphism f e m -> Map (SORT, OpType) (SORT, OpType)
getOpFun mor :: Morphism f e m
mor = let
                  ssign :: Sign f e
ssign = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
mor
                  smap :: Sort_map
smap = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
mor
                  omap :: Map (SORT, OpType) (SORT, OpKind)
omap = Morphism f e m -> Map (SORT, OpType) (SORT, OpKind)
forall f e m. Morphism f e m -> Map (SORT, OpType) (SORT, OpKind)
op_map Morphism f e m
mor
                 in (Map (SORT, OpType) (SORT, OpType)
 -> (SORT, OpType) -> Map (SORT, OpType) (SORT, OpType))
-> Map (SORT, OpType) (SORT, OpType)
-> [(SORT, OpType)]
-> Map (SORT, OpType) (SORT, OpType)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ f :: Map (SORT, OpType) (SORT, OpType)
f x :: (SORT, OpType)
x -> let y :: (SORT, OpType)
y = Sort_map
-> Map (SORT, OpType) (SORT, OpKind)
-> (SORT, OpType)
-> (SORT, OpType)
mapOpSym Sort_map
smap Map (SORT, OpType) (SORT, OpKind)
omap (SORT, OpType)
x
                                  in if (SORT, OpType)
x (SORT, OpType) -> (SORT, OpType) -> Bool
forall a. Eq a => a -> a -> Bool
== (SORT, OpType)
y then Map (SORT, OpType) (SORT, OpType)
f else (SORT, OpType)
-> (SORT, OpType)
-> Map (SORT, OpType) (SORT, OpType)
-> Map (SORT, OpType) (SORT, OpType)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT, OpType)
x (SORT, OpType)
y Map (SORT, OpType) (SORT, OpType)
f)
                  Map (SORT, OpType) (SORT, OpType)
forall k a. Map k a
Map.empty ([(SORT, OpType)] -> Map (SORT, OpType) (SORT, OpType))
-> [(SORT, OpType)] -> Map (SORT, OpType) (SORT, OpType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> [(SORT, OpType)]
forall f e. Sign f e -> [(SORT, OpType)]
getOps Sign f e
ssign
 in (Sign f e -> Set (SORT, OpType))
-> Gr (Sign f e) (Int, Map (SORT, OpType) (SORT, OpType))
-> Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
nmap ([(SORT, OpType)] -> Set (SORT, OpType)
forall a. Ord a => [a] -> Set a
Set.fromList ([(SORT, OpType)] -> Set (SORT, OpType))
-> (Sign f e -> [(SORT, OpType)]) -> Sign f e -> Set (SORT, OpType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> [(SORT, OpType)]
forall f e. Sign f e -> [(SORT, OpType)]
getOps) (Gr (Sign f e) (Int, Map (SORT, OpType) (SORT, OpType))
 -> Gr
      (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType)))
-> Gr (Sign f e) (Int, Map (SORT, OpType) (SORT, OpType))
-> Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
forall a b. (a -> b) -> a -> b
$ ((Int, Morphism f e m) -> (Int, Map (SORT, OpType) (SORT, OpType)))
-> Gr (Sign f e) (Int, Morphism f e m)
-> Gr (Sign f e) (Int, Map (SORT, OpType) (SORT, OpType))
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
emap (\ (i :: Int
i, m :: Morphism f e m
m) -> (Int
i, Morphism f e m -> Map (SORT, OpType) (SORT, OpType)
forall f e m. Morphism f e m -> Map (SORT, OpType) (SORT, OpType)
getOpFun Morphism f e m
m)) Gr (Sign f e) (Int, Morphism f e m)
graph

buildColimOvrl :: Gr (Sign f e) (Int, Morphism f e m) ->
                  Gr (Set.Set (Id, OpType)) (Int, EndoMap (Id, OpType)) ->
                  Set.Set ((Id, OpType), Int) ->
                  Map.Map Int (Map.Map (Id, OpType) ((Id, OpType), Int)) ->
                  (Rel.Rel ((Id, OpType), Int),
                   Map.Map ((Id, OpType), Int)
                           (Map.Map Id Int),
                   Map.Map ((Id, OpType), Int) Bool)
buildColimOvrl :: Gr (Sign f e) (Int, Morphism f e m)
-> Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Set ((SORT, OpType), Int)
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> (Rel ((SORT, OpType), Int),
    Map ((SORT, OpType), Int) (Map SORT Int),
    Map ((SORT, OpType), Int) Bool)
buildColimOvrl graph :: Gr (Sign f e) (Int, Morphism f e m)
graph graph' :: Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph' colim :: Set ((SORT, OpType), Int)
colim morMap :: Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap = let
   (ovrl :: Rel a
ovrl, names :: Map ((SORT, OpType), Int) (Map k a)
names) = (Rel a
forall a. Rel a
Rel.empty, [(((SORT, OpType), Int), Map k a)]
-> Map ((SORT, OpType), Int) (Map k a)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(((SORT, OpType), Int), Map k a)]
 -> Map ((SORT, OpType), Int) (Map k a))
-> [(((SORT, OpType), Int), Map k a)]
-> Map ((SORT, OpType), Int) (Map k a)
forall a b. (a -> b) -> a -> b
$ [((SORT, OpType), Int)]
-> [Map k a] -> [(((SORT, OpType), Int), Map k a)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Set ((SORT, OpType), Int) -> [((SORT, OpType), Int)]
forall a. Set a -> [a]
Set.toList Set ((SORT, OpType), Int)
colim) ([Map k a] -> [(((SORT, OpType), Int), Map k a)])
-> [Map k a] -> [(((SORT, OpType), Int), Map k a)]
forall a b. (a -> b) -> a -> b
$
                                                  Map k a -> [Map k a]
forall a. a -> [a]
repeat Map k a
forall k a. Map k a
Map.empty )
   (ovrl' :: Rel ((SORT, OpType), Int)
ovrl', names' :: Map ((SORT, OpType), Int) (Map SORT Int)
names', totalF' :: Map ((SORT, OpType), Int) Bool
totalF') = Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Set ((SORT, OpType), Int)
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Rel ((SORT, OpType), Int)
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> Map ((SORT, OpType), Int) Bool
-> [(Int, Sign f e)]
-> (Rel ((SORT, OpType), Int),
    Map ((SORT, OpType), Int) (Map SORT Int),
    Map ((SORT, OpType), Int) Bool)
forall f e.
Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Set ((SORT, OpType), Int)
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Rel ((SORT, OpType), Int)
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> Map ((SORT, OpType), Int) Bool
-> [(Int, Sign f e)]
-> (Rel ((SORT, OpType), Int),
    Map ((SORT, OpType), Int) (Map SORT Int),
    Map ((SORT, OpType), Int) Bool)
buildOvrlAtNode Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph' Set ((SORT, OpType), Int)
colim Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap
                      Rel ((SORT, OpType), Int)
forall a. Rel a
ovrl Map ((SORT, OpType), Int) (Map SORT Int)
forall k a. Map ((SORT, OpType), Int) (Map k a)
names Map ((SORT, OpType), Int) Bool
forall k a. Map k a
Map.empty ([(Int, Sign f e)]
 -> (Rel ((SORT, OpType), Int),
     Map ((SORT, OpType), Int) (Map SORT Int),
     Map ((SORT, OpType), Int) Bool))
-> [(Int, Sign f e)]
-> (Rel ((SORT, OpType), Int),
    Map ((SORT, OpType), Int) (Map SORT Int),
    Map ((SORT, OpType), Int) Bool)
forall a b. (a -> b) -> a -> b
$ Gr (Sign f e) (Int, Morphism f e m) -> [(Int, Sign f e)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr (Sign f e) (Int, Morphism f e m)
graph
  in (Rel ((SORT, OpType), Int) -> Rel ((SORT, OpType), Int)
forall a. Ord a => Rel a -> Rel a
Rel.transClosure Rel ((SORT, OpType), Int)
ovrl', Map ((SORT, OpType), Int) (Map SORT Int)
names', Map ((SORT, OpType), Int) Bool
totalF')

buildOvrlAtNode :: Gr (Set.Set (Id, OpType)) (Int, EndoMap (Id, OpType)) ->
                   Set.Set ((Id, OpType), Int) ->
                   Map.Map Int (Map.Map (Id, OpType) ((Id, OpType), Int)) ->
                   Rel.Rel ((Id, OpType), Int) ->
                   Map.Map ((Id, OpType), Int) (Map.Map Id Int) ->
                   Map.Map ((Id, OpType), Int) Bool ->
                   [(Int, Sign f e)] ->
                   (Rel.Rel ((Id, OpType), Int),
                   Map.Map ((Id, OpType), Int) (Map.Map Id Int),
                   Map.Map ((Id, OpType), Int) Bool )
buildOvrlAtNode :: Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Set ((SORT, OpType), Int)
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Rel ((SORT, OpType), Int)
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> Map ((SORT, OpType), Int) Bool
-> [(Int, Sign f e)]
-> (Rel ((SORT, OpType), Int),
    Map ((SORT, OpType), Int) (Map SORT Int),
    Map ((SORT, OpType), Int) Bool)
buildOvrlAtNode graph' :: Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph' colim :: Set ((SORT, OpType), Int)
colim morMap :: Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap ovrl :: Rel ((SORT, OpType), Int)
ovrl names :: Map ((SORT, OpType), Int) (Map SORT Int)
names totalF :: Map ((SORT, OpType), Int) Bool
totalF nodeList :: [(Int, Sign f e)]
nodeList =
 case [(Int, Sign f e)]
nodeList of
   [] -> (Rel ((SORT, OpType), Int)
ovrl, Map ((SORT, OpType), Int) (Map SORT Int)
names, Map ((SORT, OpType), Int) Bool
totalF)
   (n :: Int
n, sig :: Sign f e
sig) : lists :: [(Int, Sign f e)]
lists -> let
       Just oSet :: Set (SORT, OpType)
oSet = Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Int -> Maybe (Set (SORT, OpType))
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Maybe a
lab Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph' Int
n
       names' :: Map ((SORT, OpType), Int) (Map SORT Int)
names' = (Map ((SORT, OpType), Int) (Map SORT Int)
 -> (SORT, OpType) -> Map ((SORT, OpType), Int) (Map SORT Int))
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> [(SORT, OpType)]
-> Map ((SORT, OpType), Int) (Map SORT Int)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ g :: Map ((SORT, OpType), Int) (Map SORT Int)
g x :: (SORT, OpType)
x@(idN :: SORT
idN, _) -> let
                                 y :: ((SORT, OpType), Int)
y = ((SORT, OpType), Int)
-> (SORT, OpType)
-> Map (SORT, OpType) ((SORT, OpType), Int)
-> ((SORT, OpType), Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ((SORT, OpType)
x, Int
n) (SORT, OpType)
x (Map (SORT, OpType) ((SORT, OpType), Int) -> ((SORT, OpType), Int))
-> Map (SORT, OpType) ((SORT, OpType), Int)
-> ((SORT, OpType), Int)
forall a b. (a -> b) -> a -> b
$
                                     Map (SORT, OpType) ((SORT, OpType), Int)
-> Int
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Map (SORT, OpType) ((SORT, OpType), Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Map (SORT, OpType) ((SORT, OpType), Int)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Map (SORT, OpType) ((SORT, OpType), Int))
-> [Char] -> Map (SORT, OpType) ((SORT, OpType), Int)
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
                                         Int
n Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap
                                 altF :: Maybe a -> Maybe a
altF v :: Maybe a
v = case Maybe a
v of
                                      Nothing -> a -> Maybe a
forall a. a -> Maybe a
Just 1
                                      Just m :: a
m -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a
m a -> a -> a
forall a. Num a => a -> a -> a
+ 1
                                in (Map SORT Int -> Map SORT Int)
-> ((SORT, OpType), Int)
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> Map ((SORT, OpType), Int) (Map SORT Int)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ((Maybe Int -> Maybe Int) -> SORT -> Map SORT Int -> Map SORT Int
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter Maybe Int -> Maybe Int
forall a. Num a => Maybe a -> Maybe a
altF SORT
idN) ((SORT, OpType), Int)
y Map ((SORT, OpType), Int) (Map SORT Int)
g)
                       Map ((SORT, OpType), Int) (Map SORT Int)
names ([(SORT, OpType)] -> Map ((SORT, OpType), Int) (Map SORT Int))
-> [(SORT, OpType)] -> Map ((SORT, OpType), Int) (Map SORT Int)
forall a b. (a -> b) -> a -> b
$ Set (SORT, OpType) -> [(SORT, OpType)]
forall a. Set a -> [a]
Set.toList Set (SORT, OpType)
oSet
       equivF :: (a, OpType) -> (a, OpType) -> Bool
equivF (id1 :: a
id1, ot1 :: OpType
ot1) (id2 :: a
id2, ot2 :: OpType
ot2) = (a
id1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
id2) Bool -> Bool -> Bool
&& Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF Sign f e
sig OpType
ot1 OpType
ot2
       parts :: [[(SORT, OpType)]]
parts = ((SORT, OpType) -> (SORT, OpType) -> Bool)
-> Set (SORT, OpType) -> [[(SORT, OpType)]]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [[a]]
Rel.leqClasses (SORT, OpType) -> (SORT, OpType) -> Bool
forall a. Eq a => (a, OpType) -> (a, OpType) -> Bool
equivF Set (SORT, OpType)
oSet
       addParts :: Rel ((SORT, OpType), Int)
-> t [(SORT, OpType)]
-> (Rel ((SORT, OpType), Int), Map ((SORT, OpType), Int) Bool)
addParts rel :: Rel ((SORT, OpType), Int)
rel =
         ((Rel ((SORT, OpType), Int), Map ((SORT, OpType), Int) Bool)
 -> [(SORT, OpType)]
 -> (Rel ((SORT, OpType), Int), Map ((SORT, OpType), Int) Bool))
-> (Rel ((SORT, OpType), Int), Map ((SORT, OpType), Int) Bool)
-> t [(SORT, OpType)]
-> (Rel ((SORT, OpType), Int), Map ((SORT, OpType), Int) Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (r :: Rel ((SORT, OpType), Int)
r, f :: Map ((SORT, OpType), Int) Bool
f) l :: [(SORT, OpType)]
l -> let l1 :: [((SORT, OpType), Int)]
l1 = ((SORT, OpType) -> ((SORT, OpType), Int))
-> [(SORT, OpType)] -> [((SORT, OpType), Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: (SORT, OpType)
x -> ((SORT, OpType), Int)
-> (SORT, OpType)
-> Map (SORT, OpType) ((SORT, OpType), Int)
-> ((SORT, OpType), Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ((SORT, OpType)
x, Int
n)
                                              (SORT, OpType)
x (Map (SORT, OpType) ((SORT, OpType), Int) -> ((SORT, OpType), Int))
-> Map (SORT, OpType) ((SORT, OpType), Int)
-> ((SORT, OpType), Int)
forall a b. (a -> b) -> a -> b
$ Map (SORT, OpType) ((SORT, OpType), Int)
-> Int
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Map (SORT, OpType) ((SORT, OpType), Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                                               ([Char] -> Map (SORT, OpType) ((SORT, OpType), Int)
forall a. HasCallStack => [Char] -> a
error "morMap(n)") Int
n Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap) [(SORT, OpType)]
l
                        in case [((SORT, OpType), Int)]
l1 of
                   [] -> [Char]
-> (Rel ((SORT, OpType), Int), Map ((SORT, OpType), Int) Bool)
forall a. HasCallStack => [Char] -> a
error "addParts"
                   x :: ((SORT, OpType), Int)
x : xs :: [((SORT, OpType), Int)]
xs -> let
                             (r' :: Rel ((SORT, OpType), Int)
r', ly :: ((SORT, OpType), Int)
ly) = ((Rel ((SORT, OpType), Int), ((SORT, OpType), Int))
 -> ((SORT, OpType), Int)
 -> (Rel ((SORT, OpType), Int), ((SORT, OpType), Int)))
-> (Rel ((SORT, OpType), Int), ((SORT, OpType), Int))
-> [((SORT, OpType), Int)]
-> (Rel ((SORT, OpType), Int), ((SORT, OpType), Int))
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
                              (\ (rl :: Rel ((SORT, OpType), Int)
rl, lx :: ((SORT, OpType), Int)
lx) y :: ((SORT, OpType), Int)
y -> (((SORT, OpType), Int)
-> ((SORT, OpType), Int)
-> Rel ((SORT, OpType), Int)
-> Rel ((SORT, OpType), Int)
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair ((SORT, OpType), Int)
lx ((SORT, OpType), Int)
y Rel ((SORT, OpType), Int)
rl, ((SORT, OpType), Int)
y))
                              (Rel ((SORT, OpType), Int)
r, ((SORT, OpType), Int)
x) [((SORT, OpType), Int)]
xs
                             f' :: Map ((SORT, OpType), Int) Bool
f' = (Map ((SORT, OpType), Int) Bool
 -> ((SORT, OpType), ((SORT, OpType), Int))
 -> Map ((SORT, OpType), Int) Bool)
-> Map ((SORT, OpType), Int) Bool
-> [((SORT, OpType), ((SORT, OpType), Int))]
-> Map ((SORT, OpType), Int) Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ g :: Map ((SORT, OpType), Int) Bool
g ((_i :: SORT
_i, o :: OpType
o), ((i' :: SORT
i', o' :: OpType
o'), n' :: Int
n')) ->
                                   if OpType -> Bool
isTotal OpType
o then
                                    ((SORT, OpType), Int)
-> Bool
-> Map ((SORT, OpType), Int) Bool
-> Map ((SORT, OpType), Int) Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ((SORT
i', OpType -> OpType
mkPartial OpType
o'), Int
n')
                                               Bool
True Map ((SORT, OpType), Int) Bool
g
                                    else Map ((SORT, OpType), Int) Bool
g ) Map ((SORT, OpType), Int) Bool
f ([((SORT, OpType), ((SORT, OpType), Int))]
 -> Map ((SORT, OpType), Int) Bool)
-> [((SORT, OpType), ((SORT, OpType), Int))]
-> Map ((SORT, OpType), Int) Bool
forall a b. (a -> b) -> a -> b
$ [(SORT, OpType)]
-> [((SORT, OpType), Int)]
-> [((SORT, OpType), ((SORT, OpType), Int))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(SORT, OpType)]
l [((SORT, OpType), Int)]
l1
                            in (((SORT, OpType), Int)
-> ((SORT, OpType), Int)
-> Rel ((SORT, OpType), Int)
-> Rel ((SORT, OpType), Int)
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair ((SORT, OpType), Int)
ly ((SORT, OpType), Int)
x Rel ((SORT, OpType), Int)
r', Map ((SORT, OpType), Int) Bool
f')
                        ) (Rel ((SORT, OpType), Int)
rel, Map ((SORT, OpType), Int) Bool
totalF)
       (ovrl' :: Rel ((SORT, OpType), Int)
ovrl', totalF' :: Map ((SORT, OpType), Int) Bool
totalF') = Rel ((SORT, OpType), Int)
-> [[(SORT, OpType)]]
-> (Rel ((SORT, OpType), Int), Map ((SORT, OpType), Int) Bool)
forall (t :: * -> *).
Foldable t =>
Rel ((SORT, OpType), Int)
-> t [(SORT, OpType)]
-> (Rel ((SORT, OpType), Int), Map ((SORT, OpType), Int) Bool)
addParts Rel ((SORT, OpType), Int)
ovrl [[(SORT, OpType)]]
parts
     in Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Set ((SORT, OpType), Int)
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Rel ((SORT, OpType), Int)
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> Map ((SORT, OpType), Int) Bool
-> [(Int, Sign f e)]
-> (Rel ((SORT, OpType), Int),
    Map ((SORT, OpType), Int) (Map SORT Int),
    Map ((SORT, OpType), Int) Bool)
forall f e.
Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Set ((SORT, OpType), Int)
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Rel ((SORT, OpType), Int)
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> Map ((SORT, OpType), Int) Bool
-> [(Int, Sign f e)]
-> (Rel ((SORT, OpType), Int),
    Map ((SORT, OpType), Int) (Map SORT Int),
    Map ((SORT, OpType), Int) Bool)
buildOvrlAtNode Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph' Set ((SORT, OpType), Int)
colim Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap Rel ((SORT, OpType), Int)
ovrl' Map ((SORT, OpType), Int) (Map SORT Int)
names' Map ((SORT, OpType), Int) Bool
totalF' [(Int, Sign f e)]
lists

assignName :: (Set.Set ((Id, OpType), Int), Int) -> [Id] ->
              Map.Map ((Id, OpType), Int) (Map.Map Id Int) ->
              (Id, [Id])
assignName :: (Set ((SORT, OpType), Int), Int)
-> [SORT]
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> (SORT, [SORT])
assignName (opSet :: Set ((SORT, OpType), Int)
opSet, idx :: Int
idx) givenNames :: [SORT]
givenNames namesFun :: Map ((SORT, OpType), Int) (Map SORT Int)
namesFun =
 let opSetNames :: Map SORT Int
opSetNames = (((SORT, OpType), Int) -> Map SORT Int -> Map SORT Int)
-> Map SORT Int -> Set ((SORT, OpType), Int) -> Map SORT Int
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ x :: ((SORT, OpType), Int)
x f :: Map SORT Int
f -> (Int -> Int -> Int) -> Map SORT Int -> Map SORT Int -> Map SORT Int
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Map SORT Int
f
                              (Map SORT Int
-> ((SORT, OpType), Int)
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> Map SORT Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Map SORT Int
forall a. HasCallStack => [Char] -> a
error "namesFun") ((SORT, OpType), Int)
x
                                Map ((SORT, OpType), Int) (Map SORT Int)
namesFun)) Map SORT Int
forall k a. Map k a
Map.empty Set ((SORT, OpType), Int)
opSet
     availNames :: [SORT]
availNames = (SORT -> Bool) -> [SORT] -> [SORT]
forall a. (a -> Bool) -> [a] -> [a]
filter (SORT -> [SORT] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [SORT]
givenNames) ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$
                  Map SORT Int -> [SORT]
forall k a. Map k a -> [k]
Map.keys Map SORT Int
opSetNames
 in case [SORT]
availNames of
     [] -> let
       -- must generate name with the most frequent name idx and an origin
        sndOrd :: SORT -> SORT -> Ordering
sndOrd x :: SORT
x y :: SORT
y = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
                      (Int -> SORT -> Map SORT Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Int
forall a. HasCallStack => [Char] -> a
error "assignName") SORT
x Map SORT Int
opSetNames)
                      (Int -> SORT -> Map SORT Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Int
forall a. HasCallStack => [Char] -> a
error "assignName") SORT
y Map SORT Int
opSetNames)
        avail' :: [SORT]
avail' = (SORT -> SORT -> Ordering) -> [SORT] -> [SORT]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy SORT -> SORT -> Ordering
sndOrd ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ Map SORT Int -> [SORT]
forall k a. Map k a -> [k]
Map.keys Map SORT Int
opSetNames
        idN :: SORT
idN = [SORT] -> SORT
forall a. [a] -> a
head [SORT]
avail'
       in (SORT -> [Char] -> SORT
appendString SORT
idN ([Char] -> SORT) -> [Char] -> SORT
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
idx, [SORT]
givenNames)
     _ -> {- must take the most frequent available name and give it to the class
          and this name becomes given -}
          let
         sndOrd :: SORT -> SORT -> Ordering
sndOrd x :: SORT
x y :: SORT
y = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
                       (Int -> SORT -> Map SORT Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Int
forall a. HasCallStack => [Char] -> a
error "assignName") SORT
x Map SORT Int
opSetNames)
                       (Int -> SORT -> Map SORT Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Int
forall a. HasCallStack => [Char] -> a
error "assignName") SORT
y Map SORT Int
opSetNames)
         avail' :: [SORT]
avail' = (SORT -> SORT -> Ordering) -> [SORT] -> [SORT]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy SORT -> SORT -> Ordering
sndOrd [SORT]
availNames
         idN :: SORT
idN = [SORT] -> SORT
forall a. [a] -> a
last [SORT]
avail'
        in (SORT
idN, SORT
idN SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: [SORT]
givenNames)

nameSymbols :: Gr (Set.Set (Id, OpType))
                   (Int, Map.Map (Id, OpType) (Id, OpType)) ->
               Map.Map Int (Map.Map (Id, OpType) ((Id, OpType), Int)) ->
               Map.Map Int (Morphism f e m) ->
               Map.Map ((Id, OpType), Int) (Map.Map Id Int) ->
               Rel.Rel ((Id, OpType), Int) ->
               Map.Map ((Id, OpType), Int) Bool ->
               (OpMap, Map.Map Int (Map.Map (Id, OpType) ((Id, OpType), Int)))
nameSymbols :: Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Map Int (Morphism f e m)
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> Rel ((SORT, OpType), Int)
-> Map ((SORT, OpType), Int) Bool
-> (OpMap, Map Int (Map (SORT, OpType) ((SORT, OpType), Int)))
nameSymbols graph :: Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph morMap :: Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap phi :: Map Int (Morphism f e m)
phi names :: Map ((SORT, OpType), Int) (Map SORT Int)
names ovrl :: Rel ((SORT, OpType), Int)
ovrl totalOps :: Map ((SORT, OpType), Int) Bool
totalOps = let
  colimOvrl :: [Set ((SORT, OpType), Int)]
colimOvrl = Rel ((SORT, OpType), Int) -> [Set ((SORT, OpType), Int)]
forall a. Ord a => Rel a -> [Set a]
Rel.sccOfClosure Rel ((SORT, OpType), Int)
ovrl
  nameClass :: OpMap
-> [SORT]
-> (Set ((SORT, OpType), Int), Int)
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> (OpMap, [SORT],
    Map Int (Map (SORT, OpType) ((SORT, OpType), Int)))
nameClass opFun :: OpMap
opFun gNames :: [SORT]
gNames (set :: Set ((SORT, OpType), Int)
set, idx :: Int
idx) morFun :: Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morFun = let
    (newName :: SORT
newName, gNames' :: [SORT]
gNames') = (Set ((SORT, OpType), Int), Int)
-> [SORT]
-> Map ((SORT, OpType), Int) (Map SORT Int)
-> (SORT, [SORT])
assignName (Set ((SORT, OpType), Int)
set, Int
idx) [SORT]
gNames Map ((SORT, OpType), Int) (Map SORT Int)
names
    opTypes :: Set OpType
opTypes = (((SORT, OpType), Int) -> OpType)
-> Set ((SORT, OpType), Int) -> Set OpType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ ((oldId :: SORT
oldId, ot :: OpType
ot), i :: Int
i) -> let
                 oKind' :: OpKind
oKind' = if Bool
-> ((SORT, OpType), Int) -> Map ((SORT, OpType), Int) Bool -> Bool
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Bool
False
                             ((SORT
oldId, OpType -> OpType
mkPartial OpType
ot), Int
i)
                             Map ((SORT, OpType), Int) Bool
totalOps
                           then OpKind
Total else OpKind
Partial
                 imor :: Morphism f e m
imor = Morphism f e m -> Int -> Map Int (Morphism f e m) -> Morphism f e m
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Morphism f e m
forall a. HasCallStack => [Char] -> a
error "imor") Int
i Map Int (Morphism f e m)
phi
                in Sort_map -> OpType -> OpType
mapOpType (Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
imor) (OpType -> OpType) -> OpType -> OpType
forall a b. (a -> b) -> a -> b
$ OpKind -> OpType -> OpType
setOpKind OpKind
oKind' OpType
ot) Set ((SORT, OpType), Int)
set
    renameSymbols :: Int
-> Map (SORT, OpType) ((SORT, OpType), Int)
-> Map (SORT, OpType) ((SORT, OpType), Int)
renameSymbols n :: Int
n f :: Map (SORT, OpType) ((SORT, OpType), Int)
f = let
        Just opSyms :: Set (SORT, OpType)
opSyms = Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
-> Int -> Maybe (Set (SORT, OpType))
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Maybe a
lab Gr (Set (SORT, OpType)) (Int, Map (SORT, OpType) (SORT, OpType))
graph Int
n
        setKeys :: [(SORT, OpType)]
setKeys = ((SORT, OpType) -> Bool) -> [(SORT, OpType)] -> [(SORT, OpType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: (SORT, OpType)
x -> let y :: ((SORT, OpType), Int)
y = ((SORT, OpType), Int)
-> (SORT, OpType)
-> Map (SORT, OpType) ((SORT, OpType), Int)
-> ((SORT, OpType), Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ((SORT, OpType)
x, Int
n) (SORT, OpType)
x Map (SORT, OpType) ((SORT, OpType), Int)
f
                                in ((SORT, OpType), Int) -> Set ((SORT, OpType), Int) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ((SORT, OpType), Int)
y Set ((SORT, OpType), Int)
set) ([(SORT, OpType)] -> [(SORT, OpType)])
-> [(SORT, OpType)] -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$ Set (SORT, OpType) -> [(SORT, OpType)]
forall a. Set a -> [a]
Set.toList Set (SORT, OpType)
opSyms
        updateAtKey :: (SORT, OpType)
-> ((SORT, OpType), Int) -> Maybe ((SORT, OpType), Int)
updateAtKey (i :: SORT
i, o :: OpType
o) ((i' :: SORT
i', o' :: OpType
o'), n' :: Int
n') = let
          nmor :: Morphism f e m
nmor = Morphism f e m -> Int -> Map Int (Morphism f e m) -> Morphism f e m
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Morphism f e m
forall a. HasCallStack => [Char] -> a
error "nmor") Int
n Map Int (Morphism f e m)
phi
          o'' :: OpType
o'' = Sort_map -> OpType -> OpType
mapOpType (Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
nmor) OpType
o'
          oKind :: OpKind
oKind = if Bool
-> ((SORT, OpType), Int) -> Map ((SORT, OpType), Int) Bool -> Bool
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Bool
False
                             ((SORT
i', OpType -> OpType
mkPartial OpType
o'), Int
n')
                             Map ((SORT, OpType), Int) Bool
totalOps
                           then OpKind
Total else OpKind
Partial
          z :: (SORT, OpType)
z = (SORT
newName, OpKind -> OpType -> OpType
setOpKind OpKind
oKind OpType
o'')
         in if (SORT
i, OpType
o) (SORT, OpType) -> (SORT, OpType) -> Bool
forall a. Eq a => a -> a -> Bool
== (SORT, OpType)
z then
               Maybe ((SORT, OpType), Int)
forall a. Maybe a
Nothing
                          else
               ((SORT, OpType), Int) -> Maybe ((SORT, OpType), Int)
forall a. a -> Maybe a
Just ((SORT, OpType)
z, Int
n')
       in (Map (SORT, OpType) ((SORT, OpType), Int)
 -> (SORT, OpType) -> Map (SORT, OpType) ((SORT, OpType), Int))
-> Map (SORT, OpType) ((SORT, OpType), Int)
-> [(SORT, OpType)]
-> Map (SORT, OpType) ((SORT, OpType), Int)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ g :: Map (SORT, OpType) ((SORT, OpType), Int)
g x :: (SORT, OpType)
x -> (((SORT, OpType), Int) -> Maybe ((SORT, OpType), Int))
-> (SORT, OpType)
-> Map (SORT, OpType) ((SORT, OpType), Int)
-> Map (SORT, OpType) ((SORT, OpType), Int)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update ((SORT, OpType)
-> ((SORT, OpType), Int) -> Maybe ((SORT, OpType), Int)
updateAtKey (SORT, OpType)
x) (SORT, OpType)
x Map (SORT, OpType) ((SORT, OpType), Int)
g)
                 Map (SORT, OpType) ((SORT, OpType), Int)
f [(SORT, OpType)]
setKeys
{- -- i have to map symbols entering set
-- to (newName, their otype mapped) -}
    morFun' :: Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morFun' = (Int
 -> Map (SORT, OpType) ((SORT, OpType), Int)
 -> Map (SORT, OpType) ((SORT, OpType), Int))
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey Int
-> Map (SORT, OpType) ((SORT, OpType), Int)
-> Map (SORT, OpType) ((SORT, OpType), Int)
renameSymbols Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morFun
   in ((Set OpType -> Set OpType) -> SORT -> OpMap -> OpMap
forall a b.
(Ord a, Ord b) =>
(Set b -> Set b) -> a -> MapSet a b -> MapSet a b
MapSet.update (Set OpType -> Set OpType -> Set OpType
forall a b. a -> b -> a
const Set OpType
opTypes) SORT
newName OpMap
opFun, [SORT]
gNames', Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morFun')
  colimOvrl' :: [Set ((SORT, OpType), Int)]
colimOvrl' = (Set ((SORT, OpType), Int)
 -> Set ((SORT, OpType), Int) -> Ordering)
-> [Set ((SORT, OpType), Int)] -> [Set ((SORT, OpType), Int)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\ s1 :: Set ((SORT, OpType), Int)
s1 s2 :: Set ((SORT, OpType), Int)
s2 -> Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Set ((SORT, OpType), Int) -> Int
forall a. Set a -> Int
Set.size Set ((SORT, OpType), Int)
s2) (Set ((SORT, OpType), Int) -> Int
forall a. Set a -> Int
Set.size Set ((SORT, OpType), Int)
s1)) [Set ((SORT, OpType), Int)]
colimOvrl
  (opFuns :: OpMap
opFuns, _, renMap :: Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
renMap) = ((OpMap, [SORT],
  Map Int (Map (SORT, OpType) ((SORT, OpType), Int)))
 -> (Set ((SORT, OpType), Int), Int)
 -> (OpMap, [SORT],
     Map Int (Map (SORT, OpType) ((SORT, OpType), Int))))
-> (OpMap, [SORT],
    Map Int (Map (SORT, OpType) ((SORT, OpType), Int)))
-> [(Set ((SORT, OpType), Int), Int)]
-> (OpMap, [SORT],
    Map Int (Map (SORT, OpType) ((SORT, OpType), Int)))
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (oF :: OpMap
oF, gN :: [SORT]
gN, mM :: Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
mM) x :: (Set ((SORT, OpType), Int), Int)
x -> OpMap
-> [SORT]
-> (Set ((SORT, OpType), Int), Int)
-> Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
-> (OpMap, [SORT],
    Map Int (Map (SORT, OpType) ((SORT, OpType), Int)))
nameClass OpMap
oF [SORT]
gN (Set ((SORT, OpType), Int), Int)
x Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
mM)
                                  (OpMap
forall a b. MapSet a b
MapSet.empty, [], Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
morMap)
                                  ([(Set ((SORT, OpType), Int), Int)]
 -> (OpMap, [SORT],
     Map Int (Map (SORT, OpType) ((SORT, OpType), Int))))
-> [(Set ((SORT, OpType), Int), Int)]
-> (OpMap, [SORT],
    Map Int (Map (SORT, OpType) ((SORT, OpType), Int)))
forall a b. (a -> b) -> a -> b
$ [Set ((SORT, OpType), Int)] -> [(Set ((SORT, OpType), Int), Int)]
forall a. [a] -> [(a, Int)]
number [Set ((SORT, OpType), Int)]
colimOvrl'
 in (OpMap
opFuns , Map Int (Map (SORT, OpType) ((SORT, OpType), Int))
renMap)

{- -CASL signatures colimit on predicate symbols
almost identical with operation symbols,
only minor changes because of different types
- -}

computeColimitPred :: Gr (Sign f e) (Int, Morphism f e m) -> Sign f e ->
      Map.Map Node (Morphism f e m) -> (Sign f e, Map.Map Node (Morphism f e m))
computeColimitPred :: Gr (Sign f e) (Int, Morphism f e m)
-> Sign f e
-> Map Int (Morphism f e m)
-> (Sign f e, Map Int (Morphism f e m))
computeColimitPred graph :: Gr (Sign f e) (Int, Morphism f e m)
graph sigmaOp :: Sign f e
sigmaOp phiOp :: Map Int (Morphism f e m)
phiOp = let
  graph' :: Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph' = Gr (Sign f e) (Int, Morphism f e m)
-> Gr
     (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
forall f e m.
Gr (Sign f e) (Int, Morphism f e m)
-> Gr
     (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
buildPredGraph Gr (Sign f e) (Int, Morphism f e m)
graph
  (colim :: Set ((SORT, PredType), Int)
colim, morMap' :: Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap') = Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> (Set ((SORT, PredType), Int),
    Map Int (Map (SORT, PredType) ((SORT, PredType), Int)))
forall a.
Ord a =>
Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map a (a, Int)))
computeColimitSet Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph'
  (ovrl :: Rel ((SORT, PredType), Int)
ovrl, names :: Map ((SORT, PredType), Int) (Map SORT Int)
names) = Gr (Sign f e) (Int, Morphism f e m)
-> Gr
     (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Set ((SORT, PredType), Int)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> (Rel ((SORT, PredType), Int),
    Map ((SORT, PredType), Int) (Map SORT Int))
forall f e m.
Gr (Sign f e) (Int, Morphism f e m)
-> Gr
     (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Set ((SORT, PredType), Int)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> (Rel ((SORT, PredType), Int),
    Map ((SORT, PredType), Int) (Map SORT Int))
buildPColimOvrl Gr (Sign f e) (Int, Morphism f e m)
graph Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph' Set ((SORT, PredType), Int)
colim Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap'
  (colim1 :: PredMap
colim1, morMap1 :: Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap1) = Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Map Int (Morphism f e m)
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> Rel ((SORT, PredType), Int)
-> (PredMap,
    Map Int (Map (SORT, PredType) ((SORT, PredType), Int)))
forall f e m.
Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Map Int (Morphism f e m)
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> Rel ((SORT, PredType), Int)
-> (PredMap,
    Map Int (Map (SORT, PredType) ((SORT, PredType), Int)))
namePSymbols Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph' Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap' Map Int (Morphism f e m)
phiOp Map ((SORT, PredType), Int) (Map SORT Int)
names Rel ((SORT, PredType), Int)
ovrl
  morMap2 :: Map Int (Map (SORT, PredType) SORT)
morMap2 = (Map (SORT, PredType) ((SORT, PredType), Int)
 -> Map (SORT, PredType) SORT)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Map Int (Map (SORT, PredType) SORT)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((((SORT, PredType), Int) -> SORT)
-> Map (SORT, PredType) ((SORT, PredType), Int)
-> Map (SORT, PredType) SORT
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ ((i :: SORT
i, _p :: PredType
_p), _) -> SORT
i)) Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap1
  sigmaPreds :: Sign f e
sigmaPreds = Sign f e
sigmaOp {predMap :: PredMap
predMap = PredMap
colim1}
  phiPreds :: Map Int (Morphism f e m)
phiPreds = (Int -> Morphism f e m -> Morphism f e m)
-> Map Int (Morphism f e m) -> Map Int (Morphism f e m)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey
          (\ n :: Int
n phi :: Morphism f e m
phi -> Morphism f e m
phi {pred_map :: Map (SORT, PredType) SORT
pred_map =
                         Map (SORT, PredType) SORT
-> Int
-> Map Int (Map (SORT, PredType) SORT)
-> Map (SORT, PredType) SORT
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Map (SORT, PredType) SORT
forall a. HasCallStack => [Char] -> a
error "pred_map") Int
n Map Int (Map (SORT, PredType) SORT)
morMap2})
          Map Int (Morphism f e m)
phiOp
 in (Sign f e
sigmaPreds, Map Int (Morphism f e m)
phiPreds)

buildPredGraph :: Gr (Sign f e) (Int, Morphism f e m) ->
                Gr (Set.Set (Id, PredType))
                   (Int, Map.Map (Id, PredType) (Id, PredType))
buildPredGraph :: Gr (Sign f e) (Int, Morphism f e m)
-> Gr
     (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
buildPredGraph graph :: Gr (Sign f e) (Int, Morphism f e m)
graph = let
  getPreds :: Sign f e -> [(SORT, PredType)]
getPreds = PredMap -> [(SORT, PredType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (PredMap -> [(SORT, PredType)])
-> (Sign f e -> PredMap) -> Sign f e -> [(SORT, PredType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap
  getPredFun :: Morphism f e m -> Map (SORT, PredType) (SORT, PredType)
getPredFun mor :: Morphism f e m
mor = let
                  ssign :: Sign f e
ssign = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
mor
                  smap :: Sort_map
smap = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
mor
                  pmap :: Map (SORT, PredType) SORT
pmap = Morphism f e m -> Map (SORT, PredType) SORT
forall f e m. Morphism f e m -> Map (SORT, PredType) SORT
pred_map Morphism f e m
mor
                 in (Map (SORT, PredType) (SORT, PredType)
 -> (SORT, PredType) -> Map (SORT, PredType) (SORT, PredType))
-> Map (SORT, PredType) (SORT, PredType)
-> [(SORT, PredType)]
-> Map (SORT, PredType) (SORT, PredType)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ f :: Map (SORT, PredType) (SORT, PredType)
f x :: (SORT, PredType)
x -> let y :: (SORT, PredType)
y = Sort_map
-> Map (SORT, PredType) SORT
-> (SORT, PredType)
-> (SORT, PredType)
mapPredSym Sort_map
smap Map (SORT, PredType) SORT
pmap (SORT, PredType)
x
                                  in if (SORT, PredType)
x (SORT, PredType) -> (SORT, PredType) -> Bool
forall a. Eq a => a -> a -> Bool
== (SORT, PredType)
y then Map (SORT, PredType) (SORT, PredType)
f else (SORT, PredType)
-> (SORT, PredType)
-> Map (SORT, PredType) (SORT, PredType)
-> Map (SORT, PredType) (SORT, PredType)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT, PredType)
x (SORT, PredType)
y Map (SORT, PredType) (SORT, PredType)
f)
                  Map (SORT, PredType) (SORT, PredType)
forall k a. Map k a
Map.empty ([(SORT, PredType)] -> Map (SORT, PredType) (SORT, PredType))
-> [(SORT, PredType)] -> Map (SORT, PredType) (SORT, PredType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> [(SORT, PredType)]
forall f e. Sign f e -> [(SORT, PredType)]
getPreds Sign f e
ssign
 in (Sign f e -> Set (SORT, PredType))
-> Gr (Sign f e) (Int, Map (SORT, PredType) (SORT, PredType))
-> Gr
     (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
nmap ([(SORT, PredType)] -> Set (SORT, PredType)
forall a. Ord a => [a] -> Set a
Set.fromList ([(SORT, PredType)] -> Set (SORT, PredType))
-> (Sign f e -> [(SORT, PredType)])
-> Sign f e
-> Set (SORT, PredType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> [(SORT, PredType)]
forall f e. Sign f e -> [(SORT, PredType)]
getPreds) (Gr (Sign f e) (Int, Map (SORT, PredType) (SORT, PredType))
 -> Gr
      (Set (SORT, PredType))
      (Int, Map (SORT, PredType) (SORT, PredType)))
-> Gr (Sign f e) (Int, Map (SORT, PredType) (SORT, PredType))
-> Gr
     (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
forall a b. (a -> b) -> a -> b
$ ((Int, Morphism f e m)
 -> (Int, Map (SORT, PredType) (SORT, PredType)))
-> Gr (Sign f e) (Int, Morphism f e m)
-> Gr (Sign f e) (Int, Map (SORT, PredType) (SORT, PredType))
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
emap (\ (i :: Int
i, m :: Morphism f e m
m) -> (Int
i, Morphism f e m -> Map (SORT, PredType) (SORT, PredType)
forall f e m.
Morphism f e m -> Map (SORT, PredType) (SORT, PredType)
getPredFun Morphism f e m
m)) Gr (Sign f e) (Int, Morphism f e m)
graph


buildPColimOvrl :: Gr (Sign f e) (Int, Morphism f e m) ->
                  Gr (Set.Set (Id, PredType)) (Int, EndoMap (Id, PredType)) ->
                  Set.Set ((Id, PredType), Int) ->
                  Map.Map Int (Map.Map (Id, PredType) ((Id, PredType), Int)) ->
                  (Rel.Rel ((Id, PredType), Int),
                   Map.Map ((Id, PredType), Int) (Map.Map Id Int))
buildPColimOvrl :: Gr (Sign f e) (Int, Morphism f e m)
-> Gr
     (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Set ((SORT, PredType), Int)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> (Rel ((SORT, PredType), Int),
    Map ((SORT, PredType), Int) (Map SORT Int))
buildPColimOvrl graph :: Gr (Sign f e) (Int, Morphism f e m)
graph graph' :: Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph' colim :: Set ((SORT, PredType), Int)
colim morMap :: Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap = let
   (ovrl :: Rel a
ovrl, names :: Map ((SORT, PredType), Int) (Map k a)
names) = (Rel a
forall a. Rel a
Rel.empty, [(((SORT, PredType), Int), Map k a)]
-> Map ((SORT, PredType), Int) (Map k a)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(((SORT, PredType), Int), Map k a)]
 -> Map ((SORT, PredType), Int) (Map k a))
-> [(((SORT, PredType), Int), Map k a)]
-> Map ((SORT, PredType), Int) (Map k a)
forall a b. (a -> b) -> a -> b
$ [((SORT, PredType), Int)]
-> [Map k a] -> [(((SORT, PredType), Int), Map k a)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Set ((SORT, PredType), Int) -> [((SORT, PredType), Int)]
forall a. Set a -> [a]
Set.toList Set ((SORT, PredType), Int)
colim) ([Map k a] -> [(((SORT, PredType), Int), Map k a)])
-> [Map k a] -> [(((SORT, PredType), Int), Map k a)]
forall a b. (a -> b) -> a -> b
$
                                                  Map k a -> [Map k a]
forall a. a -> [a]
repeat Map k a
forall k a. Map k a
Map.empty )
   (ovrl' :: Rel ((SORT, PredType), Int)
ovrl', names' :: Map ((SORT, PredType), Int) (Map SORT Int)
names') = Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Set ((SORT, PredType), Int)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Rel ((SORT, PredType), Int)
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> [(Int, Sign f e)]
-> (Rel ((SORT, PredType), Int),
    Map ((SORT, PredType), Int) (Map SORT Int))
forall f e.
Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Set ((SORT, PredType), Int)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Rel ((SORT, PredType), Int)
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> [(Int, Sign f e)]
-> (Rel ((SORT, PredType), Int),
    Map ((SORT, PredType), Int) (Map SORT Int))
buildPOvrlAtNode Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph' Set ((SORT, PredType), Int)
colim Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap
                      Rel ((SORT, PredType), Int)
forall a. Rel a
ovrl Map ((SORT, PredType), Int) (Map SORT Int)
forall k a. Map ((SORT, PredType), Int) (Map k a)
names ([(Int, Sign f e)]
 -> (Rel ((SORT, PredType), Int),
     Map ((SORT, PredType), Int) (Map SORT Int)))
-> [(Int, Sign f e)]
-> (Rel ((SORT, PredType), Int),
    Map ((SORT, PredType), Int) (Map SORT Int))
forall a b. (a -> b) -> a -> b
$ Gr (Sign f e) (Int, Morphism f e m) -> [(Int, Sign f e)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr (Sign f e) (Int, Morphism f e m)
graph
  in (Rel ((SORT, PredType), Int) -> Rel ((SORT, PredType), Int)
forall a. Ord a => Rel a -> Rel a
Rel.transClosure Rel ((SORT, PredType), Int)
ovrl', Map ((SORT, PredType), Int) (Map SORT Int)
names')

buildPOvrlAtNode :: Gr (Set.Set (Id, PredType)) (Int, EndoMap (Id, PredType)) ->
                   Set.Set ((Id, PredType), Int) ->
                   Map.Map Int (Map.Map (Id, PredType) ((Id, PredType), Int)) ->
                   Rel.Rel ((Id, PredType), Int) ->
                   Map.Map ((Id, PredType), Int) (Map.Map Id Int) ->
                   [(Int, Sign f e)] ->
                   (Rel.Rel ((Id, PredType), Int),
                   Map.Map ((Id, PredType), Int) (Map.Map Id Int))
buildPOvrlAtNode :: Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Set ((SORT, PredType), Int)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Rel ((SORT, PredType), Int)
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> [(Int, Sign f e)]
-> (Rel ((SORT, PredType), Int),
    Map ((SORT, PredType), Int) (Map SORT Int))
buildPOvrlAtNode graph' :: Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph' colim :: Set ((SORT, PredType), Int)
colim morMap :: Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap ovrl :: Rel ((SORT, PredType), Int)
ovrl names :: Map ((SORT, PredType), Int) (Map SORT Int)
names nodeList :: [(Int, Sign f e)]
nodeList =
 case [(Int, Sign f e)]
nodeList of
   [] -> (Rel ((SORT, PredType), Int)
ovrl, Map ((SORT, PredType), Int) (Map SORT Int)
names)
   (n :: Int
n, sig :: Sign f e
sig) : lists :: [(Int, Sign f e)]
lists -> let
       Just pSet :: Set (SORT, PredType)
pSet = Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Int -> Maybe (Set (SORT, PredType))
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Maybe a
lab Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph' Int
n
       names' :: Map ((SORT, PredType), Int) (Map SORT Int)
names' = (Map ((SORT, PredType), Int) (Map SORT Int)
 -> (SORT, PredType) -> Map ((SORT, PredType), Int) (Map SORT Int))
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> [(SORT, PredType)]
-> Map ((SORT, PredType), Int) (Map SORT Int)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ g :: Map ((SORT, PredType), Int) (Map SORT Int)
g x :: (SORT, PredType)
x@(idN :: SORT
idN, _) -> let
                                 y :: ((SORT, PredType), Int)
y = ((SORT, PredType), Int)
-> (SORT, PredType)
-> Map (SORT, PredType) ((SORT, PredType), Int)
-> ((SORT, PredType), Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ((SORT, PredType)
x, Int
n) (SORT, PredType)
x (Map (SORT, PredType) ((SORT, PredType), Int)
 -> ((SORT, PredType), Int))
-> Map (SORT, PredType) ((SORT, PredType), Int)
-> ((SORT, PredType), Int)
forall a b. (a -> b) -> a -> b
$
                                     Map (SORT, PredType) ((SORT, PredType), Int)
-> Int
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Map (SORT, PredType) ((SORT, PredType), Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Map (SORT, PredType) ((SORT, PredType), Int)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Map (SORT, PredType) ((SORT, PredType), Int))
-> [Char] -> Map (SORT, PredType) ((SORT, PredType), Int)
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
                                         Int
n Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap
                                 altF :: Maybe a -> Maybe a
altF v :: Maybe a
v = case Maybe a
v of
                                      Nothing -> a -> Maybe a
forall a. a -> Maybe a
Just 1
                                      Just m :: a
m -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a
m a -> a -> a
forall a. Num a => a -> a -> a
+ 1
                                in (Map SORT Int -> Map SORT Int)
-> ((SORT, PredType), Int)
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> Map ((SORT, PredType), Int) (Map SORT Int)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ((Maybe Int -> Maybe Int) -> SORT -> Map SORT Int -> Map SORT Int
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter Maybe Int -> Maybe Int
forall a. Num a => Maybe a -> Maybe a
altF SORT
idN)
                                   ((SORT, PredType), Int)
y Map ((SORT, PredType), Int) (Map SORT Int)
g)
                       Map ((SORT, PredType), Int) (Map SORT Int)
names ([(SORT, PredType)] -> Map ((SORT, PredType), Int) (Map SORT Int))
-> [(SORT, PredType)] -> Map ((SORT, PredType), Int) (Map SORT Int)
forall a b. (a -> b) -> a -> b
$ Set (SORT, PredType) -> [(SORT, PredType)]
forall a. Set a -> [a]
Set.toList Set (SORT, PredType)
pSet
       equivP :: (a, PredType) -> (a, PredType) -> Bool
equivP (id1 :: a
id1, pt1 :: PredType
pt1) (id2 :: a
id2, pt2 :: PredType
pt2) = (a
id1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
id2) Bool -> Bool -> Bool
&& Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP Sign f e
sig PredType
pt1 PredType
pt2
       parts :: [[(SORT, PredType)]]
parts = ((SORT, PredType) -> (SORT, PredType) -> Bool)
-> Set (SORT, PredType) -> [[(SORT, PredType)]]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [[a]]
Rel.leqClasses (SORT, PredType) -> (SORT, PredType) -> Bool
forall a. Eq a => (a, PredType) -> (a, PredType) -> Bool
equivP Set (SORT, PredType)
pSet
       nmor :: Map (SORT, PredType) ((SORT, PredType), Int)
nmor = Map (SORT, PredType) ((SORT, PredType), Int)
-> Int
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Map (SORT, PredType) ((SORT, PredType), Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Map (SORT, PredType) ((SORT, PredType), Int)
forall a. HasCallStack => [Char] -> a
error "buildAtNode") Int
n Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap
       addParts :: Rel ((SORT, PredType), Int)
-> [[(SORT, PredType)]] -> Rel ((SORT, PredType), Int)
addParts =
         (Rel ((SORT, PredType), Int)
 -> [(SORT, PredType)] -> Rel ((SORT, PredType), Int))
-> Rel ((SORT, PredType), Int)
-> [[(SORT, PredType)]]
-> Rel ((SORT, PredType), Int)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ r :: Rel ((SORT, PredType), Int)
r l :: [(SORT, PredType)]
l -> let l1 :: [((SORT, PredType), Int)]
l1 = ((SORT, PredType) -> ((SORT, PredType), Int))
-> [(SORT, PredType)] -> [((SORT, PredType), Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: (SORT, PredType)
x ->
                                  ((SORT, PredType), Int)
-> (SORT, PredType)
-> Map (SORT, PredType) ((SORT, PredType), Int)
-> ((SORT, PredType), Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ((SORT, PredType)
x, Int
n) (SORT, PredType)
x Map (SORT, PredType) ((SORT, PredType), Int)
nmor) [(SORT, PredType)]
l
                        in case [((SORT, PredType), Int)]
l1 of
                   [] -> [Char] -> Rel ((SORT, PredType), Int)
forall a. HasCallStack => [Char] -> a
error "addParts"
                   x :: ((SORT, PredType), Int)
x : xs :: [((SORT, PredType), Int)]
xs -> let
                             (r' :: Rel ((SORT, PredType), Int)
r', ly :: ((SORT, PredType), Int)
ly) = ((Rel ((SORT, PredType), Int), ((SORT, PredType), Int))
 -> ((SORT, PredType), Int)
 -> (Rel ((SORT, PredType), Int), ((SORT, PredType), Int)))
-> (Rel ((SORT, PredType), Int), ((SORT, PredType), Int))
-> [((SORT, PredType), Int)]
-> (Rel ((SORT, PredType), Int), ((SORT, PredType), Int))
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
                              (\ (rl :: Rel ((SORT, PredType), Int)
rl, lx :: ((SORT, PredType), Int)
lx) y :: ((SORT, PredType), Int)
y -> (((SORT, PredType), Int)
-> ((SORT, PredType), Int)
-> Rel ((SORT, PredType), Int)
-> Rel ((SORT, PredType), Int)
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair ((SORT, PredType), Int)
lx ((SORT, PredType), Int)
y Rel ((SORT, PredType), Int)
rl, ((SORT, PredType), Int)
y))
                              (Rel ((SORT, PredType), Int)
r, ((SORT, PredType), Int)
x) [((SORT, PredType), Int)]
xs
                            in ((SORT, PredType), Int)
-> ((SORT, PredType), Int)
-> Rel ((SORT, PredType), Int)
-> Rel ((SORT, PredType), Int)
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair ((SORT, PredType), Int)
ly ((SORT, PredType), Int)
x Rel ((SORT, PredType), Int)
r'
                          )
       ovrl' :: Rel ((SORT, PredType), Int)
ovrl' = Rel ((SORT, PredType), Int)
-> [[(SORT, PredType)]] -> Rel ((SORT, PredType), Int)
addParts Rel ((SORT, PredType), Int)
ovrl [[(SORT, PredType)]]
parts
     in Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Set ((SORT, PredType), Int)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Rel ((SORT, PredType), Int)
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> [(Int, Sign f e)]
-> (Rel ((SORT, PredType), Int),
    Map ((SORT, PredType), Int) (Map SORT Int))
forall f e.
Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Set ((SORT, PredType), Int)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Rel ((SORT, PredType), Int)
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> [(Int, Sign f e)]
-> (Rel ((SORT, PredType), Int),
    Map ((SORT, PredType), Int) (Map SORT Int))
buildPOvrlAtNode Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph' Set ((SORT, PredType), Int)
colim Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap Rel ((SORT, PredType), Int)
ovrl' Map ((SORT, PredType), Int) (Map SORT Int)
names' [(Int, Sign f e)]
lists

assignPName :: (Set.Set ((Id, PredType), Int), Int) -> [Id] ->
              Map.Map ((Id, PredType), Int) (Map.Map Id Int) ->
              (Id, [Id])
assignPName :: (Set ((SORT, PredType), Int), Int)
-> [SORT]
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> (SORT, [SORT])
assignPName (pSet :: Set ((SORT, PredType), Int)
pSet, idx :: Int
idx) givenNames :: [SORT]
givenNames namesFun :: Map ((SORT, PredType), Int) (Map SORT Int)
namesFun =
 let pSetNames :: Map SORT Int
pSetNames = (((SORT, PredType), Int) -> Map SORT Int -> Map SORT Int)
-> Map SORT Int -> Set ((SORT, PredType), Int) -> Map SORT Int
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ x :: ((SORT, PredType), Int)
x f :: Map SORT Int
f -> (Int -> Int -> Int) -> Map SORT Int -> Map SORT Int -> Map SORT Int
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Map SORT Int
f
                            (Map SORT Int
-> ((SORT, PredType), Int)
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> Map SORT Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Map SORT Int
forall a. HasCallStack => [Char] -> a
error "pname") ((SORT, PredType), Int)
x Map ((SORT, PredType), Int) (Map SORT Int)
namesFun))
                           Map SORT Int
forall k a. Map k a
Map.empty Set ((SORT, PredType), Int)
pSet
     availNames :: [SORT]
availNames = (SORT -> Bool) -> [SORT] -> [SORT]
forall a. (a -> Bool) -> [a] -> [a]
filter (SORT -> [SORT] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [SORT]
givenNames) ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ Map SORT Int -> [SORT]
forall k a. Map k a -> [k]
Map.keys Map SORT Int
pSetNames
 in case [SORT]
availNames of
     [] -> let
       -- must generate name with the most frequent name idx and an origin
        sndOrd :: SORT -> SORT -> Ordering
sndOrd x :: SORT
x y :: SORT
y = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Map SORT Int
pSetNames Map SORT Int -> SORT -> Int
forall k a. Ord k => Map k a -> k -> a
Map.! SORT
x) (Map SORT Int
pSetNames Map SORT Int -> SORT -> Int
forall k a. Ord k => Map k a -> k -> a
Map.! SORT
y)
        avail' :: [SORT]
avail' = (SORT -> SORT -> Ordering) -> [SORT] -> [SORT]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy SORT -> SORT -> Ordering
sndOrd ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ Map SORT Int -> [SORT]
forall k a. Map k a -> [k]
Map.keys Map SORT Int
pSetNames
        idN :: SORT
idN = [SORT] -> SORT
forall a. [a] -> a
head [SORT]
avail'
       in (SORT -> [Char] -> SORT
appendString SORT
idN ([Char] -> SORT) -> [Char] -> SORT
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
idx, [SORT]
givenNames)
     _ -> {- must take the most frequent available name and give it to the class
          and this name becomes given -}
          let
         sndOrd :: SORT -> SORT -> Ordering
sndOrd x :: SORT
x y :: SORT
y = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Map SORT Int
pSetNames Map SORT Int -> SORT -> Int
forall k a. Ord k => Map k a -> k -> a
Map.! SORT
x) (Map SORT Int
pSetNames Map SORT Int -> SORT -> Int
forall k a. Ord k => Map k a -> k -> a
Map.! SORT
y)
         avail' :: [SORT]
avail' = (SORT -> SORT -> Ordering) -> [SORT] -> [SORT]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy SORT -> SORT -> Ordering
sndOrd [SORT]
availNames
         idN :: SORT
idN = [SORT] -> SORT
forall a. [a] -> a
last [SORT]
avail'
        in (SORT
idN, SORT
idN SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: [SORT]
givenNames)

namePSymbols :: Gr (Set.Set (Id, PredType))
                   (Int, Map.Map (Id, PredType) (Id, PredType)) ->
               Map.Map Int (Map.Map (Id, PredType) ((Id, PredType), Int)) ->
               Map.Map Int (Morphism f e m) ->
               Map.Map ((Id, PredType), Int) (Map.Map Id Int) ->
               Rel.Rel ((Id, PredType), Int) ->
               (PredMap, Map.Map Int (Map.Map (Id, PredType)
                                              ((Id, PredType), Int)))
namePSymbols :: Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Map Int (Morphism f e m)
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> Rel ((SORT, PredType), Int)
-> (PredMap,
    Map Int (Map (SORT, PredType) ((SORT, PredType), Int)))
namePSymbols graph :: Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph morMap :: Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap phi :: Map Int (Morphism f e m)
phi names :: Map ((SORT, PredType), Int) (Map SORT Int)
names ovrl :: Rel ((SORT, PredType), Int)
ovrl = let
  colimOvrl :: [Set ((SORT, PredType), Int)]
colimOvrl = Rel ((SORT, PredType), Int) -> [Set ((SORT, PredType), Int)]
forall a. Ord a => Rel a -> [Set a]
Rel.sccOfClosure Rel ((SORT, PredType), Int)
ovrl
  nameClass :: PredMap
-> [SORT]
-> (Set ((SORT, PredType), Int), Int)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> (PredMap, [SORT],
    Map Int (Map (SORT, PredType) ((SORT, PredType), Int)))
nameClass pFun :: PredMap
pFun gNames :: [SORT]
gNames (set :: Set ((SORT, PredType), Int)
set, idx :: Int
idx) morFun :: Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morFun = let
    (newName :: SORT
newName, gNames' :: [SORT]
gNames') = (Set ((SORT, PredType), Int), Int)
-> [SORT]
-> Map ((SORT, PredType), Int) (Map SORT Int)
-> (SORT, [SORT])
assignPName (Set ((SORT, PredType), Int)
set, Int
idx) [SORT]
gNames Map ((SORT, PredType), Int) (Map SORT Int)
names
    pTypes :: Set PredType
pTypes = (((SORT, PredType), Int) -> PredType)
-> Set ((SORT, PredType), Int) -> Set PredType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ ((_oldId :: SORT
_oldId, pt :: PredType
pt), i :: Int
i) -> let
                in Sort_map -> PredType -> PredType
mapPredType (Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map (Morphism f e m -> Sort_map) -> Morphism f e m -> Sort_map
forall a b. (a -> b) -> a -> b
$ Map Int (Morphism f e m)
phi Map Int (Morphism f e m) -> Int -> Morphism f e m
forall k a. Ord k => Map k a -> k -> a
Map.! Int
i) PredType
pt) Set ((SORT, PredType), Int)
set
    renameSymbols :: Int
-> Map (SORT, PredType) ((SORT, PredType), Int)
-> Map (SORT, PredType) ((SORT, PredType), Int)
renameSymbols n :: Int
n f :: Map (SORT, PredType) ((SORT, PredType), Int)
f = let
        Just pSyms :: Set (SORT, PredType)
pSyms = Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
-> Int -> Maybe (Set (SORT, PredType))
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Maybe a
lab Gr
  (Set (SORT, PredType)) (Int, Map (SORT, PredType) (SORT, PredType))
graph Int
n
        setKeys :: [(SORT, PredType)]
setKeys = ((SORT, PredType) -> Bool)
-> [(SORT, PredType)] -> [(SORT, PredType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: (SORT, PredType)
x -> let y :: ((SORT, PredType), Int)
y = ((SORT, PredType), Int)
-> (SORT, PredType)
-> Map (SORT, PredType) ((SORT, PredType), Int)
-> ((SORT, PredType), Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ((SORT, PredType)
x, Int
n) (SORT, PredType)
x Map (SORT, PredType) ((SORT, PredType), Int)
f
                                in ((SORT, PredType), Int) -> Set ((SORT, PredType), Int) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ((SORT, PredType), Int)
y Set ((SORT, PredType), Int)
set) ([(SORT, PredType)] -> [(SORT, PredType)])
-> [(SORT, PredType)] -> [(SORT, PredType)]
forall a b. (a -> b) -> a -> b
$ Set (SORT, PredType) -> [(SORT, PredType)]
forall a. Set a -> [a]
Set.toList Set (SORT, PredType)
pSyms
        updateAtKey :: (SORT, PredType)
-> ((a, PredType), b) -> Maybe ((SORT, PredType), b)
updateAtKey (i :: SORT
i, p :: PredType
p) ((_i' :: a
_i', p' :: PredType
p'), n' :: b
n') = let
          p'' :: PredType
p'' = Sort_map -> PredType -> PredType
mapPredType (Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map (Morphism f e m -> Sort_map) -> Morphism f e m -> Sort_map
forall a b. (a -> b) -> a -> b
$ Map Int (Morphism f e m)
phi Map Int (Morphism f e m) -> Int -> Morphism f e m
forall k a. Ord k => Map k a -> k -> a
Map.! Int
n) PredType
p'
          z :: (SORT, PredType)
z = (SORT
newName, PredType
p'')
         in if (SORT
i, PredType
p) (SORT, PredType) -> (SORT, PredType) -> Bool
forall a. Eq a => a -> a -> Bool
== (SORT, PredType)
z then
               Maybe ((SORT, PredType), b)
forall a. Maybe a
Nothing
                          else
               ((SORT, PredType), b) -> Maybe ((SORT, PredType), b)
forall a. a -> Maybe a
Just ((SORT, PredType)
z, b
n')
       in (Map (SORT, PredType) ((SORT, PredType), Int)
 -> (SORT, PredType)
 -> Map (SORT, PredType) ((SORT, PredType), Int))
-> Map (SORT, PredType) ((SORT, PredType), Int)
-> [(SORT, PredType)]
-> Map (SORT, PredType) ((SORT, PredType), Int)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ g :: Map (SORT, PredType) ((SORT, PredType), Int)
g x :: (SORT, PredType)
x -> (((SORT, PredType), Int) -> Maybe ((SORT, PredType), Int))
-> (SORT, PredType)
-> Map (SORT, PredType) ((SORT, PredType), Int)
-> Map (SORT, PredType) ((SORT, PredType), Int)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update ((SORT, PredType)
-> ((SORT, PredType), Int) -> Maybe ((SORT, PredType), Int)
forall a b.
(SORT, PredType)
-> ((a, PredType), b) -> Maybe ((SORT, PredType), b)
updateAtKey (SORT, PredType)
x) (SORT, PredType)
x Map (SORT, PredType) ((SORT, PredType), Int)
g)
                 Map (SORT, PredType) ((SORT, PredType), Int)
f [(SORT, PredType)]
setKeys
{- -- i have to map symbols entering set
-- to (newName, their predtype mapped) -}
    morFun' :: Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morFun' = (Int
 -> Map (SORT, PredType) ((SORT, PredType), Int)
 -> Map (SORT, PredType) ((SORT, PredType), Int))
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey Int
-> Map (SORT, PredType) ((SORT, PredType), Int)
-> Map (SORT, PredType) ((SORT, PredType), Int)
renameSymbols Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morFun
   in ((Set PredType -> Set PredType) -> SORT -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
(Set b -> Set b) -> a -> MapSet a b -> MapSet a b
MapSet.update (Set PredType -> Set PredType -> Set PredType
forall a b. a -> b -> a
const Set PredType
pTypes) SORT
newName PredMap
pFun, [SORT]
gNames', Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morFun')
  colimOvrl' :: [Set ((SORT, PredType), Int)]
colimOvrl' = (Set ((SORT, PredType), Int)
 -> Set ((SORT, PredType), Int) -> Ordering)
-> [Set ((SORT, PredType), Int)] -> [Set ((SORT, PredType), Int)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\ s1 :: Set ((SORT, PredType), Int)
s1 s2 :: Set ((SORT, PredType), Int)
s2 -> Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Set ((SORT, PredType), Int) -> Int
forall a. Set a -> Int
Set.size Set ((SORT, PredType), Int)
s2) (Set ((SORT, PredType), Int) -> Int
forall a. Set a -> Int
Set.size Set ((SORT, PredType), Int)
s1)) [Set ((SORT, PredType), Int)]
colimOvrl
  (pFuns :: PredMap
pFuns, _, renMap :: Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
renMap) = ((PredMap, [SORT],
  Map Int (Map (SORT, PredType) ((SORT, PredType), Int)))
 -> (Set ((SORT, PredType), Int), Int)
 -> (PredMap, [SORT],
     Map Int (Map (SORT, PredType) ((SORT, PredType), Int))))
-> (PredMap, [SORT],
    Map Int (Map (SORT, PredType) ((SORT, PredType), Int)))
-> [(Set ((SORT, PredType), Int), Int)]
-> (PredMap, [SORT],
    Map Int (Map (SORT, PredType) ((SORT, PredType), Int)))
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (pF :: PredMap
pF, gN :: [SORT]
gN, mM :: Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
mM) x :: (Set ((SORT, PredType), Int), Int)
x -> PredMap
-> [SORT]
-> (Set ((SORT, PredType), Int), Int)
-> Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
-> (PredMap, [SORT],
    Map Int (Map (SORT, PredType) ((SORT, PredType), Int)))
nameClass PredMap
pF [SORT]
gN (Set ((SORT, PredType), Int), Int)
x Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
mM)
                                  (PredMap
forall a b. MapSet a b
MapSet.empty, [], Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
morMap)
                                  ([(Set ((SORT, PredType), Int), Int)]
 -> (PredMap, [SORT],
     Map Int (Map (SORT, PredType) ((SORT, PredType), Int))))
-> [(Set ((SORT, PredType), Int), Int)]
-> (PredMap, [SORT],
    Map Int (Map (SORT, PredType) ((SORT, PredType), Int)))
forall a b. (a -> b) -> a -> b
$ [Set ((SORT, PredType), Int)]
-> [(Set ((SORT, PredType), Int), Int)]
forall a. [a] -> [(a, Int)]
number [Set ((SORT, PredType), Int)]
colimOvrl'
 in (PredMap
pFuns , Map Int (Map (SORT, PredType) ((SORT, PredType), Int))
renMap)

applyMor :: Morphism f e m -> (Id, OpType) -> (Id, OpType)
applyMor :: Morphism f e m -> (SORT, OpType) -> (SORT, OpType)
applyMor phi :: Morphism f e m
phi (i :: SORT
i, optype :: OpType
optype) = Sort_map
-> Map (SORT, OpType) (SORT, OpKind)
-> (SORT, OpType)
-> (SORT, OpType)
mapOpSym (Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
phi) (Morphism f e m -> Map (SORT, OpType) (SORT, OpKind)
forall f e m. Morphism f e m -> Map (SORT, OpType) (SORT, OpKind)
op_map Morphism f e m
phi) (SORT
i, OpType
optype)

-- associative operations

assocSymbols :: Sign f e -> [(Id, OpType)]
assocSymbols :: Sign f e -> [(SORT, OpType)]
assocSymbols = OpMap -> [(SORT, OpType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (OpMap -> [(SORT, OpType)])
-> (Sign f e -> OpMap) -> Sign f e -> [(SORT, OpType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> OpMap
forall f e. Sign f e -> OpMap
assocOps

colimitAssoc :: Gr (Sign f e) (Int, Morphism f e m) -> Sign f e ->
   Map.Map Int (Morphism f e m) -> (Sign f e, Map.Map Int (Morphism f e m))
colimitAssoc :: Gr (Sign f e) (Int, Morphism f e m)
-> Sign f e
-> Map Int (Morphism f e m)
-> (Sign f e, Map Int (Morphism f e m))
colimitAssoc graph :: Gr (Sign f e) (Int, Morphism f e m)
graph sig :: Sign f e
sig morMap :: Map Int (Morphism f e m)
morMap = let
  assocOpList :: [(SORT, OpType)]
assocOpList = [(SORT, OpType)] -> [(SORT, OpType)]
forall a. Ord a => [a] -> [a]
nubOrd ([(SORT, OpType)] -> [(SORT, OpType)])
-> [(SORT, OpType)] -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$ ((Int, Sign f e) -> [(SORT, OpType)])
-> [(Int, Sign f e)] -> [(SORT, OpType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
    (\ (node :: Int
node, sigma :: Sign f e
sigma) -> ((SORT, OpType) -> (SORT, OpType))
-> [(SORT, OpType)] -> [(SORT, OpType)]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism f e m -> (SORT, OpType) -> (SORT, OpType)
forall f e m. Morphism f e m -> (SORT, OpType) -> (SORT, OpType)
applyMor (Map Int (Morphism f e m) -> Int -> Morphism f e m
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map Int (Morphism f e m)
morMap Int
node)) ([(SORT, OpType)] -> [(SORT, OpType)])
-> [(SORT, OpType)] -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$
    Sign f e -> [(SORT, OpType)]
forall f e. Sign f e -> [(SORT, OpType)]
assocSymbols Sign f e
sigma ) ([(Int, Sign f e)] -> [(SORT, OpType)])
-> [(Int, Sign f e)] -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$ Gr (Sign f e) (Int, Morphism f e m) -> [(Int, Sign f e)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr (Sign f e) (Int, Morphism f e m)
graph
  idList :: [SORT]
idList = [SORT] -> [SORT]
forall a. Ord a => [a] -> [a]
nubOrd ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType) -> SORT) -> [(SORT, OpType)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, OpType) -> SORT
forall a b. (a, b) -> a
fst [(SORT, OpType)]
assocOpList
  sig1 :: Sign f e
sig1 = Sign f e
sig {assocOps :: OpMap
assocOps = [(SORT, [OpType])] -> OpMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList ([(SORT, [OpType])] -> OpMap) -> [(SORT, [OpType])] -> OpMap
forall a b. (a -> b) -> a -> b
$
   (SORT -> (SORT, [OpType])) -> [SORT] -> [(SORT, [OpType])]
forall a b. (a -> b) -> [a] -> [b]
map (\ sb :: SORT
sb -> (SORT
sb, ((SORT, OpType) -> OpType) -> [(SORT, OpType)] -> [OpType]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, OpType) -> OpType
forall a b. (a, b) -> b
snd ([(SORT, OpType)] -> [OpType]) -> [(SORT, OpType)] -> [OpType]
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType) -> Bool) -> [(SORT, OpType)] -> [(SORT, OpType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (i :: SORT
i, _) -> SORT
i SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
sb)
                                            [(SORT, OpType)]
assocOpList )) [SORT]
idList}
  morMap1 :: Map Int (Morphism f e m)
morMap1 = (Morphism f e m -> Morphism f e m)
-> Map Int (Morphism f e m) -> Map Int (Morphism f e m)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ phi :: Morphism f e m
phi -> Morphism f e m
phi {mtarget :: Sign f e
mtarget = Sign f e
sig1}) Map Int (Morphism f e m)
morMap
 in (Sign f e
sig1, Map Int (Morphism f e m)
morMap1)