Provided functions to retrieve proven and required consistency

HetsAPI/Internal.hs

@@ -11,6 +11,9 @@ module HetsAPI.Internal (
     , ConsistencyStatus
     , sType
     , ConsStatus
+    , requiredConservativity
+    , provenConservativity
+    , linkStatus
     , Conservativity
     , getNodeConsStatus
     , getConsOfStatus
@@ -26,7 +29,7 @@ import Common.Result (Result, resultToMaybe, Diagnosis)
 import Common.Consistency(Conservativity(..), showConsistencyStatus)
 import Driver.Options (HetcatsOpts, defaultHetcatsOpts)
 import Static.DevGraph (DGraph, DGNodeLab(..), getNodeConsStatus, getNodeCons)
-import Static.DgUtils (ConsStatus, getConsOfStatus, isProvenConsStatusLink)
+import Static.DgUtils (ConsStatus(..), getConsOfStatus, isProvenConsStatusLink)
 import Logic.Prover (ProofStatus, GoalStatus, TacticScript)
 import Proofs.AbstractState (ProofState)
 import Proofs.ConsistencyCheck (ConsistencyStatus(..))

Static/DgUtils.hs

@@ -212,7 +212,11 @@ fcList :: [FreeOrCofree]
 fcList = [minBound .. maxBound]
 
 -- | required and proven conservativity (with a proof)
-data ConsStatus = ConsStatus Conservativity Conservativity ThmLinkStatus
+data ConsStatus = ConsStatus
+  { requiredConservativity :: Conservativity,
+    provenConservativity :: Conservativity,
+    linkStatus :: ThmLinkStatus
+  }
   deriving (Show, Eq, Ord, Typeable, Data)
 
 isProvenConsStatusLink :: ConsStatus -> Bool

python/hets/ConsistencyStatus.py

@@ -5,9 +5,14 @@ class ConsistencyStatus:
     def __init__(self, hsConsStatus: ConsStatus):
         self._hsConsStatus = hsConsStatus
 
-    def consistency(self) -> str:
-        hsCons = self._hsConsStatus.getConsOfStatus()
+    def required(self) -> str:
+        hsCons = self._hsConsStatus.requiredConservativity()
         return showConsistencyStatus(hsCons)
 
+    def proven(self) -> str:
+        hsCons = self._hsConsStatus.provenConservativity()
+        return showConsistencyStatus(hsCons)
+
+
     def isProvenLink(self) -> bool:
-        return self._hsConsStatus.isProvenConsStatusLink()
+        return self._hsConsStatus.isProvenConsStatusLink()

python/hets/DevGraphNode.py

@@ -35,7 +35,6 @@ def label(self):
     def name(self):
         return self.label().dgn_name()
 
-    # TODO Move prove and consistency from theory
     def _theoryPointer(self) -> TheoryPointer:
         node = self.hsObj()
         graph = self.parent().hsObj()
@@ -104,19 +103,12 @@ def checkConsistency(self,
         return ccResult
 
 
-    # TODO Add consistency result
     def consistencyStatus(self) -> ConsistencyStatus:
         nodeLab = snd(self._hsNode)
         hsConsStatus = nodeLab.getNodeConsStatus()
         return ConsistencyStatus(hsConsStatus)
 
-        # TODO return both Conservativity Conservativity
-
-    # TODO after proving/consistency call recomputeNodeLabel
-
     def globalTheory(self) -> Optional[Theory]:
-        # TODO: call computeTheory
-        # l.getDevelopmentGraph().nodes()[10].globalTheory().sentences() != []
         nodeLab = snd(self._hsNode)
 
         pyTheoryM = getGlobalTheory(nodeLab)

python/hets/haskell/__init__.py

@@ -20,6 +20,7 @@
 from hs.HetsAPI.Internal import (fromJust, Result, resultToMaybe, Diagnosis, HetcatsOpts, defaultHetcatsOpts, DGraph,
                                  DGNodeLab, ProofStatus, ProofState, ConsistencyStatus, dgn_name, ConsistencyStatus,
                                  ConsStatus, Conservativity, getNodeConsStatus, showConsistencyStatus, GoalStatus,
-                                 TimeOfDay, TacticScript, getConsOfStatus)
+                                 TimeOfDay, TacticScript, getConsOfStatus, requiredConservativity, provenConservativity,
+                                 linkStatus)
 
 import hs.Common.OrderedMap as OMap

python/hets/haskell/__init__.pyi

@@ -44,10 +44,12 @@ def resultToMaybe(r: Result[A]) -> Maybe[A]: ...
 class Conservativity: ...
 
 class ConsStatus:
-    def getConsOfStatus(self) -> Conservativity: ...
-
     def isProvenConsStatusLink(self) -> bool: ...
 
+    def requiredConservativity(self) -> Conservativity: ...
+
+    def provenConservativity(self) -> Conservativity: ...
+
     ...
 
 def showConsistencyStatus(c: Conservativity) -> str: ...
@@ -312,4 +314,4 @@ def qualifyLibEnv(name: LibName, env: LibEnv) -> LibEnv: ...
 
 def getGlobalTheory(node: DGNodeLab) -> PyTheory: ...
 
-def recomputeNode(thPtr: TheoryPointer) -> LibEnv: ...
+def recomputeNode(thPtr: TheoryPointer) -> LibEnv: ...