{- |
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 fn lib_name = return . fn 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 fn lib_name ls = return . fn lib_name ls
-- | General function for implementing dg all style commands
commandDgAll :: (LibName -> LibEnv -> Result LibEnv)
-> CmdlState -> IO CmdlState
commandDgAll fn state = case i_state $ intState state of
Nothing -> return $ genMsgAndCode "No library loaded" 1 state
Just ist -> case fn (i_ln ist) (i_libEnv ist) of
Result _ (Just 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 -}
return $ add2hist [IStateChange $ Just ist] $ state
{ intState = (intState state)
{ i_state = Just $ emptyIntIState nwLibEnv $ i_ln ist } }
Result diag Nothing ->
return $ genMsgAndCode (concatMap diagString diag) 1 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 fn input state = case i_state $ intState state of
Nothing -> return $ genMsgAndCode "No library loaded" 1 state
Just ist -> do
let (_, edg, nbEdg, errs) = decomposeIntoGoals input
tmpErrs = prettyPrintErrList errs
case (edg, nbEdg) of
([], []) ->
-- leave the internal state intact so that the interface can recover
return $ genMsgAndCode (tmpErrs ++ "No edges in input string\n") 1
state
(_, _) -> do
let lsNodes = getAllNodes ist
lsEdges = getAllEdges ist
-- compute the list of edges from the input
(errs', listEdges) = obtainEdgeList edg nbEdg lsNodes lsEdges
tmpErrs' = tmpErrs ++ prettyPrintErrList errs'
case listEdges of
[] -> return $ genMsgAndCode
(tmpErrs' ++ "No edge in input string\n") 1 state
_ -> case fn (i_ln ist) listEdges (i_libEnv ist) of
Result _ (Just nwLibEnv) ->
-- name added later !!
return $ add2hist [IStateChange $ Just ist]
$ genMessage tmpErrs' [] state
{ intState = (intState state)
{ i_state = Just $ emptyIntIState nwLibEnv
$ i_ln ist } }
Result diag Nothing ->
return $ genMsgAndCode (concatMap diagString diag) 1 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 input state = do
let file = trim input
opts = hetsOpts state
tmp <- case i_state $ intState state of
Nothing -> anaLib opts file
Just dgState -> let
le = i_libEnv dgState
ln = i_ln dgState
dg = lookupDGraph ln le
initDG = cpIndexMaps dg emptyDG
in anaLibExt opts file le initDG
case tmp of
Nothing ->
-- leave the internal state intact so that the interface can recover
return $ genMsgAndCode ("Unable to load library " ++ input) 1 state
Just (nwLn, nwLibEnv) -> return state
{ intState = IntState
{ i_hist = IntHistory
{ undoList = []
, redoList = [] }
, i_state = Just $ emptyIntIState nwLibEnv nwLn
, filename = file }
, prompter = (prompter state)
{ fileLoaded = file } }
{- The only command that requires a list of nodes instead
of edges. -}
cDgThmHideShift :: String -> CmdlState -> IO CmdlState
cDgThmHideShift input state = case i_state $ intState state of
Nothing -> return $ genMsgAndCode "No library loaded" 1 state
Just dgState ->
let (errors, nodes) = getInputDGNodes input dgState
in if null nodes
then return $ genMsgAndCode errors 1 state
else let Result diag nwLibEnv = theoremHideShiftFromList
(i_ln dgState) nodes (i_libEnv dgState)
-- diag not used, how should it?
in return (case nwLibEnv of
Nothing -> genMsgAndCode (concatMap diagString diag) 1
state
-- ADD TO HISTORY ??
Just newEnv -> add2hist [IStateChange $ Just dgState] $
genMessage errors [] state
{ intState = (intState state)
{ i_state = Just $ emptyIntIState
newEnv $ i_ln
dgState
}
})
-- selection commands
selectANode :: Int -> IntIState -> [Int_NodeInfo]
selectANode x 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 = computeTheory (i_libEnv dgState) (i_ln dgState)
nodeName t = case lookup t $ getAllNodes dgState of
Nothing -> "Unknown node"
Just ll -> getDGNodeName ll
in case knownProversWithKind ProveCMDLautomatic of
Result _ Nothing -> []
Result _ (Just kpMap) ->
{- if compute theory was successful give the
result as one element list, otherwise an
empty list -}
case gth x of
Just th ->
-- le not used and should be
let sl = sublogicOfTh th
tmp = (initialState
(libToFileName (i_ln dgState) ++ "_" ++ nodeName x)
th
(shrinkKnownProvers sl kpMap))
{ comorphismsToProvers =
getAllProvers ProveCMDLautomatic sl logicGraph }
-- all goals and axioms are selected initialy in the proof status
in [initNodeInfo tmp 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 input state = let iState = intState state in
return $ case i_state iState of
Nothing -> genMsgAndCode "No library loaded" 1 state
Just dgState -> let (errors, nodes) = getInputDGNodes input dgState
in if null nodes then genMsgAndCode errors 1 state else
case maybeResult $ knownProversWithKind ProveCMDLautomatic of
Nothing -> genMsgAndCode (errors ++ "\nNo prover found") 1 state
Just _ -> let {- elems is the list of all results (i.e.
concat of all one element lists) -}
elems = concatMap (flip selectANode dgState . fst) nodes
nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState)
in add2hist [IStateChange $ Just dgState] $ genMessage errors [] state
{- add the prove state to the status
containing all information selected
in the input -}
{ intState = iState
{ i_state = Just nwist
{ elements = elems
, cComorphism = getIdComorphism elems } } }
cExpand :: String -> CmdlState -> IO CmdlState
cExpand input state = let iState = intState state in case i_state iState of
Nothing -> return $ genMsgAndCode "No library loaded to expand" 1 state
Just ist -> do
let opts = hetsOpts state
fname = trim input
lg = logicGraph
ln = i_ln ist
libenv = i_libEnv ist
dg = lookupDGraph ln libenv
Result ds mres <- runResultT
$ anaSourceFile lg opts Set.empty libenv dg fname
return $ case mres of
Nothing -> genMsgAndCode
("Analysis failed:\n" ++ showRelDiags (verbose opts) ds) 1 state
Just (lN', libEnv') ->
-- assume lN' is empty, ignored or identical to ln
let dg' = lookupDGraph lN' libEnv'
newLibEnv = Map.insert ln dg' $ Map.delete lN' libEnv'
in state
{ intState = iState
{ i_state = Just $ emptyIntIState newLibEnv ln } }
cAddView :: String -> CmdlState -> IO CmdlState
cAddView input state = let iState = intState state in case i_state iState of
Nothing -> return $ genMsgAndCode "No library loaded to add view to" 1 state
Just ist -> do
let libenv = i_libEnv ist
ln = i_ln ist
lg = logicGraph
opts = hetsOpts state
dg = lookupDGraph ln libenv
[vn, spec1, spec2] = words input
mkSpecInst = makeSpecInst . simpleIdToIRI . mkSimpleId
Result ds tmp <- runResultT $ liftR $ anaViewDefn lg ln libenv dg opts
Map.empty -- not sure if no CURIE-to-IRI mapping shall be done
(simpleIdToIRI $ mkSimpleId vn) (Genericity (Params []) (Imported [])
nullRange)
(View_type (mkSpecInst spec1)
(mkSpecInst spec2) nullRange) [] nullRange
return $ case tmp of
Nothing -> genMsgAndCode
("View analysis failed:\n" ++ showRelDiags (verbose opts) ds) 1 state
Just (_, nwDg, nwLibEnv, _, _) ->
let newLibEnv' = Map.insert ln nwDg nwLibEnv
in state
{ intState = iState
{ i_state = Just $ emptyIntIState newLibEnv' ln } }
{- | Function switches the interface in proving mode by
selecting all nodes -}
cDgSelectAll :: CmdlState -> IO CmdlState
cDgSelectAll state = let iState = intState state in
return $ case i_state iState of
Nothing -> genMsgAndCode "No library loaded" 1 state
Just dgState ->
case maybeResult $ knownProversWithKind ProveCMDLautomatic of
Nothing -> genMsgAndCode "No prover found" 1 state
Just _ -> let
-- list of all nodes
lsNodes = getAllNodes dgState
{- elems is the list of all results (i.e. concat
of all one element lists) -}
elems = concatMap (flip selectANode dgState . fst) lsNodes
nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState)
-- ADD TO HISTORY
in add2hist [IStateChange $ Just dgState] $ state
{- add the prove state to the status containing
all information selected in the input -}
{ intState = iState
{ i_state = Just nwist
{ elements = elems
, cComorphism = getIdComorphism elems } } }