640b2adac05bb7f5e9fba064434c91852c3a72e6nd{- |

640b2adac05bb7f5e9fba064434c91852c3a72e6ndModule :$Header$

640b2adac05bb7f5e9fba064434c91852c3a72e6ndCopyright : uni-bremen and Razvan Pascanu

640b2adac05bb7f5e9fba064434c91852c3a72e6ndLicence : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

640b2adac05bb7f5e9fba064434c91852c3a72e6ndMaintainer : r.pascanu@iu-bremen.de

640b2adac05bb7f5e9fba064434c91852c3a72e6ndStability : provisional

640b2adac05bb7f5e9fba064434c91852c3a72e6ndPortability : portable

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6ndFunction that executes the script commands together with the datatypes used.

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6nd TODO :

640b2adac05bb7f5e9fba064434c91852c3a72e6nd - add comments

640b2adac05bb7f5e9fba064434c91852c3a72e6nd - implement the rest of the functions

640b2adac05bb7f5e9fba064434c91852c3a72e6nd - delete the test function

640b2adac05bb7f5e9fba064434c91852c3a72e6nd-}

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabelemodule PGIP.Commands where

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

ef685e00a47967e27d89709461728a229d762172ndimport Syntax.AS_Library

ef685e00a47967e27d89709461728a229d762172ndimport Static.AnalysisLibrary

ef685e00a47967e27d89709461728a229d762172ndimport Static.DevGraph

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Driver.Options

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.Utils

51853aa2ebfdf9903a094467e1d02099f143639daaronimport Proofs.Automatic

51853aa2ebfdf9903a094467e1d02099f143639daaronimport Proofs.Global

51853aa2ebfdf9903a094467e1d02099f143639daaronimport Proofs.Local

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Proofs.Composition

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Proofs.HideTheoremShift

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Proofs.TheoremHideShift

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Proofs.EdgeUtils

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Proofs.InferBasic

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabeleimport Common.Id

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.DocUtils

ef685e00a47967e27d89709461728a229d762172ndimport Common.Result

ef685e00a47967e27d89709461728a229d762172ndimport Data.Maybe

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Data.Graph.Inductive.Graph

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Comorphisms.LogicGraph

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive--import Proofs.InferBasic

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivedata GOAL =

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Node Id

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive | Edge Id Id

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele | LabeledEdge Id Int Id

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive deriving (Eq,Show)

ef685e00a47967e27d89709461728a229d762172nd

2a7c98db85d4969dcbe7711a5ec3264ee4fc6222yoshiki

ef685e00a47967e27d89709461728a229d762172nddata ScriptCommandParameters =

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Path [String]

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive | Formula Id

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive | Prover Id

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive | Goals [GOAL]

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive | ParsedComorphism [Id]

2a7c98db85d4969dcbe7711a5ec3264ee4fc6222yoshiki | AxiomSelectionWith [Id]

2a7c98db85d4969dcbe7711a5ec3264ee4fc6222yoshiki | AxiomSelectionExcluding [Id]

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive | Formulas [Id]

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive | ProofScript String

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive | ParamErr String

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive | NoParam

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive deriving (Eq,Show)

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivedata CmdInterpreterStatus =

ef685e00a47967e27d89709461728a229d762172nd OutputErr String

ef685e00a47967e27d89709461728a229d762172nd | CmdInitialState

ef685e00a47967e27d89709461728a229d762172nd | Env LIB_NAME LibEnv

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive | SelectedNodes [Node]

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivedata CmdInterpreterStatusID =

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive EnvID

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivedata CommandFunctionsAndParameters=

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive CommandParam ([ScriptCommandParameters]->IO [CmdInterpreterStatus]) [ScriptCommandParameters]

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive | CommandParamStatus (([ScriptCommandParameters],[CmdInterpreterStatus])-> [CmdInterpreterStatus]) [ScriptCommandParameters] [CmdInterpreterStatusID]

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx | CommandStatus ([CmdInterpreterStatus] -> [CmdInterpreterStatus]) [CmdInterpreterStatusID]

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele | CommandTest ([ScriptCommandParameters]->IO()) [ScriptCommandParameters]

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx | CommandShowStatus ([CmdInterpreterStatus] -> ()) [CmdInterpreterStatusID]

ef685e00a47967e27d89709461728a229d762172nd | CommandError

ef685e00a47967e27d89709461728a229d762172nd

ef685e00a47967e27d89709461728a229d762172nd

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxtest::([ScriptCommandParameters])->IO()

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxtest (ls) = putStrLn $ show ls

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxcommandUse::[ScriptCommandParameters]->IO [CmdInterpreterStatus]

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxcommandUse ls

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx = case ls of

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick (Path list):_ -> do

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick let file = joinWith '/' list

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick let opts = defaultHetcatsOpts

1b3225113bb6fcf326cf16af9023e381ae0ac083nd result<- anaLib opts file

1b3225113bb6fcf326cf16af9023e381ae0ac083nd case result of

1b3225113bb6fcf326cf16af9023e381ae0ac083nd Just (name,env) -> return [(Env name env)]

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick Nothing -> return [(OutputErr "Couldn't load the file specified")]

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick _ -> return [(OutputErr "Wrong parameter")]

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickcommandDgAllAuto::[CmdInterpreterStatus] -> [CmdInterpreterStatus]

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickcommandDgAllAuto arg

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick = case arg of

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick (Env x y):_ -> let result= automatic x y

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick in [(Env x result)]

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick _:l -> commandDgAllAuto l

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive [] -> [(OutputErr "Wrong parameter")]

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivecommandDgAuto :: ([ScriptCommandParameters],[CmdInterpreterStatus]) -> [CmdInterpreterStatus]

ef685e00a47967e27d89709461728a229d762172ndcommandDgAuto (param,status)

ef685e00a47967e27d89709461728a229d762172nd = case status of

ef685e00a47967e27d89709461728a229d762172nd (Env ln libEnv):_ -> case param of

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive (Goals ls):_ -> let l = getAllEdgeGoals ln libEnv ls

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive result = automaticFromList ln l libEnv

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive in [(Env ln result)]

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive _ -> [(OutputErr "Wrong parameters")]

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive _:l -> commandDgAuto (param, l)

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive [] -> [(OutputErr "Wrong parameters")]

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivecommandDgGlobSubsume::([ScriptCommandParameters],[CmdInterpreterStatus]) -> [CmdInterpreterStatus]

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelecommandDgGlobSubsume (param,status)

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele = case status of

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele (Env ln libEnv):_ -> case param of

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele (Goals ls):_ -> let l = getAllGlobalEdgeGoals ln libEnv ls

ef685e00a47967e27d89709461728a229d762172nd result = globSubsumeFromList ln l libEnv

ef685e00a47967e27d89709461728a229d762172nd in [(Env ln result)]

ef685e00a47967e27d89709461728a229d762172nd _ -> [(OutputErr "Wrong parameters")]

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele _:l -> commandDgGlobSubsume (param,l)

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele [] -> [(OutputErr "Wrong parameters")]

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelecommandDgAllGlobSubsume::[CmdInterpreterStatus] -> [CmdInterpreterStatus]

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelecommandDgAllGlobSubsume arg

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele = case arg of

81622596373177e079337e956f7a5800895443b3erikabele (Env x y):_ -> let result =(globSubsume x) y

81622596373177e079337e956f7a5800895443b3erikabele in [(Env x result)]

81622596373177e079337e956f7a5800895443b3erikabele _:l -> commandDgAllGlobSubsume l

81622596373177e079337e956f7a5800895443b3erikabele [] -> [(OutputErr "Wrong parameters")]

ef685e00a47967e27d89709461728a229d762172nd

ef685e00a47967e27d89709461728a229d762172ndcommandDgAllGlobDecomp::[CmdInterpreterStatus] -> [CmdInterpreterStatus]

ef685e00a47967e27d89709461728a229d762172ndcommandDgAllGlobDecomp arg

81622596373177e079337e956f7a5800895443b3erikabele = case arg of

81622596373177e079337e956f7a5800895443b3erikabele (Env x y):_ -> let result= (globDecomp x) y

81622596373177e079337e956f7a5800895443b3erikabele in [(Env x result)]

81622596373177e079337e956f7a5800895443b3erikabele _:l -> commandDgAllGlobDecomp l

81622596373177e079337e956f7a5800895443b3erikabele [] -> [(OutputErr "Wrong parameters")]

81622596373177e079337e956f7a5800895443b3erikabele

81622596373177e079337e956f7a5800895443b3erikabele

ef685e00a47967e27d89709461728a229d762172ndcommandDgGlobDecomp :: ([ScriptCommandParameters],[CmdInterpreterStatus]) -> [CmdInterpreterStatus]

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelecommandDgGlobDecomp (param,status)

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele = case status of

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele (Env ln libEnv):_ -> case param of

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele (Goals ls):_ -> let l = getAllGlobalEdgeGoals ln libEnv ls

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele result = globDecompFromList ln l libEnv

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele in [(Env ln result)]

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele _ -> [(OutputErr "Wrong parameters")]

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele _:l -> commandDgGlobDecomp (param,l)

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele [] -> [(OutputErr "Wrong parameters")]

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelecommandDgAllLocInfer::[CmdInterpreterStatus] -> [CmdInterpreterStatus]

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelecommandDgAllLocInfer arg

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki = case arg of

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki (Env x y):_ -> let result= (localInference x) y

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki in [(Env x result)]

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki _:l -> commandDgAllLocInfer l

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki [] -> [(OutputErr "Wrong parameters")]

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshikicommandDgLocInfer::([ScriptCommandParameters],[CmdInterpreterStatus]) -> [CmdInterpreterStatus]

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshikicommandDgLocInfer (param,status)

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki = case status of

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki (Env ln libEnv):_ -> case param of

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki (Goals ls):_ -> let l = getAllLocalEdgeGoals ln libEnv ls

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki result = localInferenceFromList ln l libEnv

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki in [(Env ln result)]

_ -> [(OutputErr "Wrong parameters")]

_:l -> commandDgLocInfer (param,l)

[] -> [(OutputErr "Wrong parameters")]

commandDgAllLocDecomp::[CmdInterpreterStatus] -> [CmdInterpreterStatus]

commandDgAllLocDecomp arg

= case arg of

(Env x y):l -> let result= (locDecomp x) y

in [(Env x result)]

_:l -> commandDgAllLocDecomp l

[] -> [(OutputErr "Wrong parameters")]

commandDgLocDecomp::([ScriptCommandParameters], [CmdInterpreterStatus])-> [CmdInterpreterStatus]

commandDgLocDecomp (param,status)

= case status of

(Env ln libEnv):_ -> case param of

(Goals ls):_ -> let l = getAllLocalEdgeGoals ln libEnv ls

result = locDecompFromList ln l libEnv

in [(Env ln result)]

_ -> [(OutputErr "Wrong parameters")]

_:l -> commandDgLocDecomp (param,l)

[] -> [(OutputErr "Wrong parameters")]

commandDgComp::([ScriptCommandParameters], [CmdInterpreterStatus]) -> [CmdInterpreterStatus]

commandDgComp (param, status)

= case status of

(Env ln libEnv):_ -> case param of

(Goals ls):_ -> let l = getAllGlobalEdgeGoals ln libEnv ls

result = compositionFromList ln l libEnv

in [(Env ln result)]

_ -> [(OutputErr "Wrong parameters")]

_:l -> commandDgComp (param, l)

[] -> [(OutputErr "Wrong parameters")]

commandDgAllComp::[CmdInterpreterStatus] -> [CmdInterpreterStatus]

commandDgAllComp arg

= case arg of

(Env x y):_ -> let result= (composition x) y

in [(Env x result)]

_:l -> commandDgAllComp l

[] -> [(OutputErr "Wrong parameters")]

commandDgCompNew::([ScriptCommandParameters],[CmdInterpreterStatus]) -> [CmdInterpreterStatus]

commandDgCompNew (param, status)

= case status of

(Env ln libEnv):_ -> case param of

(Goals ls):_ -> let l = getAllGlobalEdgeGoals ln libEnv ls

result = compositionCreatingEdgesFromList ln l libEnv

in [(Env ln result)]

_ -> [(OutputErr "Wrong parameters")]

_:l -> commandDgCompNew (param,l)

[] -> [(OutputErr "Wrong parameters")]

commandDgAllCompNew::[CmdInterpreterStatus] -> [CmdInterpreterStatus]

commandDgAllCompNew arg

= case arg of

(Env x y):_ -> let result=(compositionCreatingEdges x) y

in [(Env x result)]

_:l -> commandDgAllCompNew l

[] -> [(OutputErr "Wrong parameters")]

commandDgHideThm::([ScriptCommandParameters],[CmdInterpreterStatus]) -> [CmdInterpreterStatus]

commandDgHideThm (param, status)

= case status of

(Env ln libEnv):_ -> case param of

(Goals ls):_ -> let l = getAllHidingThmGoals ln libEnv ls

result = automaticHideTheoremShiftFromList ln l libEnv

in [(Env ln result)]

_ -> [(OutputErr "Wrong parameters")]

_:l -> commandDgHideThm (param,l)

[] -> [(OutputErr "Wrong parameters")]

commandDgAllHideThm::[CmdInterpreterStatus] -> [CmdInterpreterStatus]

commandDgAllHideThm arg

= case arg of

(Env x y):_ -> let result= (automaticHideTheoremShift x) y

in [(Env x result)]

_:l -> commandDgAllHideThm l

[] -> [(OutputErr "Wrong parameters")]

commandDgAllThmHide::[CmdInterpreterStatus] -> [CmdInterpreterStatus]

commandDgAllThmHide arg

= case arg of

(Env x y):_ -> let result=(theoremHideShift x) y

in [(Env x result)]

_:l -> commandDgAllThmHide l

[] -> [(OutputErr "Wrong parameters")]

commandDgAllInferBasic::[CmdInterpreterStatus] -> [CmdInterpreterStatus]

commandDgAllInferBasic arg

= case arg of

(Env x y):_ -> let dgraph = lookupDGraph x y

lno = labNodes dgraph

ls = extractDGNodeLab lno

ll = filter hasOpenGoals ls

-- result = applyInferBasic ll x y

in (Env x y):(SelectedNodes (extractNode lno)):[]

_:l -> commandDgAllInferBasic l

[] -> [(OutputErr "Wrong parameters")]

extractDGNodeLab :: [LNode DGNodeLab] -> [DGNodeLab]

extractDGNodeLab ls =

case ls of

[] -> []

(_,r):l -> r:(extractDGNodeLab l)

extractNode :: [LNode DGNodeLab] -> [Node]

extractNode ls =

case ls of

[] -> []

(r,_):l -> r:(extractNode l)

commandShowTheory :: [CmdInterpreterStatus] -> ()

commandShowTheory arg

= case arg of

(Env x y):l -> case l of

(SelectedNodes ll):_ -> let dgraph = lookupDGraph x y

in printAllTheory ll dgraph

_:ls -> commandShowTheory ((Env x y):ls)

[] -> ()

(SelectedNodes ll):l -> case l of

(Env x y):_ -> let dgraph = lookupDGraph x y

in printAllTheory ll dgraph

_:ls -> commandShowTheory ((SelectedNodes ll):ls)

[] -> ()

printAllTheory:: [Node] ->DGraph -> ()

printAllTheory ls dgraph

= case ls of

x:l ->

let dgnode = lab' (context dgraph x)

theTh = fromJust $ getNodeByNumber (labNodes dgraph) x

str = showDoc theTh "\n"

-- let thName = showName (dgn_name x)

-- putStr ( "\n\n"++str++"\n")

in printAllTheory l dgraph

[] -> ()

getNodeByNumber :: [LNode DGNodeLab] -> Node -> Maybe G_theory

getNodeByNumber ls x = case ls of

(xx,(DGNode _ theTh _ _ _ _ _)):l -> if (x==xx) then (Just theTh)

else getNodeByNumber l x

_:l -> getNodeByNumber l x

[] -> Nothing

commandDgInferBasic::([ScriptCommandParameters],[CmdInterpreterStatus]) -> [CmdInterpreterStatus]

commandDgInferBasic (param, status)

= case status of

(Env ln libEnv):_ -> case param of

(Goals ls):_ -> let dgraph = lookupDGraph ln libEnv

lno = labNodes dgraph

ll = getAllNodeGoals lno ls

-- result = applyInferBasic ll ln libEnv

in (Env ln libEnv):(SelectedNodes ll):[]

_ -> [(OutputErr "Wrong parameters")]

_:l -> commandDgInferBasic (param, l)

[] -> [(OutputErr "Wrong parameters")]

--applyInferBasic:: [Node] -> LIB_NAME -> LibEnv -> LibEnv

--applyInferBasic ll ln libEnv

-- = case ll of

-- x:l -> do

-- (Result _ r) <- basicInferenceNode False logicGraph (ln,x) ln libEnv

-- applyInferBasic l ln (fromJust r)

-- [] -> libEnv

getAllNodeGoals :: [LNode DGNodeLab]->[GOAL] -> [Node]

getAllNodeGoals lno ls

= case ls of

(Edge _ _):l -> getAllNodeGoals lno l

(LabeledEdge _ _ _):l -> getAllNodeGoals lno l

(Node x):l -> (fromJust $ findNodeNumber lno x):(getAllNodeGoals lno l)

[] -> []

-- | The 'findNodeNumber' function, given the Id of a node searches a list of LNode and returns the index of the node

findNodeNumber :: [LNode DGNodeLab] -> Id -> Maybe Node

findNodeNumber ls x

= case ls of

[] -> Nothing

(nb,label):l -> if (( getDGNodeName label)==(show x)) then Just nb else findNodeNumber l x

-- | The 'isEdgeBetween' function checks for two given Node and an edge if the edge is between those nodes

isEdgeBetween:: Node -> Node -> LEdge DGLinkLab -> Bool

isEdgeBetween x y (currentEdgeX,currentEdgeY, currentEdgeLab) =

if ((x==currentEdgeX)&&(y==currentEdgeY)) then True else False

-- | The 'getAllEdges' function, given the Id of two nodes finds out all edges between those nodes

getAllEdges:: LIB_NAME->LibEnv->Id -> Id -> [LEdge DGLinkLab]

getAllEdges ln libEnv x y =

let dgraph = lookupDGraph ln libEnv

lno = labNodes dgraph

xNb = fromJust $ findNodeNumber lno x

yNb = fromJust $ findNodeNumber lno y

in filter (isEdgeBetween xNb yNb) (labEdges dgraph)

selectLabeledEdge:: Int-> [LEdge DGLinkLab] -> Maybe (LEdge DGLinkLab)

selectLabeledEdge x ls =

case x of

0 -> case ls of

[] -> Nothing

e:l-> Just e

n -> case ls of

[] -> Nothing

e:l-> selectLabeledEdge (n-1) l

getAllEdgeGoals :: LIB_NAME->LibEnv ->[GOAL]->[LEdge DGLinkLab]

getAllEdgeGoals ln libEnv ls =

(getAllGlobalEdgeGoals ln libEnv ls)++(getAllLocalEdgeGoals ln libEnv ls);

-- | The 'getAllGlobalEdgeGoals' function, given the list of goals extracts only the globalUnprovenThm from all the edges in the list

getAllGlobalEdgeGoals:: LIB_NAME->LibEnv->[GOAL]->[LEdge DGLinkLab]

getAllGlobalEdgeGoals ln libEnv ls =

case ls of

[] -> []

(Node _):l -> getAllGlobalEdgeGoals ln libEnv l

(Edge x y):l -> let allEdges = getAllEdges ln libEnv x y

allGlobalThm = filter isUnprovenGlobalThm allEdges

in allGlobalThm ++ (getAllGlobalEdgeGoals ln libEnv l)

(LabeledEdge x thelab y):l -> let allEdges = getAllEdges ln libEnv x y

allGlobalThm = filter isUnprovenGlobalThm allEdges

theEdge = fromJust $ selectLabeledEdge thelab allGlobalThm

in theEdge: (getAllGlobalEdgeGoals ln libEnv l)

getAllLocalEdgeGoals:: LIB_NAME->LibEnv->[GOAL]->[LEdge DGLinkLab]

getAllLocalEdgeGoals ln libEnv ls =

case ls of

[] -> []

(Node _):l -> getAllGlobalEdgeGoals ln libEnv l

(Edge x y):l -> let allEdges = getAllEdges ln libEnv x y

allLocalThm = filter isUnprovenLocalThm allEdges

in allLocalThm ++ (getAllLocalEdgeGoals ln libEnv l)

(LabeledEdge x thelab y):l -> let allEdges = getAllEdges ln libEnv x y

allLocalThm = filter isUnprovenLocalThm allEdges

theEdge = fromJust $ selectLabeledEdge thelab allLocalThm

in theEdge : (getAllLocalEdgeGoals ln libEnv l)

getAllHidingThmGoals :: LIB_NAME -> LibEnv -> [GOAL] -> [LEdge DGLinkLab]

getAllHidingThmGoals ln libEnv ls =

case ls of

[] -> []

(Node _):l -> getAllHidingThmGoals ln libEnv l

(Edge x y):l -> let allEdges = getAllEdges ln libEnv x y

allHidingThm = filter isUnprovenHidingThm allEdges

in allHidingThm ++ (getAllHidingThmGoals ln libEnv l)

(LabeledEdge x thelab y):l -> let allEdges = getAllEdges ln libEnv x y

allHidingThm = filter isUnprovenHidingThm allEdges

theEdge = fromJust $ selectLabeledEdge thelab allHidingThm

in theEdge : (getAllHidingThmGoals ln libEnv l)