{- |
Module      :  ./Proofs/DGFlattening.hs
Description :  flattening parts of development graphs
Copyright   :  (c) Igor Stassiy, DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

In this module we introduce flattening of the graph:

Flattening importings - deleting all inclusion links,
 and inserting a new node, with new computed theory (computeTheory).

Flattening non-disjoint unions - for each node with more than two importings
 modify importings in such a way that at each level, only non-disjoint
 signatures are imported.

Flattening renaming - deterimining renaming link,
inserting a new node with the renaming morphism applied to theory of a
source, deleting the link and setting a new inclusion link between a
new node and the target node.

Flattening hiding links - for each compute normal form if there is such
 and eliminate hiding links.

Flattening heterogeneity - for each heterogeneous link, compute theory of
 a target node and eliminate heterogeneous link.

-}

module Proofs.DGFlattening
  ( dgFlatImports
  , libFlatImports   -- importing
  , dgFlatDUnions
  , libFlatDUnions   -- non-disjoint unions
  , dgFlatRenamings
  , libFlatRenamings -- import with renaming
  , dgFlatHiding
  , libFlatHiding    -- hiding
  , dgFlatHeterogen
  , libFlatHeterogen -- heterogeniety
  , singleTreeFlatDUnions
  ) where

import Common.ExtSign
import Common.Id
import Common.IRI (simpleIdToIRI)
import Common.LibName
import Common.Result

import Comorphisms.LogicGraph

import Logic.Coerce
import Logic.Grothendieck
import Logic.Logic

import Proofs.EdgeUtils
import Proofs.NormalForm

import Static.ComputeTheory
import Static.DevGraph
import Static.DgUtils
import Static.GTheory
import Static.History

import Data.Graph.Inductive.Graph hiding (empty)
import Data.List
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set

mkFlatStr :: String -> DGRule
mkFlatStr :: String -> DGRule
mkFlatStr = String -> DGRule
DGRule (String -> DGRule) -> (String -> String) -> String -> DGRule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("Flat " String -> String -> String
forall a. [a] -> [a] -> [a]
++)

flatImports :: DGRule
flatImports :: DGRule
flatImports = String -> DGRule
mkFlatStr "all imports"

flatNonDisjUnion :: DGRule
flatNonDisjUnion :: DGRule
flatNonDisjUnion = String -> DGRule
mkFlatStr "non-disjoint union"

flatRename :: DGRule
flatRename :: DGRule
flatRename = String -> DGRule
mkFlatStr "renaming"

flatHide :: DGRule
flatHide :: DGRule
flatHide = String -> DGRule
mkFlatStr "hiding"

flatHet :: DGRule
flatHet :: DGRule
flatHet = String -> DGRule
mkFlatStr "heterogeneity"

cErr :: String -> Node -> a
cErr :: String -> Node -> a
cErr str :: String
str n :: Node
n = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ " no global theory for node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
n

-- this function performs flattening of import links
dgFlatImports :: LibEnv -> LibName -> DGraph -> DGraph
dgFlatImports :: LibEnv -> LibName -> DGraph -> DGraph
dgFlatImports libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg = let
  nds :: [Node]
nds = DGraph -> [Node]
nodesDG DGraph
dg
  -- part for dealing with the graph itself
  updLib :: LibEnv
updLib = LibEnv -> LibName -> [Node] -> LibEnv
updateLib LibEnv
libEnv LibName
ln [Node]
nds
  updDG :: DGraph
updDG = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
updLib
  -- it seems changes of the labels are lost and all edges are simply deleted
  n_dg :: DGraph
n_dg = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg ([DGChange] -> DGraph) -> [DGChange] -> DGraph
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> DGChange) -> [LEdge DGLinkLab] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> DGChange
DeleteEdge ([LEdge DGLinkLab] -> [DGChange])
-> [LEdge DGLinkLab] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
updDG
  in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg DGRule
flatImports DGraph
n_dg
  where
   updateNode :: LibEnv -> LibName -> Node -> DGChange
   updateNode :: LibEnv -> LibName -> Node -> DGChange
updateNode lib_Env :: LibEnv
lib_Env l_n :: LibName
l_n n :: Node
n =
    let
     labRf :: DGNodeLab
labRf = DGraph -> Node -> DGNodeLab
labDG (LibName -> LibEnv -> DGraph
lookupDGraph LibName
l_n LibEnv
lib_Env) Node
n
      {- have to consider references here. computeTheory is applied
      to the node at the end of the chain of references only. -}
    in case LibEnv -> LibName -> Node -> Maybe G_theory
computeTheory LibEnv
lib_Env LibName
l_n Node
n of
         Just ndgn_theory :: G_theory
ndgn_theory ->
           DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
labRf (Node
n, DGNodeLab
labRf {dgn_theory :: G_theory
dgn_theory = G_theory
ndgn_theory})
         Nothing ->
           String -> Node -> DGChange
forall a. String -> Node -> a
cErr "dgFlatImports" Node
n
   updateLib :: LibEnv -> LibName -> [Node] -> LibEnv
   updateLib :: LibEnv -> LibName -> [Node] -> LibEnv
updateLib lib_Env :: LibEnv
lib_Env l_n :: LibName
l_n nds :: [Node]
nds =
    case [Node]
nds of
     [] -> LibEnv
lib_Env
     hd :: Node
hd : tl :: [Node]
tl -> let
               change :: DGChange
change = LibEnv -> LibName -> Node -> DGChange
updateNode LibEnv
lib_Env LibName
l_n Node
hd
               ref_dg :: DGraph
ref_dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
l_n LibEnv
lib_Env
               u_dg :: DGraph
u_dg = DGraph -> DGChange -> DGraph
changeDGH DGraph
ref_dg DGChange
change
               new_dg :: DGraph
new_dg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
ref_dg DGRule
flatImports DGraph
u_dg
              in
               LibEnv -> LibName -> [Node] -> LibEnv
updateLib (LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
l_n DGraph
new_dg LibEnv
lib_Env) LibName
l_n [Node]
tl

-- this function performs flattening of imports for the whole library
libFlatImports :: LibEnv -> Result LibEnv
libFlatImports :: LibEnv -> Result LibEnv
libFlatImports lib :: LibEnv
lib = LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv) -> LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ (LibName -> DGraph -> DGraph) -> LibEnv -> LibEnv
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (LibEnv -> LibName -> DGraph -> DGraph
dgFlatImports LibEnv
lib) LibEnv
lib

{- this function performs flattening of imports with renamings
links for a given developement graph -}
dgFlatRenamings :: LibEnv -> LibName -> DGraph -> DGraph
dgFlatRenamings :: LibEnv -> LibName -> DGraph -> DGraph
dgFlatRenamings lib_Env :: LibEnv
lib_Env l_n :: LibName
l_n dg :: DGraph
dg =
  let
   l_edges :: [LEdge DGLinkLab]
l_edges = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg
   renamings :: [LEdge DGLinkLab]
renamings = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, x :: DGLinkLab
x) -> let l_type :: DGEdgeType
l_type = DGLinkLab -> DGEdgeType
getRealDGLinkType DGLinkLab
x in
     case DGEdgeType
l_type of
       DGEdgeType { edgeTypeModInc :: DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc = DGEdgeTypeModInc
GlobalDef, isInc :: DGEdgeType -> Bool
isInc = Bool
False} -> Bool
True
       _ -> Bool
False ) [LEdge DGLinkLab]
l_edges
   fin_dg :: DGraph
fin_dg = [LEdge DGLinkLab] -> DGraph -> DGraph
applyUpdDG [LEdge DGLinkLab]
renamings DGraph
dg
  {- no need to care about references as each node
  is preserved during flattening. -}
  in LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
lib_Env LibName
l_n DGraph
fin_dg
    where
     updateDGWithChanges :: LEdge DGLinkLab -> DGraph -> DGraph
     updateDGWithChanges :: LEdge DGLinkLab -> DGraph -> DGraph
updateDGWithChanges l_edg :: LEdge DGLinkLab
l_edg@( v1 :: Node
v1, v2 :: Node
v2, label :: DGLinkLab
label) d_graph :: DGraph
d_graph =
      let
      -- update nodes
       lv1 :: DGNodeLab
lv1 = DGraph -> Node -> DGNodeLab
labDG DGraph
d_graph Node
v1
       lv2 :: DGNodeLab
lv2 = DGraph -> Node -> DGNodeLab
labDG DGraph
d_graph Node
v2
       name :: NodeName
name = DGNodeLab -> NodeName
dgn_name DGNodeLab
lv1
       n_node :: Node
n_node = DGraph -> Node
getNewNodeDG DGraph
d_graph
       nlv1 :: DGNodeLab
nlv1 = case LibEnv -> LibName -> Node -> Maybe G_theory
computeTheory LibEnv
lib_Env LibName
l_n Node
v1 of
         Just n_dgn_theory :: G_theory
n_dgn_theory -> DGNodeLab
lv1 {dgn_theory :: G_theory
dgn_theory = G_theory
n_dgn_theory }
         Nothing -> String -> Node -> DGNodeLab
forall a. String -> Node -> a
cErr "dgFlatRenamings1" Node
v1
       nlv2 :: DGNodeLab
nlv2 = case LibEnv -> LibName -> Node -> Maybe G_theory
computeTheory LibEnv
lib_Env LibName
l_n Node
v2 of
         Just n_dgn_theory :: G_theory
n_dgn_theory -> DGNodeLab
lv2 {dgn_theory :: G_theory
dgn_theory = G_theory
n_dgn_theory }
         Nothing -> String -> Node -> DGNodeLab
forall a. String -> Node -> a
cErr "dgFlatRenamings2" Node
v2
       n_lnode :: LNode DGNodeLab
n_lnode@(_, n_lv :: DGNodeLab
n_lv) = String -> Result (LNode DGNodeLab) -> LNode DGNodeLab
forall a. String -> Result a -> a
propagateErrors "dgFlatRenamings3" (Result (LNode DGNodeLab) -> LNode DGNodeLab)
-> Result (LNode DGNodeLab) -> LNode DGNodeLab
forall a b. (a -> b) -> a -> b
$ do
             G_theory
t_dgn_theory <- GMorphism -> G_theory -> Result G_theory
translateG_theory (DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
label)
                             (G_theory -> Result G_theory) -> G_theory -> Result G_theory
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
nlv1
             LNode DGNodeLab -> Result (LNode DGNodeLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node
n_node, NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
name
                                     (DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGFlattening)
                                     G_theory
t_dgn_theory)
       -- create edge
       sign_source :: G_sign
sign_source = G_theory -> G_sign
signOf (G_theory -> G_sign) -> G_theory -> G_sign
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
n_lv
       sign_target :: G_sign
sign_target = G_theory -> G_sign
signOf (G_theory -> G_sign) -> G_theory -> G_sign
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
lv2
       n_edg :: Result (LEdge DGLinkLab)
n_edg = do
                 GMorphism
ng_morphism <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
logicGraph G_sign
sign_source G_sign
sign_target
                 LEdge DGLinkLab -> Result (LEdge DGLinkLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node
n_node,
                         Node
v2,
                         DGLinkLab
label { dgl_morphism :: GMorphism
dgl_morphism = GMorphism
ng_morphism,
                                 dgl_type :: DGLinkType
dgl_type = DGLinkType
globalDef ,
                                 dgl_origin :: DGLinkOrigin
dgl_origin = DGLinkOrigin
DGLinkFlatteningRename,
                                 dgl_id :: EdgeId
dgl_id = EdgeId
defaultEdgeId })
       change_dg :: [DGChange]
change_dg = [DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
lv1 (Node
v1, DGNodeLab
nlv1),
                    DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
lv2 (Node
v2, DGNodeLab
nlv2),
                    LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
l_edg,
                    LNode DGNodeLab -> DGChange
InsertNode LNode DGNodeLab
n_lnode,
                    LEdge DGLinkLab -> DGChange
InsertEdge (String -> Result (LEdge DGLinkLab) -> LEdge DGLinkLab
forall a. String -> Result a -> a
propagateErrors "dgFlatRenamings4" Result (LEdge DGLinkLab)
n_edg)]
      in
       DGraph -> [DGChange] -> DGraph
changesDGH DGraph
d_graph [DGChange]
change_dg

     applyUpdDG :: [LEdge DGLinkLab] -> DGraph -> DGraph
     applyUpdDG :: [LEdge DGLinkLab] -> DGraph -> DGraph
applyUpdDG l_list :: [LEdge DGLinkLab]
l_list d_g :: DGraph
d_g = case [LEdge DGLinkLab]
l_list of
      [] -> DGraph
d_g
      hd :: LEdge DGLinkLab
hd : tl :: [LEdge DGLinkLab]
tl -> let
                dev_g :: DGraph
dev_g = LEdge DGLinkLab -> DGraph -> DGraph
updateDGWithChanges LEdge DGLinkLab
hd DGraph
d_g
               in [LEdge DGLinkLab] -> DGraph -> DGraph
applyUpdDG [LEdge DGLinkLab]
tl (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
d_g DGRule
flatRename DGraph
dev_g

-- this function performs flattening of imports with renamings
libFlatRenamings :: LibEnv -> Result LibEnv
libFlatRenamings :: LibEnv -> Result LibEnv
libFlatRenamings lib :: LibEnv
lib = LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv) -> LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ (LibName -> DGraph -> DGraph) -> LibEnv -> LibEnv
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (LibEnv -> LibName -> DGraph -> DGraph
dgFlatRenamings LibEnv
lib) LibEnv
lib

-- this function performs flattening of hiding links
dgFlatHiding :: DGraph -> DGraph
dgFlatHiding :: DGraph -> DGraph
dgFlatHiding dg :: DGraph
dg = let
   hids :: [LEdge DGLinkLab]
hids = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, x :: DGLinkLab
x) -> (case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
x of
                                         HidingDefLink -> Bool
True
                                         _ -> Bool
False)) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg
  {- no need to care about references either, as nodes are preserved
  after flattening, as well as references. -}
   n_dg :: DGraph
n_dg = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg ([DGChange] -> DGraph) -> [DGChange] -> DGraph
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> DGChange) -> [LEdge DGLinkLab] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> DGChange
DeleteEdge [LEdge DGLinkLab]
hids
  in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg DGRule
flatHide DGraph
n_dg

-- this function performs flattening of heterogeniety for the whole library
libFlatHiding :: LibEnv -> Result LibEnv
libFlatHiding :: LibEnv -> Result LibEnv
libFlatHiding = (LibEnv -> LibEnv) -> Result LibEnv -> Result LibEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((DGraph -> DGraph) -> LibEnv -> LibEnv
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map DGraph -> DGraph
dgFlatHiding) (Result LibEnv -> Result LibEnv)
-> (LibEnv -> Result LibEnv) -> LibEnv -> Result LibEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibEnv -> Result LibEnv
normalFormLibEnv

{- this function performs flattening of heterogeniety
for a given developement graph -}
dgFlatHeterogen :: LibEnv -> LibName -> DGraph -> DGraph
dgFlatHeterogen :: LibEnv -> LibName -> DGraph -> DGraph
dgFlatHeterogen libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg = let
  het_comorph :: [LEdge DGLinkLab]
het_comorph = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter
    (\ (_, _, x :: DGLinkLab
x) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GMorphism -> Bool
isHomogeneous (GMorphism -> Bool) -> GMorphism -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
x) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg
  het_del_changes :: [DGChange]
het_del_changes = (LEdge DGLinkLab -> DGChange) -> [LEdge DGLinkLab] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> DGChange
DeleteEdge [LEdge DGLinkLab]
het_comorph
  updLib :: LibEnv
updLib = LibEnv -> LibName -> [(Node, Bool)] -> LibEnv
updateNodes LibEnv
libEnv LibName
ln ([(Node, Bool)] -> LibEnv)
-> ([(Node, Bool)] -> [(Node, Bool)]) -> [(Node, Bool)] -> LibEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Node, Bool) -> [(Node, Bool)]
forall a. Set a -> [a]
Set.toList (Set (Node, Bool) -> [(Node, Bool)])
-> ([(Node, Bool)] -> Set (Node, Bool))
-> [(Node, Bool)]
-> [(Node, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Node, Bool)] -> Set (Node, Bool)
forall a. Ord a => [a] -> Set a
Set.fromList
    ([(Node, Bool)] -> LibEnv) -> [(Node, Bool)] -> LibEnv
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> (Node, Bool))
-> [LEdge DGLinkLab] -> [(Node, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (_, t :: Node
t, l :: DGLinkLab
l) -> (Node
t, DGLinkType -> Bool
isDefEdge (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l)) [LEdge DGLinkLab]
het_comorph
  udg :: DGraph
udg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
updLib
  ndg :: DGraph
ndg = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
udg [DGChange]
het_del_changes
  in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
udg DGRule
flatHet DGraph
ndg
  where
   updateNodes :: LibEnv -> LibName -> [(Node, Bool)] -> LibEnv
   updateNodes :: LibEnv -> LibName -> [(Node, Bool)] -> LibEnv
updateNodes lib_Env :: LibEnv
lib_Env l_n :: LibName
l_n nds :: [(Node, Bool)]
nds = case [(Node, Bool)]
nds of
    [] -> LibEnv
lib_Env
    (hd :: Node
hd, isHetDef :: Bool
isHetDef) : tl :: [(Node, Bool)]
tl -> let
      {- have to consider references here. The global theory is taken as
      local one at the end of the reference chain. -}
      (lname :: LibName
lname, odg :: DGraph
odg, (nd :: Node
nd, labRf :: DGNodeLab
labRf)) =
          LibEnv
-> LibName -> DGraph -> Node -> (LibName, DGraph, LNode DGNodeLab)
lookupRefNode LibEnv
lib_Env LibName
l_n (LibName -> LibEnv -> DGraph
lookupDGraph LibName
l_n LibEnv
lib_Env) Node
hd
      change :: DGChange
change = case DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
labRf of
        Just ndgn_theory :: G_theory
ndgn_theory ->
          DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
labRf (Node
nd, DGNodeLab
labRf {dgn_theory :: G_theory
dgn_theory = G_theory
ndgn_theory})
        Nothing -> String -> Node -> DGChange
forall a. String -> Node -> a
cErr "dgFlatHeterogen" Node
nd
      cdg :: DGraph
cdg = DGraph -> DGChange -> DGraph
changeDGH DGraph
odg DGChange
change
      n_dg :: DGraph
n_dg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
odg DGRule
flatHet DGraph
cdg
     in LibEnv -> LibName -> [(Node, Bool)] -> LibEnv
updateNodes (if Bool
isHetDef then LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
lname DGraph
n_dg LibEnv
lib_Env
                    else LibEnv
lib_Env) LibName
l_n [(Node, Bool)]
tl

-- this function performs flattening of heterogeniety for the whole library
libFlatHeterogen :: LibEnv -> Result LibEnv
libFlatHeterogen :: LibEnv -> Result LibEnv
libFlatHeterogen lib :: LibEnv
lib =
  LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv) -> LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ (LibName -> DGraph -> DGraph) -> LibEnv -> LibEnv
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (LibEnv -> LibName -> DGraph -> DGraph
dgFlatHeterogen LibEnv
lib) LibEnv
lib

{- this function performs flattening of non-disjoint unions for the given
DGraph -}
dgFlatDUnions :: LibEnv -> LibName -> DGraph -> DGraph
dgFlatDUnions :: LibEnv -> LibName -> DGraph -> DGraph
dgFlatDUnions le :: LibEnv
le ln :: LibName
ln dg :: DGraph
dg =
 let
  all_nodes :: [Node]
all_nodes = DGraph -> [Node]
nodesDG DGraph
dg
  imp_nds :: [Node]
imp_nds = (Node -> Bool) -> [Node] -> [Node]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: Node
x -> [LEdge DGLinkLab] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length (DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dg Node
x) Node -> Node -> Bool
forall a. Ord a => a -> a -> Bool
> 1) [Node]
all_nodes
 {- lower_nodes = filter (\ x -> (outDG dg x == [])) (nodesDG dg)
 as previously, no need to care about reference nodes,
 as previous one remain same. -}
 in LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
le LibName
ln (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [Node] -> DGraph
applyToAllNodes DGraph
dg [Node]
imp_nds

-- this funciton given a list og G_sign returns intersection of them
getIntersectionOfAll :: [G_sign] -> G_sign
getIntersectionOfAll :: [G_sign] -> G_sign
getIntersectionOfAll signs :: [G_sign]
signs =
  case [G_sign]
signs of
   [] -> String -> G_sign
forall a. HasCallStack => String -> a
error "getIntersectionOfAll1: empty signatures list"
   [hd :: G_sign
hd] -> G_sign
hd
   G_sign lid1 :: lid
lid1 extSign1 :: ExtSign sign symbol
extSign1 _ : G_sign lid2 :: lid
lid2 (ExtSign signtr2 :: sign
signtr2 _) _ : tl :: [G_sign]
tl -> let
            n_signtr :: G_sign
n_signtr = String -> Result G_sign -> G_sign
forall a. String -> Result a -> a
propagateErrors "getIntersectionOfAll2" (Result G_sign -> G_sign) -> Result G_sign -> G_sign
forall a b. (a -> b) -> a -> b
$ do
               ExtSign sign1 :: sign
sign1 _ <- lid
-> lid
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid1
                                               lid
lid2
                                               "getIntersectionOfAll"
                                               ExtSign sign symbol
extSign1
               sign
n_sign <- lid -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
intersection lid
lid2 sign
sign1 sign
signtr2
               G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> Result G_sign) -> G_sign -> Result G_sign
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid
lid2 (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
n_sign) SigId
startSigId
           in
            if G_sign
n_signtr G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== AnyLogic -> G_sign
emptyG_sign (lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
lid2) then G_sign
n_signtr
            else [G_sign] -> G_sign
getIntersectionOfAll (G_sign
n_signtr G_sign -> [G_sign] -> [G_sign]
forall a. a -> [a] -> [a]
: [G_sign]
tl)

{- this function given a list of all possible combinations of nodes
of a given length -}
getAllCombinations :: Int -> [Node] -> [[Node]]
getAllCombinations :: Node -> [Node] -> [[Node]]
getAllCombinations 0 _ = [ [] ]
getAllCombinations n :: Node
n xs :: [Node]
xs = [ Node
y Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
ys | y :: Node
y : xs' :: [Node]
xs' <- [Node] -> [[Node]]
forall a. [a] -> [[a]]
tails [Node]
xs
                           , [Node]
ys <- Node -> [Node] -> [[Node]]
getAllCombinations (Node
n Node -> Node -> Node
forall a. Num a => a -> a -> a
- 1) [Node]
xs']

-- tells if two lists are equal or one contained in the other
containedInList :: [Node] -> [Node] -> Bool
containedInList :: [Node] -> [Node] -> Bool
containedInList l1 :: [Node]
l1 l2 :: [Node]
l2 = (Node -> Bool) -> [Node] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node]
l2) [Node]
l1

-- attach new nodes to the level
attachNewNodes :: [([Node], G_sign)] -> Int -> [([Node], Node, G_sign)]
attachNewNodes :: [([Node], G_sign)] -> Node -> [([Node], Node, G_sign)]
attachNewNodes [] _ = []
attachNewNodes ((hd :: [Node]
hd, sg :: G_sign
sg) : tl :: [([Node], G_sign)]
tl) n :: Node
n = ([Node]
hd, Node
n, G_sign
sg) ([Node], Node, G_sign)
-> [([Node], Node, G_sign)] -> [([Node], Node, G_sign)]
forall a. a -> [a] -> [a]
: [([Node], G_sign)] -> Node -> [([Node], Node, G_sign)]
attachNewNodes [([Node], G_sign)]
tl (Node
n Node -> Node -> Node
forall a. Num a => a -> a -> a
+ 1)

 -- search for a match for a given combination in a level
searchForMatch :: [Node] -> [([Node], Node, G_sign)]
               -> Maybe ([Node], Node, G_sign)
searchForMatch :: [Node] -> [([Node], Node, G_sign)] -> Maybe ([Node], Node, G_sign)
searchForMatch _ [] = Maybe ([Node], Node, G_sign)
forall a. Maybe a
Nothing
searchForMatch l :: [Node]
l (tripl :: ([Node], Node, G_sign)
tripl@(nds :: [Node]
nds, _, _) : tl :: [([Node], Node, G_sign)]
tl) =
  if [Node] -> [Node] -> Bool
containedInList [Node]
l [Node]
nds then ([Node], Node, G_sign) -> Maybe ([Node], Node, G_sign)
forall a. a -> Maybe a
Just ([Node], Node, G_sign)
tripl else [Node] -> [([Node], Node, G_sign)] -> Maybe ([Node], Node, G_sign)
searchForMatch [Node]
l [([Node], Node, G_sign)]
tl

 {- take a combination of nodes, previous level,
 and get the signature for the next level -}
matchCombinations :: [Node] -> [([Node], Node, G_sign)]
                  -> Maybe ([Node], G_sign)
matchCombinations :: [Node] -> [([Node], Node, G_sign)] -> Maybe ([Node], G_sign)
matchCombinations [] _ = Maybe ([Node], G_sign)
forall a. Maybe a
Nothing
matchCombinations ([_]) _ = Maybe ([Node], G_sign)
forall a. Maybe a
Nothing
matchCombinations l :: [Node]
l@(hd1 :: Node
hd1 : hd2 :: Node
hd2 : tl :: [Node]
tl) trpls :: [([Node], Node, G_sign)]
trpls =
  case [Node] -> [([Node], Node, G_sign)] -> Maybe ([Node], Node, G_sign)
searchForMatch (Node
hd1 Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
tl) [([Node], Node, G_sign)]
trpls of
   Nothing -> Maybe ([Node], G_sign)
forall a. Maybe a
Nothing
   Just (_, _, gsig1 :: G_sign
gsig1@(G_sign lid :: lid
lid _ _)) ->
     case [Node] -> [([Node], Node, G_sign)] -> Maybe ([Node], Node, G_sign)
searchForMatch (Node
hd2 Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
tl) [([Node], Node, G_sign)]
trpls of
         Nothing -> Maybe ([Node], G_sign)
forall a. Maybe a
Nothing
         Just (_, _, gsig2 :: G_sign
gsig2) ->
            let
             n_sig :: G_sign
n_sig = [G_sign] -> G_sign
getIntersectionOfAll [G_sign
gsig1, G_sign
gsig2]
            in
             if G_sign
n_sig G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== AnyLogic -> G_sign
emptyG_sign (lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
lid) then Maybe ([Node], G_sign)
forall a. Maybe a
Nothing
             else ([Node], G_sign) -> Maybe ([Node], G_sign)
forall a. a -> Maybe a
Just ([Node]
l, G_sign
n_sig)

 -- for a dg and a level, create labels for the new nodes
createLabels :: DGraph -> [([Node], Node, G_sign)] -> [LNode DGNodeLab]
createLabels :: DGraph -> [([Node], Node, G_sign)] -> [LNode DGNodeLab]
createLabels dg :: DGraph
dg tripls :: [([Node], Node, G_sign)]
tripls = case [([Node], Node, G_sign)]
tripls of
  [] -> String -> [LNode DGNodeLab]
forall a. HasCallStack => String -> a
error "createLabels: empty list on input"
  _ -> let
        labels :: [LNode DGNodeLab]
labels = (([Node], Node, G_sign) -> LNode DGNodeLab)
-> [([Node], Node, G_sign)] -> [LNode DGNodeLab]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: [Node]
x, y :: Node
y, G_sign lid :: lid
lid (ExtSign sign :: sign
sign symb :: Set symbol
symb) ind :: SigId
ind) -> let
             -- name intersection by interspersing a string for a SimpleId
             s_id :: Token
s_id = String -> Token
mkSimpleId (String -> Token) -> ([String] -> String) -> [String] -> Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "'"
               ([String] -> Token) -> [String] -> Token
forall a b. (a -> b) -> a -> b
$ (Node -> String) -> [Node] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Node -> DGraph -> String
`getNameOfNode` DGraph
dg) [Node]
x
             n_theory :: G_theory
n_theory = lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid (sign -> Set symbol -> ExtSign sign symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign
sign Set symbol
symb) SigId
ind
             n_name :: NodeName
n_name = IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ Token -> IRI
simpleIdToIRI Token
s_id
             n_info :: DGNodeInfo
n_info = DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGFlattening
            in
             (Node
y, NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
n_name DGNodeInfo
n_info G_theory
n_theory)) [([Node], Node, G_sign)]
tripls
       in [LNode DGNodeLab]
labels

-- create links connecting given node with a list of nodes
createLinks :: DGraph -> LNode DGNodeLab -> [Node] -> DGraph
createLinks :: DGraph -> LNode DGNodeLab -> [Node] -> DGraph
createLinks dg :: DGraph
dg _ [] = DGraph
dg
createLinks dg :: DGraph
dg (nd :: Node
nd, lb :: DGNodeLab
lb) (hd :: Node
hd : tl :: [Node]
tl) =
  let
   sign_source :: G_sign
sign_source = G_theory -> G_sign
signOf (DGNodeLab -> G_theory
dgn_theory DGNodeLab
lb)
   sign_target :: G_sign
sign_target = G_theory -> G_sign
signOf (DGNodeLab -> G_theory
dgn_theory (DGNodeLab -> G_theory) -> DGNodeLab -> G_theory
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
hd)
   n_edg :: LEdge DGLinkLab
n_edg = String -> Result (LEdge DGLinkLab) -> LEdge DGLinkLab
forall a. String -> Result a -> a
propagateErrors "DGFlattening.createLinks" (Result (LEdge DGLinkLab) -> LEdge DGLinkLab)
-> Result (LEdge DGLinkLab) -> LEdge DGLinkLab
forall a b. (a -> b) -> a -> b
$ do
      GMorphism
ng_morphism <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
logicGraph G_sign
sign_source G_sign
sign_target
      LEdge DGLinkLab -> Result (LEdge DGLinkLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node
nd, Node
hd, GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
ng_morphism DGLinkOrigin
DGLinkFlatteningUnion)
   u_dg :: DGraph
u_dg = case LEdge DGLinkLab -> DGraph -> Maybe (LEdge DGLinkLab)
tryToGetEdge LEdge DGLinkLab
n_edg DGraph
dg of
            Nothing -> DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
n_edg
            Just _ -> DGraph
dg
   n_dg :: DGraph
n_dg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg DGRule
flatNonDisjUnion DGraph
u_dg
  in
   DGraph -> LNode DGNodeLab -> [Node] -> DGraph
createLinks DGraph
n_dg (Node
nd, DGNodeLab
lb) [Node]
tl

{- given an element in the level and a lower link, function searches
elements in the given level, which are suitable for inserting a link
connecting given element. -}
searchForLink :: ([Node], Node, G_sign) -> [([Node], Node, G_sign)] -> [Node]
searchForLink :: ([Node], Node, G_sign) -> [([Node], Node, G_sign)] -> [Node]
searchForLink el :: ([Node], Node, G_sign)
el@(nds1 :: [Node]
nds1, _, _) down_level :: [([Node], Node, G_sign)]
down_level = case [([Node], Node, G_sign)]
down_level of
  [] -> []
  (nds2 :: [Node]
nds2, nd2 :: Node
nd2, _) : tl :: [([Node], Node, G_sign)]
tl -> [ Node
nd2 | [Node] -> [Node] -> Bool
containedInList [Node]
nds2 [Node]
nds1 ]
                         [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ ([Node], Node, G_sign) -> [([Node], Node, G_sign)] -> [Node]
searchForLink ([Node], Node, G_sign)
el [([Node], Node, G_sign)]
tl

{- given two levels of the graph, insert links between them, so that the
signatures are imported properly -}
linkLevels :: DGraph -> [([Node], Node, G_sign)] -> [([Node], Node, G_sign)]
           -> DGraph
linkLevels :: DGraph
-> [([Node], Node, G_sign)] -> [([Node], Node, G_sign)] -> DGraph
linkLevels dg :: DGraph
dg up_level :: [([Node], Node, G_sign)]
up_level down_level :: [([Node], Node, G_sign)]
down_level = case [([Node], Node, G_sign)]
up_level of
  [] -> DGraph
dg
  hd :: ([Node], Node, G_sign)
hd@(_, nd :: Node
nd, _) : tl :: [([Node], Node, G_sign)]
tl -> let
            nds :: [Node]
nds = ([Node], Node, G_sign) -> [([Node], Node, G_sign)] -> [Node]
searchForLink ([Node], Node, G_sign)
hd [([Node], Node, G_sign)]
down_level
            label :: DGNodeLab
label = DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
nd
            n_dg :: DGraph
n_dg = DGraph -> LNode DGNodeLab -> [Node] -> DGraph
createLinks DGraph
dg (Node
nd, DGNodeLab
label) [Node]
nds
           in
            DGraph
-> [([Node], Node, G_sign)] -> [([Node], Node, G_sign)] -> DGraph
linkLevels DGraph
n_dg [([Node], Node, G_sign)]
tl [([Node], Node, G_sign)]
down_level

{- given a list of the lower nodes, gives a DGraph with a first level
of nodes inserted in this graph -}
createFirstLevel :: DGraph -> [Node] -> (DGraph, [([Node], Node, G_sign)])
createFirstLevel :: DGraph -> [Node] -> (DGraph, [([Node], Node, G_sign)])
createFirstLevel dg :: DGraph
dg nds :: [Node]
nds =
  let
   combs :: [[Node]]
combs = Node -> [Node] -> [[Node]]
getAllCombinations 2 [Node]
nds
   init_level :: [([Node], G_sign)]
init_level = ([Node] -> ([Node], G_sign)) -> [[Node]] -> [([Node], G_sign)]
forall a b. (a -> b) -> [a] -> [b]
map (\ l :: [Node]
l -> let
                         [x :: Node
x, y :: Node
y] = [Node]
l
                         signx :: G_sign
signx = G_theory -> G_sign
signOf (G_theory -> G_sign) -> G_theory -> G_sign
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory (DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
x)
                         signy :: G_sign
signy = G_theory -> G_sign
signOf (G_theory -> G_sign) -> G_theory -> G_sign
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory (DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
y)
                         n_sign :: G_sign
n_sign = [G_sign] -> G_sign
getIntersectionOfAll [G_sign
signx, G_sign
signy]
                         in ([Node]
l, G_sign
n_sign)) [[Node]]
combs
   n_empty :: [([Node], G_sign)]
n_empty = (([Node], G_sign) -> Bool)
-> [([Node], G_sign)] -> [([Node], G_sign)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, sign :: G_sign
sign@(G_sign lid :: lid
lid _ _)) ->
                               G_sign
sign G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
/= AnyLogic -> G_sign
emptyG_sign (lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
lid)) [([Node], G_sign)]
init_level
  in
   case [([Node], G_sign)] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [([Node], G_sign)]
n_empty of
    0 -> (DGraph
dg, [])
    _ -> let
          atch_level :: [([Node], Node, G_sign)]
atch_level = [([Node], G_sign)] -> Node -> [([Node], Node, G_sign)]
attachNewNodes [([Node], G_sign)]
n_empty (DGraph -> Node
getNewNodeDG DGraph
dg)
          labels :: [LNode DGNodeLab]
labels = DGraph -> [([Node], Node, G_sign)] -> [LNode DGNodeLab]
createLabels DGraph
dg [([Node], Node, G_sign)]
atch_level
          changes :: [DGChange]
changes = (LNode DGNodeLab -> DGChange) -> [LNode DGNodeLab] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map LNode DGNodeLab -> DGChange
InsertNode [LNode DGNodeLab]
labels
          u_dg :: DGraph
u_dg = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
changes
          n_dg :: DGraph
n_dg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg DGRule
flatNonDisjUnion DGraph
u_dg
          zero_level :: [([Node], Node, G_sign)]
zero_level = (Node -> ([Node], Node, G_sign))
-> [Node] -> [([Node], Node, G_sign)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: Node
x ->
                        ([Node
x], Node
x, G_theory -> G_sign
signOf (G_theory -> G_sign) -> G_theory -> G_sign
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory (DGraph -> Node -> DGNodeLab
labDG DGraph
n_dg Node
x))) [Node]
nds
          lnk_dg :: DGraph
lnk_dg = DGraph
-> [([Node], Node, G_sign)] -> [([Node], Node, G_sign)] -> DGraph
linkLevels DGraph
n_dg [([Node], Node, G_sign)]
atch_level [([Node], Node, G_sign)]
zero_level
         in
          (DGraph
lnk_dg, [([Node], Node, G_sign)]
atch_level)

{- given a level of nodes and a graph, constructs upper level,
inserting the nodes of the new level to the DGraph -}
createNewLevel :: DGraph -> [Node] -> [([Node], Node, G_sign)]
               -> (DGraph, [([Node], Node, G_sign)])
createNewLevel :: DGraph
-> [Node]
-> [([Node], Node, G_sign)]
-> (DGraph, [([Node], Node, G_sign)])
createNewLevel c_dg :: DGraph
c_dg nds :: [Node]
nds tripls :: [([Node], Node, G_sign)]
tripls = case [([Node], Node, G_sign)]
tripls of
  [] -> (DGraph
c_dg, [])
  [_] -> (DGraph
c_dg, [([Node], Node, G_sign)]
tripls)
  (nd_s :: [Node]
nd_s, _, _) : _ -> if [Node] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [Node]
nd_s Node -> Node -> Node
forall a. Num a => a -> a -> a
- [Node] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [Node]
nds Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then (DGraph
c_dg, [])
    else let
     combs :: [[Node]]
combs = Node -> [Node] -> [[Node]]
getAllCombinations ([Node] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [Node]
nd_s Node -> Node -> Node
forall a. Num a => a -> a -> a
+ 1) [Node]
nds
     n_level :: [([Node], G_sign)]
n_level = ([Node] -> Maybe ([Node], G_sign))
-> [[Node]] -> [([Node], G_sign)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([Node] -> [([Node], Node, G_sign)] -> Maybe ([Node], G_sign)
`matchCombinations` [([Node], Node, G_sign)]
tripls) [[Node]]
combs
    in if [([Node], G_sign)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Node], G_sign)]
n_level then (DGraph
c_dg, []) else
           let
            atch_level :: [([Node], Node, G_sign)]
atch_level = [([Node], G_sign)] -> Node -> [([Node], Node, G_sign)]
attachNewNodes [([Node], G_sign)]
n_level (DGraph -> Node
getNewNodeDG DGraph
c_dg)
            labels :: [LNode DGNodeLab]
labels = DGraph -> [([Node], Node, G_sign)] -> [LNode DGNodeLab]
createLabels DGraph
c_dg [([Node], Node, G_sign)]
atch_level
            chngs :: [DGChange]
chngs = (LNode DGNodeLab -> DGChange) -> [LNode DGNodeLab] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map LNode DGNodeLab -> DGChange
InsertNode [LNode DGNodeLab]
labels
            u_dg :: DGraph
u_dg = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
c_dg [DGChange]
chngs
            n_dg :: DGraph
n_dg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
c_dg DGRule
flatNonDisjUnion DGraph
u_dg
            lnk_dg :: DGraph
lnk_dg = DGraph
-> [([Node], Node, G_sign)] -> [([Node], Node, G_sign)] -> DGraph
linkLevels DGraph
n_dg [([Node], Node, G_sign)]
atch_level [([Node], Node, G_sign)]
tripls
           in
            (DGraph
lnk_dg, [([Node], Node, G_sign)]
atch_level)

 {- iterate the procedure for all levels
 (the level passed is already inserted in the graph) -}
iterateForAllLevels :: DGraph -> [Node] -> [([Node], Node, G_sign)] -> DGraph
iterateForAllLevels :: DGraph -> [Node] -> [([Node], Node, G_sign)] -> DGraph
iterateForAllLevels i_dg :: DGraph
i_dg nds :: [Node]
nds init_level :: [([Node], Node, G_sign)]
init_level =
  if [([Node], Node, G_sign)] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [([Node], Node, G_sign)]
init_level Node -> Node -> Bool
forall a. Ord a => a -> a -> Bool
< 2 then DGraph
i_dg else
   let (n_dg :: DGraph
n_dg, n_level :: [([Node], Node, G_sign)]
n_level) = DGraph
-> [Node]
-> [([Node], Node, G_sign)]
-> (DGraph, [([Node], Node, G_sign)])
createNewLevel DGraph
i_dg [Node]
nds [([Node], Node, G_sign)]
init_level
   in if [([Node], Node, G_sign)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Node], Node, G_sign)]
n_level then DGraph
n_dg else
         DGraph -> [Node] -> [([Node], Node, G_sign)] -> DGraph
iterateForAllLevels DGraph
n_dg [Node]
nds [([Node], Node, G_sign)]
n_level

-- applies itteration for all the nodes in the graph
applyToAllNodes :: DGraph -> [Node] -> DGraph
applyToAllNodes :: DGraph -> [Node] -> DGraph
applyToAllNodes a_dg :: DGraph
a_dg nds :: [Node]
nds = case [Node]
nds of
 [] -> DGraph
a_dg
 hd :: Node
hd : tl :: [Node]
tl -> let
            inc_nds :: [Node]
inc_nds = (LEdge DGLinkLab -> Node) -> [LEdge DGLinkLab] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Node
x, _, _) -> Node
x) (DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
a_dg Node
hd)
            (init_dg :: DGraph
init_dg, init_level :: [([Node], Node, G_sign)]
init_level) = DGraph -> [Node] -> (DGraph, [([Node], Node, G_sign)])
createFirstLevel DGraph
a_dg [Node]
inc_nds
            final_dg :: DGraph
final_dg = DGraph -> [Node] -> [([Node], Node, G_sign)] -> DGraph
iterateForAllLevels DGraph
init_dg [Node]
inc_nds [([Node], Node, G_sign)]
init_level
           in
            DGraph -> [Node] -> DGraph
applyToAllNodes DGraph
final_dg [Node]
tl
{- given a lower level of nodes, gives upper level of nodes,
which are ingoing nodes for the lower level -}
filterIngoing :: DGraph -> [Node] -> [Node]
filterIngoing :: DGraph -> [Node] -> [Node]
filterIngoing dg :: DGraph
dg nds :: [Node]
nds = case [Node]
nds of
  [] -> []
  hd :: Node
hd : tl :: [Node]
tl -> let ind :: [Node]
ind = (LEdge DGLinkLab -> Node) -> [LEdge DGLinkLab] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Node
x, _, _) -> Node
x) (DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dg Node
hd) in
             [Node]
ind [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ DGraph -> [Node] -> [Node]
filterIngoing DGraph
dg ([Node]
ind [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
tl)

{- this function takes a node and performs flattening
of non-disjoint unions for the ingoing tree of nodes to the given node -}
singleTreeFlatDUnions :: LibEnv -> LibName -> Node -> Result LibEnv
singleTreeFlatDUnions :: LibEnv -> LibName -> Node -> Result LibEnv
singleTreeFlatDUnions libEnv :: LibEnv
libEnv libName :: LibName
libName nd :: Node
nd = let
  dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
libName LibEnv
libEnv
  in_nds :: [Node]
in_nds = DGraph -> [Node] -> [Node]
filterIngoing DGraph
dg [Node
nd]
  n_dg :: DGraph
n_dg = DGraph -> [Node] -> DGraph
applyToAllNodes DGraph
dg [Node]
in_nds
  in LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv) -> LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
libName DGraph
n_dg LibEnv
libEnv

{- this functions performs flattening of
non-disjoint unions for the whole library -}
libFlatDUnions :: LibEnv -> Result LibEnv
libFlatDUnions :: LibEnv -> Result LibEnv
libFlatDUnions le :: LibEnv
le = LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv) -> LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ (LibName -> DGraph -> DGraph) -> LibEnv -> LibEnv
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\ln :: LibName
ln dg :: DGraph
dg -> LibEnv -> LibName -> DGraph -> DGraph
dgFlatDUnions LibEnv
le LibName
ln DGraph
dg) LibEnv
le