{-# LANGUAGE ScopedTypeVariables #-}
{- |
Description :  Commands providing information about the state of the development graph and selected theories
Copyright   :  (c) Otto-von-Guericke University of Magdeburg
License     :  GPLv2 or higher, see LICENSE.txt
-}


module HetsAPI.InfoCommands (
     getGraphForLibrary
   , getNodesFromDevelopmentGraph
   , getLNodesFromDevelopmentGraph
   , getEdgesFromDevelopmentGraph
   , getLEdgesFromDevelopmentGraph
   , getAllSentences
   , getAllAxioms
   , getAllGoals
   , getProvenGoals
   , getUnprovenGoals
   , prettySentence
   , prettySentenceOfTheory
   , prettyTheory
   , getDevelopmentGraphNodeType
   , theorySentenceIsAxiom
   , theorySentenceWasTheorem
   , theorySentenceIsDefined
   , theorySentenceGetTheoremStatus
   , theorySentencePriority
   , theorySentenceContent
   , theorySentenceBestProof
   , getLibraryDependencies
   , getRefinementTree
   , getAvailableSpecificationsForRefinement
) where

import Data.Aeson (encode, eitherDecode, Result(..), ToJSON)
import Data.Dynamic
import Data.Graph.Inductive (LNode, LEdge, mkGraph, labNodes, subgraph, suc)
import qualified Data.Map as Map
import qualified Data.Set as Set

import Common.AS_Annotation (SenAttr (..))
import Common.DocUtils (pretty, showDoc)
import Common.LibName (LibName)
import qualified Common.Lib.Graph as Graph
import qualified Common.Lib.Rel as Rel
import qualified Common.OrderedMap as OMap

import Logic.Logic(Logic)
import Logic.Prover(ThmStatus(..))
import Logic.Comorphism(AnyComorphism(..))

import HetsAPI.DataTypes (TheoryPointer, TheorySentenceByName, TheorySentence, Sentence)
import qualified HetsAPI.Refinement as Refinement

import Static.DevGraph (LibEnv, lookupDGraph, labNodesDG, labEdgesDG, DGraph, DGNodeLab, DGLinkLab, getDGNodeName, getRealDGNodeType, getLibDepRel, RTNodeLab, RTLinkLab, refTree, specRoots)
import Static.DgUtils (DGNodeType)
import Static.GTheory (G_theory (..), isProvenSenStatus, BasicProof(..))



-- | @getDevelopmentGraphByName name env@ returns the development graph for the
--   library @name@ in the environment @env@.
getGraphForLibrary :: LibName -> LibEnv -> DGraph
getGraphForLibrary :: LibName -> LibEnv -> DGraph
getGraphForLibrary = LibName -> LibEnv -> DGraph
lookupDGraph

-- | @getNodesFromDevelopmentGraph graph@ returns the nodes of the development
--   graph @graph@
getNodesFromDevelopmentGraph :: DGraph -> [DGNodeLab]
getNodesFromDevelopmentGraph :: DGraph -> [DGNodeLab]
getNodesFromDevelopmentGraph = ((Node, DGNodeLab) -> DGNodeLab)
-> [(Node, DGNodeLab)] -> [DGNodeLab]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Node, DGNodeLab) -> DGNodeLab
forall a b. (a, b) -> b
snd ([(Node, DGNodeLab)] -> [DGNodeLab])
-> (DGraph -> [(Node, DGNodeLab)]) -> DGraph -> [DGNodeLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> [(Node, DGNodeLab)]
labNodesDG

-- | @getNodesFromDevelopmentGraph graph@ returns the nodes of the development
--   graph @graph@
getLNodesFromDevelopmentGraph :: DGraph -> [LNode DGNodeLab]
getLNodesFromDevelopmentGraph :: DGraph -> [(Node, DGNodeLab)]
getLNodesFromDevelopmentGraph = DGraph -> [(Node, DGNodeLab)]
labNodesDG

getLEdgesFromDevelopmentGraph :: DGraph -> [LEdge DGLinkLab]
getLEdgesFromDevelopmentGraph :: DGraph -> [LEdge DGLinkLab]
getLEdgesFromDevelopmentGraph = DGraph -> [LEdge DGLinkLab]
labEdgesDG

getEdgesFromDevelopmentGraph :: DGraph -> [DGLinkLab]
getEdgesFromDevelopmentGraph :: DGraph -> [DGLinkLab]
getEdgesFromDevelopmentGraph = (LEdge DGLinkLab -> DGLinkLab) -> [LEdge DGLinkLab] -> [DGLinkLab]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(_, _, x :: DGLinkLab
x) -> DGLinkLab
x) ([LEdge DGLinkLab] -> [DGLinkLab])
-> (DGraph -> [LEdge DGLinkLab]) -> DGraph -> [DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> [LEdge DGLinkLab]
labEdgesDG

-- getGlobalAnnotations :: DGraph -> GlobalAnnos

theorySentenceIsAxiom :: SenAttr a (ThmStatus tStatus) -> Bool
theorySentenceIsAxiom :: SenAttr a (ThmStatus tStatus) -> Bool
theorySentenceIsAxiom = SenAttr a (ThmStatus tStatus) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom

theorySentenceWasTheorem :: SenAttr a (ThmStatus tStatus) -> Bool
theorySentenceWasTheorem :: SenAttr a (ThmStatus tStatus) -> Bool
theorySentenceWasTheorem = SenAttr a (ThmStatus tStatus) -> Bool
forall s a. SenAttr s a -> Bool
wasTheorem

theorySentenceIsDefined :: SenAttr a (ThmStatus tStatus) -> Bool
theorySentenceIsDefined :: SenAttr a (ThmStatus tStatus) -> Bool
theorySentenceIsDefined = SenAttr a (ThmStatus tStatus) -> Bool
forall s a. SenAttr s a -> Bool
isDef

theorySentenceGetTheoremStatus :: SenAttr a (ThmStatus tStatus) -> [tStatus]
theorySentenceGetTheoremStatus :: SenAttr a (ThmStatus tStatus) -> [tStatus]
theorySentenceGetTheoremStatus = ThmStatus tStatus -> [tStatus]
forall a. ThmStatus a -> [a]
getThmStatus (ThmStatus tStatus -> [tStatus])
-> (SenAttr a (ThmStatus tStatus) -> ThmStatus tStatus)
-> SenAttr a (ThmStatus tStatus)
-> [tStatus]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr a (ThmStatus tStatus) -> ThmStatus tStatus
forall s a. SenAttr s a -> a
senAttr

theorySentencePriority :: SenAttr a (ThmStatus tStatus) -> Maybe String
theorySentencePriority :: SenAttr a (ThmStatus tStatus) -> Maybe String
theorySentencePriority = SenAttr a (ThmStatus tStatus) -> Maybe String
forall s a. SenAttr s a -> Maybe String
priority

theorySentenceContent :: SenAttr a (ThmStatus tStatus) -> a
theorySentenceContent :: SenAttr a (ThmStatus tStatus) -> a
theorySentenceContent = SenAttr a (ThmStatus tStatus) -> a
forall s a. SenAttr s a -> s
sentence

theorySentenceBestProof :: Ord proof => SenAttr a (ThmStatus (c, proof)) -> Maybe proof
theorySentenceBestProof :: SenAttr a (ThmStatus (c, proof)) -> Maybe proof
theorySentenceBestProof sentence :: SenAttr a (ThmStatus (c, proof))
sentence =
    if [(c, proof)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(c, proof)]
ts then Maybe proof
forall a. Maybe a
Nothing else proof -> Maybe proof
forall a. a -> Maybe a
Just (proof -> Maybe proof) -> proof -> Maybe proof
forall a b. (a -> b) -> a -> b
$ [proof] -> proof
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([proof] -> proof) -> [proof] -> proof
forall a b. (a -> b) -> a -> b
$ ((c, proof) -> proof) -> [(c, proof)] -> [proof]
forall a b. (a -> b) -> [a] -> [b]
map (c, proof) -> proof
forall a b. (a, b) -> b
snd [(c, proof)]
ts
    where ts :: [(c, proof)]
ts = SenAttr a (ThmStatus (c, proof)) -> [(c, proof)]
forall a tStatus. SenAttr a (ThmStatus tStatus) -> [tStatus]
theorySentenceGetTheoremStatus SenAttr a (ThmStatus (c, proof))
sentence


toTheorySentence :: ToJSON sentence => SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> TheorySentence
toTheorySentence :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
toTheorySentence sen :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen = SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen { sentence :: Sentence
sentence = sentence -> Sentence
forall a. ToJSON a => a -> Sentence
encode (sentence -> Sentence)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> sentence)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> Sentence)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> Sentence
forall a b. (a -> b) -> a -> b
$ SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen }

getAllSentences :: G_theory -> TheorySentenceByName
getAllSentences :: G_theory -> TheorySentenceByName
getAllSentences (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> TheorySentence)
-> ThSens sentence (AnyComorphism, BasicProof)
-> TheorySentenceByName
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
forall sentence.
ToJSON sentence =>
SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
toTheorySentence ThSens sentence (AnyComorphism, BasicProof)
sens

getAllAxioms :: G_theory -> TheorySentenceByName
getAllAxioms :: G_theory -> TheorySentenceByName
getAllAxioms (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> TheorySentence)
-> ThSens sentence (AnyComorphism, BasicProof)
-> TheorySentenceByName
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
forall sentence.
ToJSON sentence =>
SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
toTheorySentence
    (ThSens sentence (AnyComorphism, BasicProof)
 -> TheorySentenceByName)
-> ThSens sentence (AnyComorphism, BasicProof)
-> TheorySentenceByName
forall a b. (a -> b) -> a -> b
$ (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (AnyComorphism, BasicProof)
sens

getAllGoals :: G_theory -> TheorySentenceByName
getAllGoals :: G_theory -> TheorySentenceByName
getAllGoals (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> TheorySentence)
-> ThSens sentence (AnyComorphism, BasicProof)
-> TheorySentenceByName
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
forall sentence.
ToJSON sentence =>
SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
toTheorySentence
    (ThSens sentence (AnyComorphism, BasicProof)
 -> TheorySentenceByName)
-> ThSens sentence (AnyComorphism, BasicProof)
-> TheorySentenceByName
forall a b. (a -> b) -> a -> b
$ (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter (Bool -> Bool
not (Bool -> Bool)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> Bool)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom) ThSens sentence (AnyComorphism, BasicProof)
sens

getProvenGoals :: G_theory -> TheorySentenceByName
getProvenGoals :: G_theory -> TheorySentenceByName
getProvenGoals (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> TheorySentence)
-> ThSens sentence (AnyComorphism, BasicProof)
-> TheorySentenceByName
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
forall sentence.
ToJSON sentence =>
SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
toTheorySentence
    (ThSens sentence (AnyComorphism, BasicProof)
 -> TheorySentenceByName)
-> ThSens sentence (AnyComorphism, BasicProof)
-> TheorySentenceByName
forall a b. (a -> b) -> a -> b
$ (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter (\sen :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen -> Bool -> Bool
not (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen) Bool -> Bool -> Bool
&& SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen) ThSens sentence (AnyComorphism, BasicProof)
sens

getUnprovenGoals :: G_theory -> TheorySentenceByName
getUnprovenGoals :: G_theory -> TheorySentenceByName
getUnprovenGoals (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> TheorySentence)
-> ThSens sentence (AnyComorphism, BasicProof)
-> TheorySentenceByName
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
forall sentence.
ToJSON sentence =>
SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> TheorySentence
toTheorySentence
    (ThSens sentence (AnyComorphism, BasicProof)
 -> TheorySentenceByName)
-> ThSens sentence (AnyComorphism, BasicProof)
-> TheorySentenceByName
forall a b. (a -> b) -> a -> b
$ (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter (\sen :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen -> Bool -> Bool
not (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen) Bool -> Bool -> Bool
&& Bool -> Bool
not (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen)) ThSens sentence (AnyComorphism, BasicProof)
sens

prettySentence' :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree =>
    sentence -> lid -> Sentence -> String
prettySentence' :: sentence -> lid -> Sentence -> String
prettySentence' (sentence
x::sentence) _ sen :: Sentence
sen = case (Sentence -> Either String sentence
forall a. FromJSON a => Sentence -> Either String a
eitherDecode Sentence
sen :: Either String sentence) of
    Left e :: String
e -> "Error parsing JSON: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e
    Right a :: sentence
a -> Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (sentence -> Doc) -> sentence -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sentence -> Doc
forall a. Pretty a => a -> Doc
pretty (sentence -> String) -> sentence -> String
forall a b. (a -> b) -> a -> b
$ sentence
a

prettySentence :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree =>
    lid -> Sentence -> String
prettySentence :: lid -> Sentence -> String
prettySentence = sentence -> lid -> Sentence -> String
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 =>
sentence -> lid -> Sentence -> String
prettySentence' (forall sentence. sentence
forall a. HasCallStack => a
undefined :: sentence)

prettyTheory :: G_theory -> String
prettyTheory :: G_theory -> String
prettyTheory th :: G_theory
th = G_theory -> String -> String
forall a. Pretty a => a -> String -> String
showDoc G_theory
th "\n"

prettySentenceOfTheory :: G_theory -> Sentence -> String
prettySentenceOfTheory :: G_theory -> Sentence -> String
prettySentenceOfTheory (G_theory lid :: lid
lid _ _ _ _ _) = lid -> Sentence -> String
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 -> Sentence -> String
prettySentence lid
lid

getDevelopmentGraphNodeType :: DGNodeLab -> DGNodeType
getDevelopmentGraphNodeType :: DGNodeLab -> DGNodeType
getDevelopmentGraphNodeType = DGNodeLab -> DGNodeType
getRealDGNodeType

getLibraryDependencies :: LibEnv -> [(LibName, LibName)]
getLibraryDependencies :: LibEnv -> [(LibName, LibName)]
getLibraryDependencies =
  Rel LibName -> [(LibName, LibName)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel LibName -> [(LibName, LibName)])
-> (LibEnv -> Rel LibName) -> LibEnv -> [(LibName, LibName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel LibName -> Rel LibName
forall a. Ord a => Rel a -> Rel a
Rel.intransKernel (Rel LibName -> Rel LibName)
-> (LibEnv -> Rel LibName) -> LibEnv -> Rel LibName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibEnv -> Rel LibName
getLibDepRel


getRefinementTree :: String -> DGraph -> Maybe (Graph.Gr Refinement.RefinementTreeNode Refinement.RefinementTreeLink)
getRefinementTree :: String
-> DGraph -> Maybe (Gr RefinementTreeNode RefinementTreeLink)
getRefinementTree = String
-> DGraph -> Maybe (Gr RefinementTreeNode RefinementTreeLink)
Refinement.getRefinementTree

getAvailableSpecificationsForRefinement :: DGraph -> [String]
getAvailableSpecificationsForRefinement :: DGraph -> [String]
getAvailableSpecificationsForRefinement = DGraph -> [String]
Refinement.getAvailableSpecificationsForRefinement