import Syntax.AS_Library

import Static.AnalysisLibrary

import Static.GTheory

import Static.DevGraph

import Static.PrintDevGraph

import Driver.Options

import qualified Data.Map as Map

import Common.Doc

import Common.AS_Annotation

import System.Environment

-- CASL things

import Data.Maybe

import Common.Id as Id

import qualified Common.OrderedMap as OMap

import Common.AS_Annotation as Anno

import Common.Result

import Common.ResultT

import Common.ExtSign

import Logic.Coerce

import CASL.Logic_CASL

import CASL.AS_Basic_CASL

import CASL.Sign

import Comorphisms.LogicGraph

import Static.AnalysisLibrary

-- DG things :)

import Proofs.Global

import Proofs.EdgeUtils

import Proofs.StatusUtils

import Data.Graph.Inductive.Graph

import Static.DGToSpec

process :: FilePath -> IO (Maybe (LIB_NAME, LibEnv))

process = anaLib defaultHetcatsOpts

printLibEnv :: LibEnv -> Doc

printLibEnv le = vsep $ map (printLibrary le) $ Map.toList le

{- ln -s sample-ghci-script .ghci and call "make ghci" -}

-- sample code

getDevGraph :: FilePath -> IO DGraph

getDevGraph fname = do

res <- process fname

case res of

Nothing -> error "getDevGraph: process"

Just (ln, lenv) -> case Map.lookup ln lenv of

Nothing -> error "getDevGraph: lookup"

Just dg -> return dg

main :: IO()

main = do

files <- getArgs

mapM_ process files

return ()

{- Test functions for CASL signature -}

proceed fname = do

anaSourceFile logicGraph defaultHetcatsOpts emptyLibEnv fname

-- read in a CASL file and return the basic theory

getCASLSigSens :: String -- filename

-> String -- name of spec

-> IO (CASLSign,[(String, CASLFORMULA)])

getCASLSigSens fname sp = do

Result _ res <- runResultT $ proceed fname

case res of

Just (ln,lenv) ->

let dg = lookupDGraph ln lenv

SpecEntry (_,_,_,NodeSig node _) =

case Map.lookup (Id.mkSimpleId sp) $ globalEnv dg of

Just x -> x

_ -> error ("Specification "++sp++" not found")

in

case match node (dgBody dg) of

(Just ctx,_) ->

case dgn_theory $ lab' ctx of

G_theory { gTheoryLogic = lid, gTheorySign = gSig, gTheorySens = gSens } ->

case (coerceSign lid CASL "" $ gSig,

coerceThSens lid CASL "" $ gSens) of

(Just sig,Just sens) ->

return (plainSign sig,

map (\(x,y) -> (x,Anno.sentence y)) $ OMap.toList sens)

_ -> error "Not a CASL sig"

_ -> error "Node 1 no in development graph"

Nothing -> error "Error occured"

{- myTest for globDecomp(or more possiblely for removeContraryChanges

from Proofs/StatusUtils.hs -}

{- try to print the DGChanges list before and after executing

removeContraryChanges, in order to see what exactly is going on -}

myTest :: IO()

myTest = do

res<-process "../CASL-lib/Basic/RelationsAndOrders.casl"

-- not ok with "RelationsAndOrders.casl " :(

case res of

Nothing -> error "myTest"

Just (ln, lenv) -> do

{- (edges2, dgchanges2) <- myGlobal ln 2 lenv

putStrLn $ show dgchanges

-- print the DGChanges before execusion

putStrLn $ "!!!!!The DGChanges before excecuting of " ++

"removeContraryChanges by the third excecuting of " ++

"GlobalDecomposition!!!!!"

putStrLn $ show $ myPrintShow dgchanges2

putStrLn $ "!!!!!the DGChanges afterwards by the third excecuting"

++ " of GlobalDecomposition!!!!!"

putStrLn $ show $ myPrintShow $

-- removeContraryChanges dgchanges2

putStrLn $ show $ myPrintEdges edges2

-}

(edges3, dgchanges3) <- myGlobal ln 3 lenv

putStrLn $ "The global thm Edges before executing globDecomp for " ++

"the fourth time"

putStrLn $ show $ myPrintEdges edges3

{- putStrLn $ "!!!!!The DGChanges before excecuting of " ++

"removeContraryChanges by the fouth excecuting of " ++

"GlobalDecomposition!!!!!"

putStrLn $ show $ myPrintShow dgchanges3

-}

putStrLn $ "!!!!!the DGChanges by the fouth excecuting of " ++

"GlobalDecomposition: !!!!!"

putStrLn $ show $ myPrintDGChanges dgchanges3

putStrLn $ show $ myPrintDGChanges $ removeContraryChanges dgchanges3

{- putStrLn $ show (removeContraryChanges dgchanges)

-- print after...

llllll <- countD (removeContraryChanges dgchanges) 0

putStrLn $ show llllll

dgchanges4<- myGlobal ln 4 lenv

putStrLn "aaa"

-}

myPrintEdges :: [LEdge DGLinkLab] -> [String]

myPrintEdges = map edgesAux

edgesAux :: LEdge DGLinkLab -> String

edgesAux (source, target, l) = show source ++ "->" ++ show target

++ " with type" ++ show (dgl_type l)

myPrintDGChanges :: [DGChange] -> [String]

myPrintDGChanges dgs = [show dg++" "++ myPrintAux dg|dg<-dgs]

myPrintAux :: DGChange -> String

myPrintAux (DeleteEdge (_, _, dglink)) = getDGLinkType dglink

myPrintAux (InsertEdge (_, _, dglink)) = getDGLinkType dglink

myPrintAux _ = "Node"

countD :: [DGChange] -> Int -> IO Int

countD [] n = return n

countD (x:xs) n = if show x == "DeleteEdge 3->15" then countD xs (n+1)

else countD xs n

-- my simulated execusion of globDecomp

myGlobal :: LIB_NAME -> Int -> LibEnv -> IO ([LEdge DGLinkLab], [DGChange])

myGlobal ln n lenv =

let newLenv = executeGlobalDecompByNTimes n ln lenv

-- try to do n times globDecomp

dgraph = lookupDGraph ln newLenv

globalThmEdges = filter (liftE isUnprovenGlobalThm) (labEdgesDG dgraph)

(_, newHistoryElem) = globDecompAux dgraph globalThmEdges

([], [])

defEdgesToSource = myGoingIntoGTE dgraph globalThmEdges []

in do putStrLn "all the edges going into global Thm Edges"

putStrLn $ show defEdgesToSource

return (globalThmEdges , snd newHistoryElem)

-- get the DGChanges by the fourth time executing globDecomp

myGoingIntoGTE :: DGraph -> [LEdge DGLinkLab] -> [String]->[String]

myGoingIntoGTE _ [] res = res

myGoingIntoGTE dgraph ((source, _ , _) : ys) res =

let defEdgesToSource = [e | e@(_, t, l) <- labEdgesDG dgraph,

isDefEdge (dgl_type l), t == source]

in myGoingIntoGTE dgraph ys (res++(myPrintEdges defEdgesToSource))

-- execute globDecomp by n times :)

executeGlobalDecompByNTimes :: Int -> LIB_NAME -> LibEnv -> LibEnv

executeGlobalDecompByNTimes n ln lenv =

if n<0 then error "excecuteGlobalDecompByNTimes"

else if n==0 then lenv

else executeGlobalDecompByNTimes (n-1) ln $ globDecomp ln lenv