{- |
Module      :./CMDL/DgCommands.hs
Description : CMDL interface development graph commands
Copyright   : uni-bremen and DFKI
License     : GPLv2 or higher, see LICENSE.txt
Maintainer  : r.pascanu@jacobs-university.de
Stability   : provisional
Portability : portable

CMDL.DgCommands contains all development graph commands
that can be called from the CMDL interface
-}

module CMDL.DgCommands
       ( commandDgAll
       , commandDg
       , cUse
       , cDgThmHideShift
       , cDgSelect
       , cDgSelectAll
       , cExpand
       , cAddView
       , selectANode
       , wrapResultDg
       , wrapResultDgAll
       ) where

import Interfaces.DataTypes
import Interfaces.Utils

import CMDL.DataTypes

import CMDL.DataTypesUtils
import CMDL.Utils (decomposeIntoGoals, obtainEdgeList, prettyPrintErrList)

import Proofs.AbstractState (comorphismsToProvers, getAllProvers, initialState)
import Proofs.TheoremHideShift (theoremHideShiftFromList)

import Static.AnalysisLibrary
import Static.GTheory (sublogicOfTh)
import Static.DevGraph
import Static.ComputeTheory (computeTheory)

import Driver.AnaLib (anaLib, anaLibExt)
import Driver.Options

import Comorphisms.KnownProvers (knownProversWithKind, shrinkKnownProvers)
import Comorphisms.LogicGraph (logicGraph)

import Logic.Prover (ProverKind (ProveCMDLautomatic))

import Syntax.AS_Structured
import Syntax.AS_Library

import Common.LibName
import Common.Utils (trim)
import Common.Result
import Common.ResultT
import Common.Id
import Common.IRI (simpleIdToIRI)

import Data.Graph.Inductive.Graph (LEdge)
import qualified Data.Map as Map
import qualified Data.Set as Set

-- | Wraps Result structure around the result of a dg all style command
wrapResultDgAll :: (LibName -> LibEnv -> LibEnv)
                -> LibName -> LibEnv -> Result LibEnv
wrapResultDgAll :: (LibName -> LibEnv -> LibEnv) -> LibName -> LibEnv -> Result LibEnv
wrapResultDgAll fn :: LibName -> LibEnv -> LibEnv
fn lib_name :: LibName
lib_name = LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv)
-> (LibEnv -> LibEnv) -> LibEnv -> Result LibEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> LibEnv -> LibEnv
fn LibName
lib_name

-- | Wraps Result structure around the result of a dg style command
wrapResultDg :: (LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv)
             -> LibName -> [LEdge DGLinkLab] -> LibEnv -> Result LibEnv
wrapResultDg :: (LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv)
-> LibName -> [LEdge DGLinkLab] -> LibEnv -> Result LibEnv
wrapResultDg fn :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
fn lib_name :: LibName
lib_name ls :: [LEdge DGLinkLab]
ls = LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv)
-> (LibEnv -> LibEnv) -> LibEnv -> Result LibEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
fn LibName
lib_name [LEdge DGLinkLab]
ls

-- | General function for implementing dg all style commands
commandDgAll :: (LibName -> LibEnv -> Result LibEnv)
             -> CmdlState -> IO CmdlState
commandDgAll :: (LibName -> LibEnv -> Result LibEnv) -> CmdlState -> IO CmdlState
commandDgAll fn :: LibName -> LibEnv -> Result LibEnv
fn state :: CmdlState
state = case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
  Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No library loaded" 1 CmdlState
state
  Just ist :: IntIState
ist -> case LibName -> LibEnv -> Result LibEnv
fn (IntIState -> LibName
i_ln IntIState
ist) (IntIState -> LibEnv
i_libEnv IntIState
ist) of
    Result _ (Just nwLibEnv :: LibEnv
nwLibEnv) ->
         {- Name of function is not known here, so an empty text is
         added as name, in a later stage (Shell.hs) the name will
         be inserted -}
        CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ [UndoRedoElem] -> CmdlState -> CmdlState
add2hist [Maybe IntIState -> UndoRedoElem
IStateChange (Maybe IntIState -> UndoRedoElem)
-> Maybe IntIState -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
ist] (CmdlState -> CmdlState) -> CmdlState -> CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlState
state
             { intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state)
                 { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> IntIState
emptyIntIState LibEnv
nwLibEnv (LibName -> IntIState) -> LibName -> IntIState
forall a b. (a -> b) -> a -> b
$ IntIState -> LibName
i_ln IntIState
ist } }
    Result diag :: [Diagnosis]
diag Nothing ->
        CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode ((Diagnosis -> String) -> [Diagnosis] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Diagnosis -> String
diagString [Diagnosis]
diag) 1 CmdlState
state

{- | Generic function for a dg command, all other dg
commands are derived from this command by simply
specifing the function -}
commandDg :: (LibName -> [LEdge DGLinkLab] -> LibEnv -> Result LibEnv)
          -> String -> CmdlState -> IO CmdlState
commandDg :: (LibName -> [LEdge DGLinkLab] -> LibEnv -> Result LibEnv)
-> String -> CmdlState -> IO CmdlState
commandDg fn :: LibName -> [LEdge DGLinkLab] -> LibEnv -> Result LibEnv
fn input :: String
input state :: CmdlState
state = case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No library loaded" 1 CmdlState
state
    Just ist :: IntIState
ist -> do
     let (_, edg :: [String]
edg, nbEdg :: [String]
nbEdg, errs :: [String]
errs) = String -> ([String], [String], [String], [String])
decomposeIntoGoals String
input
         tmpErrs :: String
tmpErrs = [String] -> String
prettyPrintErrList [String]
errs
     case ([String]
edg, [String]
nbEdg) of
       ([], []) ->
         -- leave the internal state intact so that the interface can recover
         CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode (String
tmpErrs String -> String -> String
forall a. [a] -> [a] -> [a]
++ "No edges in input string\n") 1
                   CmdlState
state
       (_, _) -> do
        let lsNodes :: [LNode DGNodeLab]
lsNodes = IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
ist
            lsEdges :: [LEdge DGLinkLab]
lsEdges = IntIState -> [LEdge DGLinkLab]
getAllEdges IntIState
ist
            -- compute the list of edges from the input
            (errs' :: [String]
errs', listEdges :: [LEdge DGLinkLab]
listEdges) = [String]
-> [String]
-> [LNode DGNodeLab]
-> [LEdge DGLinkLab]
-> ([String], [LEdge DGLinkLab])
obtainEdgeList [String]
edg [String]
nbEdg [LNode DGNodeLab]
lsNodes [LEdge DGLinkLab]
lsEdges
            tmpErrs' :: String
tmpErrs' = String
tmpErrs String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
prettyPrintErrList [String]
errs'
        case [LEdge DGLinkLab]
listEdges of
         [] -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode
                         (String
tmpErrs' String -> String -> String
forall a. [a] -> [a] -> [a]
++ "No edge in input string\n") 1 CmdlState
state
         _ -> case LibName -> [LEdge DGLinkLab] -> LibEnv -> Result LibEnv
fn (IntIState -> LibName
i_ln IntIState
ist) [LEdge DGLinkLab]
listEdges (IntIState -> LibEnv
i_libEnv IntIState
ist) of
             Result _ (Just nwLibEnv :: LibEnv
nwLibEnv) ->
               -- name added later !!
                 CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ [UndoRedoElem] -> CmdlState -> CmdlState
add2hist [Maybe IntIState -> UndoRedoElem
IStateChange (Maybe IntIState -> UndoRedoElem)
-> Maybe IntIState -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
ist]
                   (CmdlState -> CmdlState) -> CmdlState -> CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage String
tmpErrs' [] CmdlState
state
                     { intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state)
                         { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> IntIState
emptyIntIState LibEnv
nwLibEnv
                             (LibName -> IntIState) -> LibName -> IntIState
forall a b. (a -> b) -> a -> b
$ IntIState -> LibName
i_ln IntIState
ist } }
             Result diag :: [Diagnosis]
diag Nothing ->
               CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode ((Diagnosis -> String) -> [Diagnosis] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Diagnosis -> String
diagString [Diagnosis]
diag) 1 CmdlState
state

{- | The function 'cUse' implements the Use commands, i.e.
given a path it tries to load the library  at that path -}
cUse :: String -> CmdlState -> IO CmdlState
cUse :: String -> CmdlState -> IO CmdlState
cUse input :: String
input state :: CmdlState
state = do
   let file :: String
file = String -> String
trim String
input
       opts :: HetcatsOpts
opts = CmdlState -> HetcatsOpts
hetsOpts CmdlState
state
   Maybe (LibName, LibEnv)
tmp <- case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
           Nothing -> HetcatsOpts -> String -> IO (Maybe (LibName, LibEnv))
anaLib HetcatsOpts
opts String
file
           Just dgState :: IntIState
dgState -> let
             le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
dgState
             ln :: LibName
ln = IntIState -> LibName
i_ln IntIState
dgState
             dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
             initDG :: DGraph
initDG = DGraph -> DGraph -> DGraph
cpIndexMaps DGraph
dg DGraph
emptyDG
             in HetcatsOpts
-> String -> LibEnv -> DGraph -> IO (Maybe (LibName, LibEnv))
anaLibExt HetcatsOpts
opts String
file LibEnv
le DGraph
initDG
   case Maybe (LibName, LibEnv)
tmp of
    Nothing ->
      -- leave the internal state intact so that the interface can recover
      CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode ("Unable to load library " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
input) 1 CmdlState
state
    Just (nwLn :: LibName
nwLn, nwLibEnv :: LibEnv
nwLibEnv) -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
      { intState :: IntState
intState = IntState :: IntHistory -> Maybe IntIState -> String -> IntState
IntState
          { i_hist :: IntHistory
i_hist = IntHistory :: [CmdHistory] -> [CmdHistory] -> IntHistory
IntHistory
              { undoList :: [CmdHistory]
undoList = []
              , redoList :: [CmdHistory]
redoList = [] }
          , i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> IntIState
emptyIntIState LibEnv
nwLibEnv LibName
nwLn
          , filename :: String
filename = String
file }
      , prompter :: CmdlPrompterState
prompter = (CmdlState -> CmdlPrompterState
prompter CmdlState
state)
          { fileLoaded :: String
fileLoaded = String
file } }

{- The only command that requires a list of nodes instead
of edges. -}
cDgThmHideShift :: String -> CmdlState -> IO CmdlState
cDgThmHideShift :: String -> CmdlState -> IO CmdlState
cDgThmHideShift input :: String
input state :: CmdlState
state = case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No library loaded" 1 CmdlState
state
    Just dgState :: IntIState
dgState ->
      let (errors :: String
errors, nodes :: [LNode DGNodeLab]
nodes) = String -> IntIState -> (String, [LNode DGNodeLab])
getInputDGNodes String
input IntIState
dgState
       in if [LNode DGNodeLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LNode DGNodeLab]
nodes
            then CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode String
errors 1 CmdlState
state
            else let Result diag :: [Diagnosis]
diag nwLibEnv :: Maybe LibEnv
nwLibEnv = LibName -> [LNode DGNodeLab] -> LibEnv -> Result LibEnv
theoremHideShiftFromList
                        (IntIState -> LibName
i_ln IntIState
dgState) [LNode DGNodeLab]
nodes (IntIState -> LibEnv
i_libEnv IntIState
dgState)
                     -- diag not used, how should it?
                  in CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (case Maybe LibEnv
nwLibEnv of
                       Nothing -> String -> Int -> CmdlState -> CmdlState
genMsgAndCode ((Diagnosis -> String) -> [Diagnosis] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Diagnosis -> String
diagString [Diagnosis]
diag) 1
                                   CmdlState
state
                       -- ADD TO HISTORY ??
                       Just newEnv :: LibEnv
newEnv -> [UndoRedoElem] -> CmdlState -> CmdlState
add2hist [Maybe IntIState -> UndoRedoElem
IStateChange (Maybe IntIState -> UndoRedoElem)
-> Maybe IntIState -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
dgState] (CmdlState -> CmdlState) -> CmdlState -> CmdlState
forall a b. (a -> b) -> a -> b
$
                                        String -> String -> CmdlState -> CmdlState
genMessage String
errors [] CmdlState
state
                                          { intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state)
                                              { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> IntIState
emptyIntIState
                                                                   LibEnv
newEnv (LibName -> IntIState) -> LibName -> IntIState
forall a b. (a -> b) -> a -> b
$ IntIState -> LibName
i_ln
                                                                     IntIState
dgState
                                               }
                                          })

-- selection commands
selectANode :: Int -> IntIState -> [Int_NodeInfo]
selectANode :: Int -> IntIState -> [Int_NodeInfo]
selectANode x :: Int
x dgState :: IntIState
dgState = let
    {- computes the theory of a given node
    (i.e. solves DGRef cases and so on,
    see CASL Reference Manual, p.294, Def 4.9) -}
    gth :: Int -> Maybe G_theory
gth = LibEnv -> LibName -> Int -> Maybe G_theory
computeTheory (IntIState -> LibEnv
i_libEnv IntIState
dgState) (IntIState -> LibName
i_ln IntIState
dgState)
    nodeName :: Int -> String
nodeName t :: Int
t = case Int -> [LNode DGNodeLab] -> Maybe DGNodeLab
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
t ([LNode DGNodeLab] -> Maybe DGNodeLab)
-> [LNode DGNodeLab] -> Maybe DGNodeLab
forall a b. (a -> b) -> a -> b
$ IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
dgState of
                Nothing -> "Unknown node"
                Just ll :: DGNodeLab
ll -> DGNodeLab -> String
getDGNodeName DGNodeLab
ll
    in case ProverKind -> Result KnownProversMap
knownProversWithKind ProverKind
ProveCMDLautomatic of
     Result _ Nothing -> []
     Result _ (Just kpMap :: KnownProversMap
kpMap) ->
    {- if compute theory was successful give the
    result as one element list, otherwise an
    empty list -}
      case Int -> Maybe G_theory
gth Int
x of
       Just th :: G_theory
th ->
       -- le not used and should be
         let sl :: G_sublogics
sl = G_theory -> G_sublogics
sublogicOfTh G_theory
th
             tmp :: ProofState
tmp = (String -> G_theory -> KnownProversMap -> ProofState
initialState
                (LibName -> String
libToFileName (IntIState -> LibName
i_ln IntIState
dgState) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
nodeName Int
x)
                G_theory
th
                (G_sublogics -> KnownProversMap -> KnownProversMap
shrinkKnownProvers G_sublogics
sl KnownProversMap
kpMap))
                { comorphismsToProvers :: [(G_prover, AnyComorphism)]
comorphismsToProvers =
                    ProverKind
-> G_sublogics -> LogicGraph -> [(G_prover, AnyComorphism)]
getAllProvers ProverKind
ProveCMDLautomatic G_sublogics
sl LogicGraph
logicGraph }
         -- all goals and axioms are selected initialy in the proof status
         in [ProofState -> Int -> Int_NodeInfo
initNodeInfo ProofState
tmp Int
x]
       _ -> []

{- | function swithces interface in proving mode and also
selects a list of nodes to be used inside this mode -}
cDgSelect :: String -> CmdlState -> IO CmdlState
cDgSelect :: String -> CmdlState -> IO CmdlState
cDgSelect input :: String
input state :: CmdlState
state = let iState :: IntState
iState = CmdlState -> IntState
intState CmdlState
state in
  CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ case IntState -> Maybe IntIState
i_state IntState
iState of
    Nothing -> String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No library loaded" 1 CmdlState
state
    Just dgState :: IntIState
dgState -> let (errors :: String
errors, nodes :: [LNode DGNodeLab]
nodes) = String -> IntIState -> (String, [LNode DGNodeLab])
getInputDGNodes String
input IntIState
dgState
      in if [LNode DGNodeLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LNode DGNodeLab]
nodes then String -> Int -> CmdlState -> CmdlState
genMsgAndCode String
errors 1 CmdlState
state else
      case Result KnownProversMap -> Maybe KnownProversMap
forall a. Result a -> Maybe a
maybeResult (Result KnownProversMap -> Maybe KnownProversMap)
-> Result KnownProversMap -> Maybe KnownProversMap
forall a b. (a -> b) -> a -> b
$ ProverKind -> Result KnownProversMap
knownProversWithKind ProverKind
ProveCMDLautomatic of
        Nothing -> String -> Int -> CmdlState -> CmdlState
genMsgAndCode (String
errors String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\nNo prover found") 1 CmdlState
state
        Just _ -> let {- elems is the list of all results (i.e.
                      concat of all one element lists) -}
            elems :: [Int_NodeInfo]
elems = (LNode DGNodeLab -> [Int_NodeInfo])
-> [LNode DGNodeLab] -> [Int_NodeInfo]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Int -> IntIState -> [Int_NodeInfo])
-> IntIState -> Int -> [Int_NodeInfo]
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> IntIState -> [Int_NodeInfo]
selectANode IntIState
dgState (Int -> [Int_NodeInfo])
-> (LNode DGNodeLab -> Int) -> LNode DGNodeLab -> [Int_NodeInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> Int
forall a b. (a, b) -> a
fst) [LNode DGNodeLab]
nodes
            nwist :: IntIState
nwist = LibEnv -> LibName -> IntIState
emptyIntIState (IntIState -> LibEnv
i_libEnv IntIState
dgState) (IntIState -> LibName
i_ln IntIState
dgState)
         in [UndoRedoElem] -> CmdlState -> CmdlState
add2hist [Maybe IntIState -> UndoRedoElem
IStateChange (Maybe IntIState -> UndoRedoElem)
-> Maybe IntIState -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
dgState] (CmdlState -> CmdlState) -> CmdlState -> CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage String
errors [] CmdlState
state
           {- add the prove state to the status
           containing all information selected
           in the input -}
           { intState :: IntState
intState = IntState
iState
               { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
nwist
                   { elements :: [Int_NodeInfo]
elements = [Int_NodeInfo]
elems
                   , cComorphism :: Maybe AnyComorphism
cComorphism = [Int_NodeInfo] -> Maybe AnyComorphism
getIdComorphism [Int_NodeInfo]
elems } } }

cExpand :: String -> CmdlState -> IO CmdlState
cExpand :: String -> CmdlState -> IO CmdlState
cExpand input :: String
input state :: CmdlState
state = let iState :: IntState
iState = CmdlState -> IntState
intState CmdlState
state in case IntState -> Maybe IntIState
i_state IntState
iState of
  Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No library loaded to expand" 1 CmdlState
state
  Just ist :: IntIState
ist -> do
    let opts :: HetcatsOpts
opts = CmdlState -> HetcatsOpts
hetsOpts CmdlState
state
        fname :: String
fname = String -> String
trim String
input
        lg :: LogicGraph
lg = LogicGraph
logicGraph
        ln :: LibName
ln = IntIState -> LibName
i_ln IntIState
ist
        libenv :: LibEnv
libenv = IntIState -> LibEnv
i_libEnv IntIState
ist
        dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libenv
    Result ds :: [Diagnosis]
ds mres :: Maybe (LibName, LibEnv)
mres <- ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT
      (ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv)))
-> ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> String
-> ResultT IO (LibName, LibEnv)
anaSourceFile LogicGraph
lg HetcatsOpts
opts LNS
forall a. Set a
Set.empty LibEnv
libenv DGraph
dg String
fname
    CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ case Maybe (LibName, LibEnv)
mres of
      Nothing -> String -> Int -> CmdlState -> CmdlState
genMsgAndCode
        ("Analysis failed:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> [Diagnosis] -> String
showRelDiags (HetcatsOpts -> Int
verbose HetcatsOpts
opts) [Diagnosis]
ds) 1 CmdlState
state
      Just (lN' :: LibName
lN', libEnv' :: LibEnv
libEnv') ->
       -- assume lN' is empty, ignored or identical to ln
        let dg' :: DGraph
dg' = LibName -> LibEnv -> DGraph
lookupDGraph LibName
lN' LibEnv
libEnv'
            newLibEnv :: LibEnv
newLibEnv = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
dg' (LibEnv -> LibEnv) -> LibEnv -> LibEnv
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> LibEnv
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete LibName
lN' LibEnv
libEnv'
        in CmdlState
state
          { intState :: IntState
intState = IntState
iState
              { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> IntIState
emptyIntIState LibEnv
newLibEnv LibName
ln } }

cAddView :: String -> CmdlState -> IO CmdlState
cAddView :: String -> CmdlState -> IO CmdlState
cAddView input :: String
input state :: CmdlState
state = let iState :: IntState
iState = CmdlState -> IntState
intState CmdlState
state in case IntState -> Maybe IntIState
i_state IntState
iState of
  Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No library loaded to add view to" 1 CmdlState
state
  Just ist :: IntIState
ist -> do
    let libenv :: LibEnv
libenv = IntIState -> LibEnv
i_libEnv IntIState
ist
        ln :: LibName
ln = IntIState -> LibName
i_ln IntIState
ist
        lg :: LogicGraph
lg = LogicGraph
logicGraph
        opts :: HetcatsOpts
opts = CmdlState -> HetcatsOpts
hetsOpts CmdlState
state
        dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libenv
        [vn :: String
vn, spec1 :: String
spec1, spec2 :: String
spec2] = String -> [String]
words String
input
        mkSpecInst :: String -> Annoted SPEC
mkSpecInst = SPEC_NAME -> Annoted SPEC
makeSpecInst (SPEC_NAME -> Annoted SPEC)
-> (String -> SPEC_NAME) -> String -> Annoted SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> SPEC_NAME
simpleIdToIRI (SIMPLE_ID -> SPEC_NAME)
-> (String -> SIMPLE_ID) -> String -> SPEC_NAME
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> SIMPLE_ID
mkSimpleId
    Result ds :: [Diagnosis]
ds tmp :: Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
tmp <- ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> IO
      (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)))
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
forall a b. (a -> b) -> a -> b
$ Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> LibName
-> LibEnv
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> SPEC_NAME
-> GENERICITY
-> VIEW_TYPE
-> [G_mapping]
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
anaViewDefn LogicGraph
lg LibName
ln LibEnv
libenv DGraph
dg HetcatsOpts
opts
      ExpOverrides
forall k a. Map k a
Map.empty -- not sure if no CURIE-to-IRI mapping shall be done
      (SIMPLE_ID -> SPEC_NAME
simpleIdToIRI (SIMPLE_ID -> SPEC_NAME) -> SIMPLE_ID -> SPEC_NAME
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId String
vn) (PARAMS -> IMPORTED -> Range -> GENERICITY
Genericity ([Annoted SPEC] -> PARAMS
Params []) ([Annoted SPEC] -> IMPORTED
Imported [])
                                        Range
nullRange)
      (Annoted SPEC -> Annoted SPEC -> Range -> VIEW_TYPE
View_type (String -> Annoted SPEC
mkSpecInst String
spec1)
       (String -> Annoted SPEC
mkSpecInst String
spec2) Range
nullRange) [] Range
nullRange
    CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ case Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
tmp of
      Nothing -> String -> Int -> CmdlState -> CmdlState
genMsgAndCode
          ("View analysis failed:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> [Diagnosis] -> String
showRelDiags (HetcatsOpts -> Int
verbose HetcatsOpts
opts) [Diagnosis]
ds) 1 CmdlState
state
      Just (_, nwDg :: DGraph
nwDg, nwLibEnv :: LibEnv
nwLibEnv, _, _) ->
        let newLibEnv' :: LibEnv
newLibEnv' = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
nwDg LibEnv
nwLibEnv
        in CmdlState
state
          { intState :: IntState
intState = IntState
iState
              { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> IntIState
emptyIntIState LibEnv
newLibEnv' LibName
ln } }

{- | Function switches the interface in proving mode by
selecting all nodes -}
cDgSelectAll :: CmdlState -> IO CmdlState
cDgSelectAll :: CmdlState -> IO CmdlState
cDgSelectAll state :: CmdlState
state = let iState :: IntState
iState = CmdlState -> IntState
intState CmdlState
state in
  CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ case IntState -> Maybe IntIState
i_state IntState
iState of
  Nothing -> String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No library loaded" 1 CmdlState
state
  Just dgState :: IntIState
dgState ->
    case Result KnownProversMap -> Maybe KnownProversMap
forall a. Result a -> Maybe a
maybeResult (Result KnownProversMap -> Maybe KnownProversMap)
-> Result KnownProversMap -> Maybe KnownProversMap
forall a b. (a -> b) -> a -> b
$ ProverKind -> Result KnownProversMap
knownProversWithKind ProverKind
ProveCMDLautomatic of
      Nothing -> String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No prover found" 1 CmdlState
state
      Just _ -> let
          -- list of all nodes
          lsNodes :: [LNode DGNodeLab]
lsNodes = IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
dgState
          {- elems is the list of all results (i.e. concat
          of all one element lists) -}
          elems :: [Int_NodeInfo]
elems = (LNode DGNodeLab -> [Int_NodeInfo])
-> [LNode DGNodeLab] -> [Int_NodeInfo]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Int -> IntIState -> [Int_NodeInfo])
-> IntIState -> Int -> [Int_NodeInfo]
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> IntIState -> [Int_NodeInfo]
selectANode IntIState
dgState (Int -> [Int_NodeInfo])
-> (LNode DGNodeLab -> Int) -> LNode DGNodeLab -> [Int_NodeInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> Int
forall a b. (a, b) -> a
fst) [LNode DGNodeLab]
lsNodes
          nwist :: IntIState
nwist = LibEnv -> LibName -> IntIState
emptyIntIState (IntIState -> LibEnv
i_libEnv IntIState
dgState) (IntIState -> LibName
i_ln IntIState
dgState)
               -- ADD TO HISTORY
        in [UndoRedoElem] -> CmdlState -> CmdlState
add2hist [Maybe IntIState -> UndoRedoElem
IStateChange (Maybe IntIState -> UndoRedoElem)
-> Maybe IntIState -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
dgState] (CmdlState -> CmdlState) -> CmdlState -> CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlState
state
              {- add the prove state to the status containing
              all information selected in the input -}
              { intState :: IntState
intState = IntState
iState
                  { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
nwist
                      { elements :: [Int_NodeInfo]
elements = [Int_NodeInfo]
elems
                      , cComorphism :: Maybe AnyComorphism
cComorphism = [Int_NodeInfo] -> Maybe AnyComorphism
getIdComorphism [Int_NodeInfo]
elems } } }