1693 datatypes for dol

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

Static/DevGraph.hs

@@ -275,6 +275,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
@@ -355,6 +358,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
@@ -679,10 +683,37 @@ refSigComposition (ComponentRefSig n1 rsmap1) (ComponentRefSig n2 rsmap2) = do
 refSigComposition _rsig1 _rsig2 =
   Fail.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

Static/DgUtils.hs

@@ -205,7 +205,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]
@@ -270,6 +270,7 @@ data DGEdgeTypeModInc =
     GlobalDef
   | HetDef
   | HidingDef
+  | ApproxDef
   | LocalDef
   | FreeOrCofreeDef FreeOrCofree
   | ThmType { thmEdgeType :: ThmTypes

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

Static/GTheory.hs

@@ -345,6 +345,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