8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova{- |

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaModule :$Header$

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaDescription : CMDL interface commands

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina SojakovaCopyright : uni-bremen and DFKI

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaLicence : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaMaintainer : r.pascanu@jacobs-university.de

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaStability : provisional

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaPortability : portable

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaPGIP.ProveCommands contains all commands

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovarelated to prove mode

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-}

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovamodule PGIP.ProveCommands

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ( shellTranslate

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellProver

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellProveAll

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellProve

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellSelectAxms

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellSelectGoals

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellSetAxmsAll

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellSetGoalsAll

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellUnselectAxms

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellUnselectGoals

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova , shellUnselectAxmsAll

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellUnselectGoalsAll

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova , shellAddAxms

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova , shellAddGoals

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova , shellUseThms

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellDontUseThms

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova , shellSave2File

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova , shellDontSave2File

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova , shellEndScript

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellBeginScript

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , shellTimeLimit

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , selectANode

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova ) where

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport System.Console.Shell.ShellMonad

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport PGIP.CMDLState

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport PGIP.CMDLUtils

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport PGIP.CMDLShell

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport PGIP.DgCommands

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Static.GTheory

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Static.DevGraph

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- import Static.DGToSpec

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Common.Result

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova--import Common.DocUtils

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova--import Common.Doc

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport qualified Common.OrderedMap as OMap

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaimport Data.List

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaimport Data.Graph.Inductive.Graph

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport qualified Data.Map as Map

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport Comorphisms.LogicGraph

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Proofs.EdgeUtils

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Proofs.StatusUtils

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport Proofs.AbstractState

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova-- import Proofs.BatchProcessing

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport Logic.Grothendieck

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Logic.Comorphism

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport Logic.Logic

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaimport qualified Logic.Prover as P

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport Syntax.AS_Library

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaimport Control.Concurrent

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Control.Concurrent.MVar

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport System.Posix.Signals

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaimport System.IO

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- apply comorphisms

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovashellTranslate :: String -> Sh CMDLState ()

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovashellTranslate

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova = shellComWith cTranslate False False "translate"

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova-- select a prover

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovashellProver :: String -> Sh CMDLState ()

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovashellProver

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova = shellComWith cProver False False "prover"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | select comorphisms

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovacTranslate::String -> CMDLState -> IO CMDLState

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovacTranslate input state =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case proveState state of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- nothing selected !

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing ->return state {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova errorMsg="Nothing selected"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just pS ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- parse the comorphism name

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova case lookupComorphism_in_LG $ trim input of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result _ Nothing -> return state {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova errorMsg = "Wrong comorphism name"

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result _ (Just cm) ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova do

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova case cComorphism pS of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- no comorphism used before

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova return $ register2history ("translate "++input) $

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova addToHistory (CComorphismChange $ cComorphism pS)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova state {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova proveState = Just pS {

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova cComorphism = Just cm

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova Just ocm ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova return $ register2history ("translate "++input) $

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova addToHistory (CComorphismChange $ cComorphism pS)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova state {

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova proveState = Just pS {

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova cComorphism = compComorphism ocm cm

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetProversCMDLautomatic::[AnyComorphism]->[(G_prover,AnyComorphism)]

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovagetProversCMDLautomatic = foldl addProvers []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova where addProvers acc cm =

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova case cm of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Comorphism cid -> acc ++

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova foldl (\ l p ->

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova if P.hasProverKind

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova P.ProveCMDLautomatic p

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova then (G_prover (targetLogic cid)

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova p,cm):l

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else l)

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova []

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova (provers $ targetLogic cid)

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaaddToHistory :: UndoRedoElem -> CMDLState -> CMDLState

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovaaddToHistory elm state =

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova case proveState state of

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova Nothing -> state

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova Just pS ->

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova let hist = historyList pS

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova uhist = fst hist

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova rhist = snd hist

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova in state {

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova proveState = Just pS {

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova historyList = (elm:uhist,rhist)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova }

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova }

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova-- | select a prover

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovacProver::String -> CMDLState -> IO CMDLState

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovacProver input state =

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova do

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova -- trimed input

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova let inp = trim input

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case proveState state of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> return state {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova errorMsg = "Nothing selected"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just pS ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- check that some theories are selected

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case elements pS of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova [] -> return state {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova errorMsg="Nothing selected"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (Element z _):_ ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- see if any comorphism was used

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case cComorphism pS of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- if none use the theory of the first selected node

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- to find possible comorphisms

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing-> case find (\(y,_)->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (getPName y)==inp) $

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova getProversCMDLautomatic $

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova findComorphismPaths logicGraph $

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sublogicOfTh $ theory z of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> return state {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova errorMsg="No applicable prover with"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++" this name found"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just (p,_)->return $ register2history

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ("prover "++input) $

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova addToHistory (ProverChange $

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova prover pS)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova state {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova proveState=Just pS {prover = Just p }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- if yes, use the comorphism to find a list

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- of provers

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just x ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case find (\(y,_)-> (getPName y)==inp)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova $ getProversCMDLautomatic [x] of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case find (\(y,_) ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (getPName y)==inp) $

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova getProversCMDLautomatic $

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova findComorphismPaths logicGraph $

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sublogicOfTh $ theory z of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> return state {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova errorMsg="No applicable prover with"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++" this name found"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just (p,nCm@(Comorphism cid))->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova return$ register2history ("prover " ++ input) $

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova addToHistory (ProverChange $ prover pS)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova state {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova errorMsg="Prover can't be used with the "

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++"comorphism selected using translate"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++" command. Using comorphism : "

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ language_name cid

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , proveState = Just pS {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova cComorphism=Just nCm

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ,prover = Just p

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just (p,_) -> return $ register2history ("prover "++input)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova $ addToHistory (ProverChange $ prover pS)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova state {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova proveState = Just pS {

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova prover = Just p

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | Given a proofstatus the function does the actual call of the

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- prover

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaproveNode ::

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova --use theorems is subsequent proofs

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Bool ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- save problem file for each goal

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Bool ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- Tactic script

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova String ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- proofState of the node that needs proving

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- all theorems, goals and axioms should have

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- been selected before,but the theory should have

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- not beed recomputed

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova CMDLProofAbstractState->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- selected prover, if non one will be automatically

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- selected

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Maybe G_prover ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- selected comorphism, if non one will be automatically

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- selected

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Maybe AnyComorphism ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova MVar (Maybe ThreadId) ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova MVar (Maybe CMDLProofAbstractState) ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova MVar LibEnv ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova LIB_NAME ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- returns an error message if anything happen

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova IO String

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaproveNode useTh save2File sTxt ndpf mp mcm mThr mSt mlbE libname

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova =case ndpf of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Element pf_st nd ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova do

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- recompute the theory (to make effective the selected axioms,

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- goals)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova st <- recalculateSublogicAndSelectedTheory pf_st

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- compute a prover,comorphism pair to be used in preparing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- the theory

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova p_cm@(_,acm)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova <-case mcm of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> lookupKnownProver st P.ProveCMDLautomatic

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just cm' ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case mp of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing-> lookupKnownProver st P.ProveCMDLautomatic

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just p' -> return (p',cm')

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- try to prepare the theory

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova prep <- case prepareForProving st p_cm of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result _ Nothing ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova do

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova p_cm'@(_,acm') <-

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova lookupKnownProver st P.ProveCMDLautomatic

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova return $ case prepareForProving st p_cm' of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result _ Nothing -> Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result _ (Just sm)-> Just (sm,acm')

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result _ (Just sm) -> return $ Just (sm,acm)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case prep of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- theory could not be computed

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> do

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova return "No suitable prover and comorphism found"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just (G_theory_with_prover lid1 th p, cmp)->

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova case P.proveCMDLautomaticBatch p of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> do

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova return "Error obtaining the prover"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just fn ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova do

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- mVar to poll the prover for results

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova answ <- newMVar (return [])

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let st' = st { proverRunning= True}

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- store initial input of the prover

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova swapMVar mSt $ Just $ Element st' nd

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova {- putStrLn ((theoryName st)++"\n"++

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (showDoc sign "") ++

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova show (vsep (map (print_named lid1)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova $ P.toNamedList sens))) -}

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case selectedGoals st' of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova [] -> return "No goals selected. Nothing to prove"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova _ ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova do

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova tmp <-fn useTh

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova save2File

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova answ

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (theoryName st)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (P.Tactic_script sTxt)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova th

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova swapMVar mThr $ Just $ fst tmp

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova pollForResults lid1 cmp (snd tmp) answ mSt []

swapMVar mThr $ Nothing

lbEnv <- readMVar mlbE

state <- readMVar mSt

case state of

Nothing -> return []

Just state' ->

do

lbEnv' <- addResults lbEnv libname state'

swapMVar mSt Nothing

swapMVar mlbE lbEnv'

return []

pollForResults :: (Logic lid sublogics basic_spec sentence

symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree) =>

lid ->

AnyComorphism ->

MVar () ->

MVar (Result [P.Proof_status proof_tree]) ->

MVar (Maybe CMDLProofAbstractState) ->

[P.Proof_status proof_tree] ->

IO ()

pollForResults lid acm mStop mData mState done

=do

let toPrint ls=map(\x->let txt = "Goal "++(P.goalName x)++" is "

in case P.goalStatus x of

P.Open ->txt++"still open."

P.Disproved->txt++"disproved."

P.Proved _ ->txt++"proved.") ls

d <- takeMVar mData

case d of

Result _ Nothing ->

do

tmp <- tryTakeMVar mStop

case tmp of

Just () ->

do

t <- readMVar mData

case t of

Result _ (Just _) ->

do

putMVar mStop ()

pollForResults lid acm mStop mData mState done

Result _ Nothing ->

return ()

Nothing -> pollForResults lid acm mStop mData mState done

Result _ (Just d') ->

do

let d'' = nub d'

l = d'' \\ done

ls = toPrint l

smth <- readMVar mState

case smth of

Nothing ->

do

tmp <- tryTakeMVar mStop

case tmp of

Just () -> return ()

Nothing -> pollForResults lid acm mStop mData mState done

Just (Element st node) ->

do

putStrLn $ prettyPrintList ls

swapMVar mState $Just $Element (markProved acm lid l st) node

tmp <- tryTakeMVar mStop

case tmp of

Just () -> return ()

Nothing -> pollForResults lid acm mStop mData mState

(done++l)

-- | inserts the results of the proof in the development graph

addResults :: LibEnv

-> LIB_NAME

-> CMDLProofAbstractState

-> IO LibEnv

addResults lbEnv libname ndps

=case ndps of

Element ps' node ->

do

-- inspired from Proofs/InferBasic.hs

-- and GUI/ProofManagement.hs

let ps'' = ps' {

proverRunning = False }

case theory ps'' of

G_theory lidT sigT indT sensT _ ->

do

gMap <-coerceThSens (logicId ps'') lidT

"ProveCommands last coerce"

(goalMap ps'')

let nwTh = G_theory lidT sigT indT (Map.union sensT gMap) 0

dGraph = lookupDGraph libname lbEnv

(_,oldContents) =

labNode' (safeContextDG "PGIP.ProveCommands"

dGraph node)

newNodeLab = oldContents {dgn_theory = nwTh}

(nextDGraph,changes) =

updateWithOneChange (SetNodeLab

(error "addResults")

(node,newNodeLab)) dGraph []

rules = []

nextHistoryElem = (rules, changes)

return $ mkResultProofStatus libname lbEnv nextDGraph

nextHistoryElem

-- | Signal handler that stops the prover from running

-- when SIGINT is send

sigIntHandler :: MVar (Maybe ThreadId) ->

MVar LibEnv ->

MVar (Maybe CMDLProofAbstractState) ->

ThreadId ->

MVar LibEnv ->

LIB_NAME ->

IO ()

sigIntHandler mthr mlbE mSt thr mOut libname

= do

-- print a message

-- ? shellputStr ! should be used !

putStrLn "Prover stopped."

-- check if the prover is runnig

tmp <- readMVar mthr

case tmp of

Nothing -> return ()

Just sm -> killThread sm

-- kill the prove/prove-all thread

killThread thr

-- update LibEnv with intermidiar results !?

lbEnv <- readMVar mlbE

st <- readMVar mSt

case st of

Nothing ->

do

putMVar mOut lbEnv

return ()

Just st' ->

do

lbEnv' <- addResults lbEnv libname st'

-- add to the output mvar results until now

putMVar mOut lbEnv'

return ()

proveLoop :: MVar LibEnv ->

MVar (Maybe ThreadId) ->

MVar (Maybe CMDLProofAbstractState) ->

MVar LibEnv ->

CMDLProveState ->

CMDLDevGraphState ->

[CMDLProofAbstractState] ->

IO ()

proveLoop mlbE mThr mSt mOut pS pDgS ls

= case ls of

-- we are done

[] -> do

nwLbEnv <- readMVar mlbE

putMVar mOut nwLbEnv

return ()

x: l ->

do

let nodeName x' = case x' of

Element _ t -> case find(\(n,_)-> n==t)

$ getAllNodes pDgS of

Nothing -> "Unkown node"

Just (_,ll) ->

getDGNodeName ll

putStrLn ("Analyzing node " ++ nodeName x)

err <- proveNode (useTheorems pS)

(save2file pS)

(script pS)

x

(prover pS)

(cComorphism pS)

mThr

mSt

mlbE

(ln pDgS)

case err of

[] -> proveLoop mlbE mThr mSt mOut pS pDgS l

_ -> do

putStrLn err

proveLoop mlbE mThr mSt mOut pS pDgS l

parseElements :: ActionType -> [String] -> GoalAxm

-> [CMDLProofAbstractState]

-> ([CMDLProofAbstractState],[ProofStatusChange])

-> ([CMDLProofAbstractState],[ProofStatusChange])

parseElements action gls gls_axm elems (acc1,acc2)

= case elems of

[] -> (acc1,acc2)

(Element st nb):ll ->

let allgls = case gls_axm of

TypeGoal -> OMap.keys $ goalMap st

TypeAxm -> case theory st of

G_theory _ _ _ aMap _ ->

OMap.keys aMap

selgls = case gls_axm of

TypeGoal -> selectedGoals st

TypeAxm -> includedAxioms st

fn' x y = x==y

fn ks x = case find (fn' x)$ks of

Just _ ->

case action of

ActionDel -> False

_ -> True

Nothing ->

case action of

ActionDel -> True

_ -> False

gls' = case action of

ActionDelAll -> []

ActionDel -> filter (fn selgls) gls

ActionSetAll -> allgls

ActionSet -> filter (fn allgls) gls

ActionAdd ->

nub $ (selgls)++ filter (fn allgls) gls

nwelm = Element (st { selectedGoals = gls' }) nb

in parseElements action gls gls_axm ll (nwelm:acc1,

(GoalsChange (selectedGoals st) nb):acc2)

-- | A general function that implements the actions of setting,

-- adding or deleting goals or axioms from the selection list

cGoalsAxmGeneral :: String -> ActionType -> GoalAxm ->

String ->CMDLState

-> IO CMDLState

cGoalsAxmGeneral name action gls_axm input state

= case proveState state of

Nothing -> return state {errorMsg = "Nothing selected"}

Just pS ->

case elements pS of

[] -> return state{errorMsg = "Nothing selected"}

ls ->

do

let gls = words input

let (ls',hist) = parseElements action gls

gls_axm

ls ([],[])

return $ register2history (name++input) $

addToHistory (ListChange hist)

state {proveState = Just pS {

elements = ls'

}

}

-- | Proves only selected goals from all nodes using selected

-- axioms

cProve::String -> CMDLState-> IO CMDLState

cProve name state

= case proveState state of

Nothing -> return state {errorMsg = "Nothing selected"}

Just pS ->

case devGraphState state of

Nothing -> return state{errorMsg="No library loaded"}

Just dgS ->

do

case elements pS of

[] -> return state{errorMsg="Nothing selected"}

ls ->

do

--create inital mVars to comunicate

mlbEnv <- newMVar $ libEnv dgS

mSt <- newMVar Nothing

mThr <- newMVar Nothing

mW <- newEmptyMVar

-- fork

thrID <- forkIO(proveLoop mlbEnv mThr mSt mW pS dgS ls)

-- install the handler that waits for SIG_INT

installHandler sigINT (Catch $

sigIntHandler mThr mlbEnv mSt thrID mW (ln dgS)

) Nothing

-- block and wait for answers

answ <- takeMVar mW

let nwDgS = dgS {

libEnv = answ

}

let nwls=concatMap(\(Element _ x) ->

selectANode x nwDgS) ls

hist=concatMap(\(Element stt x) ->

(AxiomsChange (includedAxioms stt) x):

(GoalsChange (selectedGoals stt) x):

[]) ls

return $ register2history name $

addToHistory (ProveChange (libEnv dgS) hist)

state {

devGraphState = Just nwDgS

,proveState = Just pS {

elements = nwls

}

}

-- | Proves all goals in the nodes selected using all axioms and

-- theorems

cProveAll::CMDLState ->IO CMDLState

cProveAll state

= case proveState state of

Nothing -> return state {errorMsg = "Nothing selected" }

Just pS ->

do

case elements pS of

[] -> return state{errorMsg="Nothing selected"}

ls ->

do

let ls' = map (\(Element st nb) ->

case theory st of

G_theory _ _ _ aMap _ ->

Element

(st {

selectedGoals = OMap.keys $

goalMap st,

includedAxioms = OMap.keys aMap,

includedTheorems = OMap.keys $

goalMap st

}) nb ) ls

let nwSt = state {

proveState = Just pS {

elements = ls'

}

}

cProve "prove-all " nwSt

-- | Sets the use theorems flag of the interface

cSetUseThms :: String->Bool -> CMDLState -> IO CMDLState

cSetUseThms name val state

= case proveState state of

Nothing -> return state {errorMsg = "Norhing selected"}

Just pS ->

do

return$ register2history name $

addToHistory (UseThmChange $ useTheorems pS)

state {

proveState = Just pS {

useTheorems = val

}

}

-- | Sets the save2File value to either true or false

cSetSave2File :: String->Bool -> CMDLState -> IO CMDLState

cSetSave2File name val state

= case proveState state of

Nothing -> return state {errorMsg = "Nothing selected"}

Just ps ->

do

return $register2history name $

addToHistory (Save2FileChange $ save2file ps)

state {

proveState = Just ps {

save2file = val

}

}

-- | Function to signal the interface that the script has ended

cEndScript :: CMDLState -> IO CMDLState

cEndScript state

= case proveState state of

Nothing -> return state {errorMsg = "Nothing selected"}

Just ps ->

case loadScript ps of

False -> return state {errorMsg = "No previous call of "

++ "begin-script"

}

True ->

do

let nwSt= state {

proveState = Just ps {

loadScript = False

}

}

return $register2history "end-script "$

addToHistory (LoadScriptChange $ loadScript ps) nwSt

-- | Function to signal the interface that a scrips starts so it should

-- not try to parse the input

cStartScript :: CMDLState-> IO CMDLState

cStartScript state

= do

case proveState state of

Nothing -> return state {errorMsg="Nothing selected"}

Just ps ->

return $register2history "begin-script" $

addToHistory (LoadScriptChange $ loadScript ps)

$addToHistory (ScriptChange $ script ps)

state {

proveState = Just ps {

loadScript = True

}

}

cTimeLimit :: String -> CMDLState-> IO CMDLState

cTimeLimit input state

= case proveState state of

Nothing -> return state {errorMsg="Nothing selected"}

Just ps ->

case checkIntString input of

False -> return state

{errorMsg="Please insert a number of seconds"}

True ->

do

case isInfixOf "Time Limit: " $ script ps of

True -> return state {errorMsg="Time limit already set"}

False->

return $ register2history ("set time-limit "++input)

$ addToHistory (ScriptChange $ script ps)

state {

proveState = Just ps {

script = ("Time Limit: " ++ input

++"\n"++ (script ps))

}

}

shellTimeLimit :: String -> Sh CMDLState ()

shellTimeLimit

= shellComWith cTimeLimit False False "set time-limit"

shellSelectAxms :: String -> Sh CMDLState ()

shellSelectAxms

= shellComWith (cGoalsAxmGeneral "set axioms " ActionSet TypeAxm)

False False "set axioms"

shellSetAxmsAll :: Sh CMDLState ()

shellSetAxmsAll

= shellComWithout (cGoalsAxmGeneral "set-all axioms "

ActionSetAll TypeAxm "")

False False "set-all axioms"

shellUnselectAxms :: String -> Sh CMDLState ()

shellUnselectAxms

= shellComWith (cGoalsAxmGeneral "del axioms " ActionDel TypeAxm)

False False "del axioms"

shellUnselectAxmsAll :: Sh CMDLState ()

shellUnselectAxmsAll

= shellComWithout (cGoalsAxmGeneral "del-all axioms "

ActionDelAll TypeAxm "")

False False "del-all axioms"

shellAddAxms :: String -> Sh CMDLState ()

shellAddAxms

= shellComWith (cGoalsAxmGeneral "add axioms" ActionAdd TypeAxm )

False False "add axioms"

shellSelectGoals :: String -> Sh CMDLState ()

shellSelectGoals

= shellComWith (cGoalsAxmGeneral "set goals " ActionSet TypeGoal )

False False "set goals"

shellSetGoalsAll :: Sh CMDLState ()

shellSetGoalsAll

= shellComWithout (cGoalsAxmGeneral "set-all goals "

ActionSetAll TypeGoal "")

False False "set-all goals"

shellUnselectGoals:: String -> Sh CMDLState ()

shellUnselectGoals

= shellComWith (cGoalsAxmGeneral "del goals " ActionDel TypeGoal )

False False "del goals"

shellUnselectGoalsAll :: Sh CMDLState ()

shellUnselectGoalsAll

= shellComWithout (cGoalsAxmGeneral "del-all goals " ActionDelAll

TypeGoal "") False False "del-all goals"

shellAddGoals :: String -> Sh CMDLState ()

shellAddGoals

= shellComWith (cGoalsAxmGeneral "add goals " ActionAdd TypeGoal)

False False "add goals"

shellUseThms :: Sh CMDLState ()

shellUseThms

= shellComWithout (cSetUseThms "set include-theorems true" True)

False False "set include-theorems true"

shellDontUseThms :: Sh CMDLState ()

shellDontUseThms

= shellComWithout (cSetUseThms "set include-theorems false" False)

False False "set include-theorems false"

shellSave2File :: Sh CMDLState ()

shellSave2File

= shellComWithout (cSetSave2File "set save-prove-to-file true" True)

False False "set save-prove-to-file true"

shellDontSave2File :: Sh CMDLState ()

shellDontSave2File

= shellComWithout (cSetSave2File "set save-prove-to-file false" False)

False False "set save-prove-to-file false"

shellBeginScript :: Sh CMDLState ()

shellBeginScript

= shellComWithout cStartScript False False "begin-script"

shellProve :: Sh CMDLState ()

shellProve

= shellComWithout (cProve "prove ") False False "prove"

shellProveAll :: Sh CMDLState ()

shellProveAll

= shellComWithout cProveAll False False "prove-all"

shellEndScript :: Sh CMDLState ()

shellEndScript

= shellComWithout cEndScript False True "end-script"