From f8941f22d8a227698fa4b38a26db7d920f7cb78b Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Fri, 24 Mar 2017 08:08:03 +0100
Subject: [PATCH 1/2] started adding the datatypes

---
 Common/Consistency.hs |  2 ++
 Static/DevGraph.hs    | 27 +++++++++++++++++++++++++++
 Static/DgUtils.hs     |  2 +-
 Static/GTheory.hs     | 11 +++++++++++
 4 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/Common/Consistency.hs b/Common/Consistency.hs
index 49486e786d..fef3e43a1b 100644
--- a/Common/Consistency.hs
+++ b/Common/Consistency.hs
@@ -31,6 +31,7 @@ data Conservativity =
   | PCons
   | Cons
   | Mono
+  | WDef
   | Def
     deriving (Show, Read, Eq, Ord, Typeable, Data)
 
@@ -42,6 +43,7 @@ showConsistencyStatus cs = case cs of
   Cons -> "conservative"
   PCons -> "proof-theoretically conservative"
   Mono -> "monomorphic"
+  WDef -> "weak definitional"
   Def -> "definitional"
 
 instance Pretty Conservativity where
diff --git a/Static/DevGraph.hs b/Static/DevGraph.hs
index 64f8b66c18..d6cd603da5 100644
--- a/Static/DevGraph.hs
+++ b/Static/DevGraph.hs
@@ -672,10 +672,37 @@ refSigComposition (ComponentRefSig n1 rsmap1) (ComponentRefSig n2 rsmap2) = do
 refSigComposition _rsig1 _rsig2 =
   fail "composition of refinement signatures"
 
+-- | signature of modules
+
+data ModuleSig = ModuleSig NodeSig NodeSig
+  deriving (Show, Typeable)
+  -- the first NodeSig is the node of the module
+  -- the second is the one of the original ontology
+  -- this determines uniquely the edge between them
+  -- labeled with the inclusion
+
+-- | signature of equivalences
+
+data EquivSig = EquivSig GDiagram GDiagram GDiagram
+ deriving (Show, Typeable)
+
+ -- we use the type GDiagram to store graphs
+ -- we have just one datatype for all types of equivalences
+ -- the ontologies in semantics of OMS equivalences
+ -- can be regarded as a graph with one node and no edges
+
+-- | signature of entailments
+
+data EntailSig = EntailSig GDiagram
+ deriving (Show, Typeable)
+
 -- | an entry of the global environment
 data GlobalEntry =
     SpecEntry ExtGenSig
   | ViewOrStructEntry Bool ExtViewSig
+  | ModuleEntry ModuleSig
+  | EntailmentEntry EntailSig
+  | EquivalenceEntry EquivSig
   | ArchOrRefEntry Bool RefSig
   | AlignEntry AlignSig
   | UnitEntry UnitSig
diff --git a/Static/DgUtils.hs b/Static/DgUtils.hs
index 46736deae7..e1aee3a35f 100644
--- a/Static/DgUtils.hs
+++ b/Static/DgUtils.hs
@@ -204,7 +204,7 @@ data Scope = Local | Global deriving (Show, Eq, Ord, Typeable, Data)
 data LinkKind = DefLink | ThmLink ThmLinkStatus
   deriving (Show, Eq, Ord, Typeable, Data)
 
-data FreeOrCofree = Free | Cofree | NPFree | Minimize
+data FreeOrCofree = Free | Cofree | NPFree | Minimize | Maximize
   deriving (Show, Eq, Ord, Enum, Bounded, Read, Typeable, Data)
 
 fcList :: [FreeOrCofree]
diff --git a/Static/GTheory.hs b/Static/GTheory.hs
index 9aa14f6d8a..35aab446e4 100644
--- a/Static/GTheory.hs
+++ b/Static/GTheory.hs
@@ -339,6 +339,17 @@ propagateProofs locTh@(G_theory lid1 syn sig ind lsens _)
 -- | Grothendieck diagrams
 type GDiagram = Gr G_theory (Int, GMorphism)
 
+-- | Morphisms between networks
+
+data DistributedMorphism = 
+   DistributedMorphism {
+    sourceNetwork :: GDiagram,
+    targetNetwork :: GDiagram,
+    graphMorphism :: Map.Map (Node, Node) GMorphism
+   }
+
+-- static analysis should check naturality condition
+
 -- | checks whether a connected GDiagram is homogeneous
 
 isHomogeneousGDiagram :: GDiagram -> Bool

From 0e1563181be6261480041a54a3fea125d5479094 Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Fri, 24 Mar 2017 08:27:49 +0100
Subject: [PATCH 2/2] new approximation links

---
 Static/DevGraph.hs | 4 ++++
 Static/DgUtils.hs  | 1 +
 Static/DotGraph.hs | 1 +
 3 files changed, 6 insertions(+)

diff --git a/Static/DevGraph.hs b/Static/DevGraph.hs
index d6cd603da5..e2fd6fd9b0 100644
--- a/Static/DevGraph.hs
+++ b/Static/DevGraph.hs
@@ -273,6 +273,9 @@ data DGLinkOrigin =
 data DGLinkType =
     ScopedLink Scope LinkKind ConsStatus
   | HidingDefLink
+  | ApproxLink 
+      -- same as hiding definition link, but needs to be treated differently 
+      -- e.g. when computing theories
   | FreeOrCofreeDefLink FreeOrCofree MaybeNode -- the "parameter" node
   | HidingFreeOrCofreeThm (Maybe FreeOrCofree) Node GMorphism ThmLinkStatus
     {- DGLink S1 S2 m2 (DGLinkType m1 p) n
@@ -353,6 +356,7 @@ getHomEdgeType isPend isHom lt = case lt of
             , isConservativ = isProvenConsStatusLink cons
             , isPending = isPend } -- needs to be checked
       HidingDefLink -> HidingDef
+      ApproxLink -> ApproxDef
       FreeOrCofreeDefLink fc _ -> FreeOrCofreeDef fc
       HidingFreeOrCofreeThm mh _ _ st -> ThmType
         { thmEdgeType = case mh of
diff --git a/Static/DgUtils.hs b/Static/DgUtils.hs
index e1aee3a35f..87ebd5623d 100644
--- a/Static/DgUtils.hs
+++ b/Static/DgUtils.hs
@@ -265,6 +265,7 @@ data DGEdgeTypeModInc =
     GlobalDef
   | HetDef
   | HidingDef
+  | ApproxDef
   | LocalDef
   | FreeOrCofreeDef FreeOrCofree
   | ThmType { thmEdgeType :: ThmTypes
diff --git a/Static/DotGraph.hs b/Static/DotGraph.hs
index 45ee854178..9e1d8f7f86 100644
--- a/Static/DotGraph.hs
+++ b/Static/DotGraph.hs
@@ -25,6 +25,7 @@ edgeAttributes ety = concatMap (", " ++)
     GlobalDef -> []
     HetDef -> ["color=" ++ doubleColor "black"]
     HidingDef -> ["color=blue"]
+    ApproxDef -> ["color=orange"] -- should think of something else here
     LocalDef -> ["style=dashed"]
     FreeOrCofreeDef _ -> ["color=blue"]
     ThmType