content: {-# OPTIONS_GHC -fno-warn-unused-imports -fno-warn-unused-binds #-}
  
  {- |
  Module      :  ./Scratch.hs
  Description :  ghci test file
  Copyright   :  (c)  C. Maeder, DFKI GmbH 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  experimental
  Portability :  non-portable (import Logic)
  
  load after calling make ghci
  -}
  
  module Main where
  
  import Syntax.AS_Library
  import Static.AnalysisLibrary
  import Static.GTheory
  import Static.DevGraph
  import Static.PrintDevGraph
  import Static.History
  import Static.ComputeTheory
  
  import Driver.Options
  import Driver.AnaLib
  
  import qualified Common.OrderedMap as OMap
  import qualified Common.Lib.MapSet as MapSet
  import Common.GlobalAnnotations
  import Common.AS_Annotation as Anno
  import Common.Result
  import Common.ResultT
  import Common.LibName
  import Common.Id as Id
  import Common.ExtSign
  import Common.Doc
  import Common.DocUtils
  
  import System.Environment
  import Data.Graph.Inductive.Graph
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Data.Maybe
  import Data.List
  
  -- Logic things
  import Logic.Coerce
  import Logic.Logic
  
  -- CASL things
  import CASL.Logic_CASL
  import CASL.AS_Basic_CASL
  import CASL.Sign
  import Comorphisms.LogicGraph
  
  -- DG things :)
  import Proofs.Global
  import Proofs.EdgeUtils
  import Proofs.StatusUtils
  import Proofs.Automatic
  
  import Static.SpecLoader
  
  myHetcatsOpts :: HetcatsOpts
  myHetcatsOpts = defaultHetcatsOpts { libdirs = ["../Hets-lib"] }
  
  process :: FilePath -> IO (Maybe (LibName, LibEnv))
  process = anaLib myHetcatsOpts
  
  -- 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 ()
  
  
  proceed :: FilePath -> ResultT IO (LibName, LibEnv)
  proceed = proceed' myHetcatsOpts
  
  
  -- Test functions for CASL signature
  
  -- 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
    res <- getSigSens myHetcatsOpts CASL fname sp
    let f z = (senAttr z, sentence z)
    return (sigsensSignature res, map f $ sigsensNamedSentences res)
  
  
  {- 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 "../Hets-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
           print dgchanges
           -- print the DGChanges before execusion
           putStrLn $ "!!!!!The DGChanges before excecuting of " ++
                        "removeContraryChanges by the third excecuting of " ++
                        "GlobalDecomposition!!!!!"
           print $ myPrintShow dgchanges2
           putStrLn $ "!!!!!the DGChanges afterwards by the third excecuting"
                      ++ " of GlobalDecomposition!!!!!"
           print $ myPrintShow $
           -- removeContraryChanges dgchanges2
           print $ myPrintEdges edges2
  -}
           (edges3, dgchanges3) <- myGlobal ln 3 lenv
           putStrLn $ "The global thm Edges before executing globDecomp for " ++
                      "the fourth time"
           print $ myPrintEdges edges3
  {-
           putStrLn $ "!!!!!The DGChanges before excecuting of " ++
                      "removeContraryChanges by the fouth excecuting of " ++
                      "GlobalDecomposition!!!!!"
           print $ myPrintShow dgchanges3
  -}
           putStrLn $ "!!!!!the DGChanges by the fouth excecuting of " ++
                      "GlobalDecomposition: !!!!!"
           print $ myPrintDGChanges dgchanges3
           print $ myPrintDGChanges $ removeContraryChanges dgchanges3
  {-
           print (removeContraryChanges dgchanges)
           -- print after...
           print $ countD $ removeContraryChanges dgchanges
           dgchanges4<- myGlobal ln 4 lenv
           putStrLn "aaa"
  -}
  
  myPrintEdges :: [LEdge DGLinkLab] -> [String]
  myPrintEdges = map showLEdge
  
  showDGChange :: DGChange -> String
  showDGChange c = showDoc c ""
  
  myPrintDGChanges :: [DGChange] -> [String]
  myPrintDGChanges = map showDGChange
  
  countD :: [DGChange] -> Int
  countD = length . filter (isPrefixOf "delete edge" . showDGChange)
  
  -- my simulated execusion of globDecomp
  myGlobal :: LibName -> Int -> LibEnv -> IO ([LEdge DGLinkLab], [DGChange])
  myGlobal ln n lenv = do
      let newLenv = executeGlobalDecompByNTimes n ln lenv
          -- try to do n times globDecomp
          dgraph = lookupDGraph ln newLenv
          globalThmEdges = filter (liftE isUnprovenGlobalThm) (labEdgesDG dgraph)
          ngraph = foldl globDecompAux dgraph globalThmEdges
          defEdgesToSource = myGoingIntoGTE dgraph globalThmEdges []
      putStrLn "all the edges going into global Thm Edges"
      print defEdgesToSource
      return (globalThmEdges,
               flatHistory $ snd $ splitHistory dgraph ngraph)
              -- get the DGChanges by 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 -> LibName -> LibEnv -> LibEnv
  executeGlobalDecompByNTimes n ln lenv = case compare n 0 of
    LT -> error "excecuteGlobalDecompByNTimes"
    EQ -> lenv
    GT -> executeGlobalDecompByNTimes (n - 1) ln $ globDecomp ln lenv
  