{-# 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
) where

import HetsAPI.DataTypes (TheoryPointer)

import Common.LibName (LibName)
import Static.DevGraph (LibEnv, lookupDGraph, labNodesDG, labEdgesDG, DGraph, DGNodeLab, DGLinkLab, getDGNodeName)
import Data.Graph.Inductive (LNode, LEdge)
import Static.GTheory (G_theory (..), isProvenSenStatus)
import qualified Common.OrderedMap as OMap
import Common.AS_Annotation (sentence, SenAttr (isAxiom))
import Data.Aeson (encode, eitherDecode, Result(..))
import Logic.Logic(Logic)
import Common.DocUtils (pretty)


import Data.Dynamic

import HetsAPI.DataTypes (SentenceByName, Sentence)


-- | @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

getAllSentences :: G_theory -> SentenceByName
getAllSentences :: G_theory -> SentenceByName
getAllSentences (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> ByteString)
-> ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map (sentence -> ByteString
forall a. ToJSON a => a -> ByteString
encode (sentence -> ByteString)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> sentence)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence) ThSens sentence (AnyComorphism, BasicProof)
sens

getAllAxioms :: G_theory -> SentenceByName
getAllAxioms :: G_theory -> SentenceByName
getAllAxioms (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> ByteString)
-> ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map (sentence -> ByteString
forall a. ToJSON a => a -> ByteString
encode (sentence -> ByteString)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> sentence)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence)
    (ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName)
-> ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName
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 -> SentenceByName
getAllGoals :: G_theory -> SentenceByName
getAllGoals (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> ByteString)
-> ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map (sentence -> ByteString
forall a. ToJSON a => a -> ByteString
encode (sentence -> ByteString)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> sentence)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence)
    (ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName)
-> ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName
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 -> SentenceByName
getProvenGoals :: G_theory -> SentenceByName
getProvenGoals (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> ByteString)
-> ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map (sentence -> ByteString
forall a. ToJSON a => a -> ByteString
encode (sentence -> ByteString)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> sentence)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence)
    (ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName)
-> ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName
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 -> SentenceByName
getUnprovenGoals :: G_theory -> SentenceByName
getUnprovenGoals (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> ByteString)
-> ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map (sentence -> ByteString
forall a. ToJSON a => a -> ByteString
encode (sentence -> ByteString)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> sentence)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence)
    (ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName)
-> ThSens sentence (AnyComorphism, BasicProof) -> SentenceByName
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 -> 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

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 -> ByteString -> String
prettySentence' (sentence
x::sentence) _ sen :: ByteString
sen = case (ByteString -> Either String sentence
forall a. FromJSON a => ByteString -> Either String a
eitherDecode ByteString
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 -> ByteString -> String
prettySentence = sentence -> lid -> ByteString -> 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 -> ByteString -> String
prettySentence' (forall sentence. sentence
forall a. HasCallStack => a
undefined :: sentence)

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