{- |
Description :  All commands to interact with the HETS API
Copyright   :  (c) Otto-von-Guericke University of Magdeburg
License     :  GPLv2 or higher, see LICENSE.txt
-}
module HetsAPI.Commands (
   automatic
   , globalSubsume
   , globalDecomposition
   , localInference
   , localDecomposition
   , compositionProveEdges
   , compositionCreateEdges
   , conservativity
   , automaticHideTheoremShift
   , theoremHideShift
   , computeColimit
   , normalForm
   , triangleCons
   , freeness
   , libFlatImports
   , libFlatDUnions
   , libFlatRenamings
   , libFlatHiding
   , libFlatHeterogen
   , qualifyLibEnv
   , loadLibrary
   , translateTheory
   , showTheory

   -- Hets.ProveCommands
   , HPC.getAvailableComorphisms
   , HPC.getUsableProvers
   , HPC.getUsableConsistencyCheckers
   , HPC.proveNode
   , HPC.checkConsistency
   , HPC.checkConservativityNode 

   -- Hets.InfoCommands
   , HIC.getGraphForLibrary
   , HIC.getNodesFromDevelopmentGraph
   , HIC.getLNodesFromDevelopmentGraph
   , HIC.getAllSentences
   , HIC.getAllAxioms
   , HIC.getAllGoals
   , HIC.getProvenGoals
   , HIC.getUnprovenGoals
) where

import qualified Data.Map as Map


import Common.Result (Result(..))
import Common.LibName (LibName)

import Interfaces.CmdAction (globLibAct, globLibResultAct)
import Interfaces.Command (GlobCmd(..))

import qualified HetsAPI.ProveCommands as HPC
import qualified HetsAPI.InfoCommands as HIC

import Driver.Options (HetcatsOpts)
import Driver.ReadMain (readAndAnalyse)

import Logic.Comorphism (AnyComorphism)
import Static.DevGraph (LibEnv)
import Static.GTheory (G_theory, mapG_theory)
import Common.DocUtils (Pretty(pretty))


globalCommands :: Map.Map GlobCmd (LibName -> LibEnv -> LibEnv)
globalCommands :: Map GlobCmd (LibName -> LibEnv -> LibEnv)
globalCommands = [(GlobCmd, LibName -> LibEnv -> LibEnv)]
-> Map GlobCmd (LibName -> LibEnv -> LibEnv)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(GlobCmd, LibName -> LibEnv -> LibEnv)]
globLibAct

globalCommand :: GlobCmd -> (LibName -> LibEnv -> LibEnv)
globalCommand :: GlobCmd -> LibName -> LibEnv -> LibEnv
globalCommand = Map GlobCmd (LibName -> LibEnv -> LibEnv)
-> GlobCmd -> LibName -> LibEnv -> LibEnv
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map GlobCmd (LibName -> LibEnv -> LibEnv)
globalCommands

globalCommandsR :: Map.Map GlobCmd (LibName -> LibEnv -> Result LibEnv)
globalCommandsR :: Map GlobCmd (LibName -> LibEnv -> Result LibEnv)
globalCommandsR = [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
-> Map GlobCmd (LibName -> LibEnv -> Result LibEnv)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
globLibResultAct

globalCommandR :: GlobCmd -> (LibName -> LibEnv -> Result LibEnv)
globalCommandR :: GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR = Map GlobCmd (LibName -> LibEnv -> Result LibEnv)
-> GlobCmd -> LibName -> LibEnv -> Result LibEnv
forall k a. Ord k => Map k a -> k -> a
(Map.!) Map GlobCmd (LibName -> LibEnv -> Result LibEnv)
globalCommandsR



automatic :: LibName -> LibEnv -> LibEnv
automatic :: LibName -> LibEnv -> LibEnv
automatic = GlobCmd -> LibName -> LibEnv -> LibEnv
globalCommand GlobCmd
Automatic

globalSubsume :: LibName -> LibEnv -> LibEnv
globalSubsume :: LibName -> LibEnv -> LibEnv
globalSubsume = GlobCmd -> LibName -> LibEnv -> LibEnv
globalCommand GlobCmd
GlobSubsume

globalDecomposition :: LibName -> LibEnv -> LibEnv
globalDecomposition :: LibName -> LibEnv -> LibEnv
globalDecomposition = GlobCmd -> LibName -> LibEnv -> LibEnv
globalCommand GlobCmd
GlobDecomp

localInference :: LibName -> LibEnv -> LibEnv
localInference :: LibName -> LibEnv -> LibEnv
localInference = GlobCmd -> LibName -> LibEnv -> LibEnv
globalCommand GlobCmd
LocalInference

localDecomposition :: LibName -> LibEnv -> LibEnv
localDecomposition :: LibName -> LibEnv -> LibEnv
localDecomposition = GlobCmd -> LibName -> LibEnv -> LibEnv
globalCommand GlobCmd
LocalDecomp

compositionProveEdges :: LibName -> LibEnv -> LibEnv
compositionProveEdges :: LibName -> LibEnv -> LibEnv
compositionProveEdges = GlobCmd -> LibName -> LibEnv -> LibEnv
globalCommand GlobCmd
CompositionProveEdges

compositionCreateEdges :: LibName -> LibEnv -> LibEnv
compositionCreateEdges :: LibName -> LibEnv -> LibEnv
compositionCreateEdges = GlobCmd -> LibName -> LibEnv -> LibEnv
globalCommand GlobCmd
CompositionCreateEdges

conservativity :: LibName -> LibEnv -> LibEnv
conservativity :: LibName -> LibEnv -> LibEnv
conservativity = GlobCmd -> LibName -> LibEnv -> LibEnv
globalCommand GlobCmd
Conservativity

automaticHideTheoremShift :: LibName -> LibEnv -> LibEnv
automaticHideTheoremShift :: LibName -> LibEnv -> LibEnv
automaticHideTheoremShift = GlobCmd -> LibName -> LibEnv -> LibEnv
globalCommand GlobCmd
HideThmShift


theoremHideShift :: LibName -> LibEnv -> Result LibEnv
theoremHideShift :: LibName -> LibEnv -> Result LibEnv
theoremHideShift = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
ThmHideShift

computeColimit :: LibName -> LibEnv -> Result LibEnv
computeColimit :: LibName -> LibEnv -> Result LibEnv
computeColimit = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
Colimit

normalForm :: LibName -> LibEnv -> Result LibEnv
normalForm :: LibName -> LibEnv -> Result LibEnv
normalForm = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
NormalForm

triangleCons :: LibName -> LibEnv -> Result LibEnv
triangleCons :: LibName -> LibEnv -> Result LibEnv
triangleCons = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
TriangleCons

freeness :: LibName -> LibEnv -> Result LibEnv
freeness :: LibName -> LibEnv -> Result LibEnv
freeness = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
Freeness



libFlatImports :: LibName -> LibEnv -> Result LibEnv
libFlatImports :: LibName -> LibEnv -> Result LibEnv
libFlatImports = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
Importing

libFlatDUnions :: LibName -> LibEnv -> Result LibEnv
libFlatDUnions :: LibName -> LibEnv -> Result LibEnv
libFlatDUnions = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
DisjointUnion

libFlatRenamings :: LibName -> LibEnv -> Result LibEnv
libFlatRenamings :: LibName -> LibEnv -> Result LibEnv
libFlatRenamings = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
Renaming

libFlatHiding :: LibName -> LibEnv -> Result LibEnv
libFlatHiding :: LibName -> LibEnv -> Result LibEnv
libFlatHiding = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
Hiding

libFlatHeterogen :: LibName -> LibEnv -> Result LibEnv
libFlatHeterogen :: LibName -> LibEnv -> Result LibEnv
libFlatHeterogen = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
Heterogeneity

qualifyLibEnv :: LibName -> LibEnv -> Result LibEnv
qualifyLibEnv :: LibName -> LibEnv -> Result LibEnv
qualifyLibEnv = GlobCmd -> LibName -> LibEnv -> Result LibEnv
globalCommandR GlobCmd
QualifyNames


loadLibrary :: FilePath -> HetcatsOpts -> IO (Result (LibName, LibEnv))
loadLibrary :: FilePath -> HetcatsOpts -> IO (Result (LibName, LibEnv))
loadLibrary file :: FilePath
file opts :: HetcatsOpts
opts = do
   Maybe (LibName, LibEnv)
analysisResult <- FilePath -> HetcatsOpts -> IO (Maybe (LibName, LibEnv))
readAndAnalyse FilePath
file HetcatsOpts
opts
   case Maybe (LibName, LibEnv)
analysisResult of
    Nothing -> Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv)))
-> Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ FilePath -> Result (LibName, LibEnv)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail  ("Unable to load library " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
file)
    Just lib :: (LibName, LibEnv)
lib -> Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv)))
-> Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ (LibName, LibEnv) -> Result (LibName, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName, LibEnv)
lib

translateTheory :: AnyComorphism -> G_theory -> Result G_theory
translateTheory :: AnyComorphism -> G_theory -> Result G_theory
translateTheory = Bool -> AnyComorphism -> G_theory -> Result G_theory
mapG_theory Bool
False

showTheory :: G_theory -> String
showTheory :: G_theory -> FilePath
showTheory = Doc -> FilePath
forall a. Show a => a -> FilePath
show (Doc -> FilePath) -> (G_theory -> Doc) -> G_theory -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_theory -> Doc
forall a. Pretty a => a -> Doc
pretty