{- |
Module      :  $Header$
Description :  Import data generated by hol2hets into a DG
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  jonathan.von_schroeder@dfki.de
Stability   :  experimental
Portability :  portable

-}

module HolLight.HolLight2DG where

import Static.GTheory
import Static.DevGraph

import Static.DgUtils
import Static.History
import Static.ComputeTheory

import Logic.Logic
import Logic.Prover
import Logic.ExtSign
import Logic.Grothendieck

import Common.LibName
import Common.Id
import Common.IRI (simpleIdToIRI)
import Common.AS_Annotation
import Common.Result
import Common.Utils
import Common.SAX
import Control.Monad
import Common.Lib.Maybe
import qualified Data.ByteString.Lazy as L
import Text.XML.Expat.SAX

import HolLight.Sign
import HolLight.Sentence
import HolLight.Term
import HolLight.Logic_HolLight

import HolLight.Helper (names)

import Driver.Options

import Data.Graph.Inductive.Graph
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)

import System.Exit
import System.Directory
import System.FilePath

readTuple :: (Show a, Show b) => MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple f1 f2 = do
 expectTag True "tuple"
 t1 <- readWithTag f1 "fst"
 t2 <- readWithTag f2 "snd"
 expectTag False "tuple"
 return (t1, t2)

readWord :: MSaxState String
readWord = liftM reverse $ foldCatchLeft (\ s ->
 do
  s' <- do
   dropSpaces
   d <- getD
   case d of
     [] -> error "HolLight.readWord"
     h : xs -> case h of
       CharacterData s' -> do
         putD xs
         return s'
       _ -> debugS $ "Expected character data but instead got: " ++ show h
  return $ trimLeft (reverse $ trimLeft s') ++ s) []

readStr :: MSaxState String
readStr = readWithTag readWord "s"

readInt :: MSaxState Int
readInt = do
 w <- readWord
 return $ fromMaybe (error "HolLight.readInt") $ readMaybe w

readInt' :: MSaxState Int
readInt' = readWithTag readInt "i"

readMappedInt :: Map.Map Int a -> MSaxState a
readMappedInt m = do
 i <- readInt
 case Map.lookup i m of
  Just a -> return a
  _ -> debugS $ "readMappedInt: Integer " ++ show i ++ " not mapped"

listToTypes :: Map.Map Int HolType -> [Int] -> Maybe [HolType]
listToTypes m l = case l of
 x : xs -> case Map.lookup x m of
  Just t -> case listToTypes m xs of
   Just ts -> Just (t : ts)
   _ -> Nothing
  _ -> Nothing
 [] -> Just []

readSharedHolType :: Map.Map Int String -> Map.Map Int HolType
                      -> MSaxState (Map.Map Int HolType)
readSharedHolType sl m = do
 d <- getM
 (b, t) <- tag
 case (b, t) of
  (True, "TyApp") -> do
   (i, l) <- readTuple readInt (whileM readInt')
   case (Map.lookup i sl, listToTypes m l) of
    (Just s, Just l') -> do
     expectTag False "TyApp"
     return $ Map.insert (Map.size m + 1) (TyApp s $ reverse l') m
    (r1, r2) -> debugS $ "readSharedHolType: Couldn't build TyApp"
                        ++ " because the result of the lookup for "
                        ++ show (i, l) ++ " was " ++ show (r1, r2)
  (True, "TyVar") -> do
   i <- readInt
   case Map.lookup i sl of
    Just s -> do
     expectTag False "TyVar"
     return $ Map.insert (Map.size m + 1) (TyVar s) m
    _ -> debugS $ "readSharedHolType: Couldn't build TyVar"
                  ++ " because looking up " ++ show i
                  ++ " failed"
  _ -> do
   putM d
   debugS $ "readSharedHolType: Expected a hol type but"
            ++ " instead got following tag: " ++ show (b, t)

readParseType :: MSaxState HolParseType
readParseType = do
 (b, t) <- tag
 case (b, t) of
  (True, "Prefix") -> do
   expectTag False "Prefix"
   return Prefix
  (True, "InfixR") -> do
   i <- readInt
   expectTag False "InfixR"
   return $ InfixR i
  (True, "InfixL") -> do
   i <- readInt
   expectTag False "InfixL"
   return $ InfixL i
  (True, "Normal") -> do
   expectTag False "Normal"
   return Normal
  (True, "Binder") -> do
   expectTag False "Binder"
   return Binder
  _ -> debugS $ "readParseType: Expected a parse type but"
                ++ " instead got following tag: " ++ show (b, t)

readTermInfo :: MSaxState HolTermInfo
readTermInfo = do
 p <- readParseType
 MaybeT $ do
  v <- runMaybeT $ readTuple readWord readParseType
  case v of
   Just _ -> return $ Just $ HolTermInfo (p, v)
   _ -> return $ Just $ HolTermInfo (p, Nothing)

readSharedHolTerm :: Map.Map Int HolType -> Map.Map Int String
                      -> Map.Map Int Term -> MSaxState (Map.Map Int Term)
readSharedHolTerm ts sl m = do
 d <- getM
 (b, tg) <- tag
 case (b, tg) of
  (True, "Var") -> do
   (n, t) <- readTuple readInt readInt
   ti <- readTermInfo
   case (Map.lookup n sl, Map.lookup t ts) of
    (Just name, Just tp) -> do
     expectTag False "Var"
     return $ Map.insert (Map.size m + 1) (Var name tp ti) m
    (r1, r2) -> debugS $ "readSharedHolTerm: Couldn't build Var"
                  ++ " because the result of the lookup for "
                  ++ show (n, t) ++ " was " ++ show (r1, r2)
  (True, "Const") -> do
   (n, t) <- readTuple readInt readInt
   ti <- readTermInfo
   case (Map.lookup n sl, Map.lookup t ts) of
    (Just name, Just tp) -> do
     expectTag False "Const"
     return $ Map.insert (Map.size m + 1) (Const name tp ti) m
    (r1, r2) -> debugS $ "readSharedHolTerm: Couldn't build Const"
                  ++ " because the result of the lookup for "
                  ++ show (n, t) ++ " was " ++ show (r1, r2)
  (True, "Comb") -> do
   (t1, t2) <- readTuple readInt readInt
   case (Map.lookup t1 m, Map.lookup t2 m) of
    (Just t1', Just t2') -> do
     expectTag False "Comb"
     return $ Map.insert (Map.size m + 1) (Comb t1' t2') m
    (r1, r2) -> debugS $ "readSharedHolTerm: Couldn't build Comb"
                  ++ " because the result of the lookup for "
                  ++ show (t1, t2) ++ " was " ++ show (r1, r2)
  (True, "Abs") -> do
   (t1, t2) <- readTuple readInt readInt
   case (Map.lookup t1 m, Map.lookup t2 m) of
    (Just t1', Just t2') -> do
     expectTag False "Abs"
     return $ Map.insert (Map.size m + 1) (Abs t1' t2') m
    (r1, r2) -> debugS $ "readSharedHoLTerm: Couldn't build Abs"
                  ++ " because the result of the lookup for "
                  ++ show (t1, t2) ++ " was " ++ show (r1, r2)
  _ -> do
   putM d
   debugS $ "readSharedHolTerm: Expected a hol term but"
            ++ " instead got following tag: " ++ show (b, tg)

importData :: HetcatsOpts -> FilePath
  -> IO ([(String, [(String, Term)])], [(String, String)])
importData opts fp' = do
  fp <- canonicalizePath fp'
  let image = "hol_light.dmtcp"
      dmtcpBin = "dmtcp_restart"
  tmpImage <- getTempFile "" image
  imageFile <- fmap (</> image) $ getEnvDef
   "HETS_HOLLIGHT_TOOLS" "HolLight/OcamlTools/"
  -- for dmtcp we need an image owned by the current user
  copyFile imageFile tmpImage
  e2 <- doesFileExist imageFile
  unless e2 $ fail $ image ++ " not found"
  tempFile <- getTempFile "" (takeBaseName fp)
  (ex, sout, err) <- executeProcess dmtcpBin [tmpImage]
    $ "use_file " ++ show fp ++ ";;\n"
    ++ "inject_hol_include " ++ show fp ++ ";;\n"
    ++ "export_libs (get_libs()) " ++ show tempFile ++ ";;\n"
    ++ "exit 0;;\n"
  removeFile tmpImage
  s <- L.readFile tempFile
  case ex of
   ExitFailure _ -> do
     removeFile tempFile
     fail $ "HolLight.importData: " ++ err
   ExitSuccess -> do
    putIfVerbose opts 5 sout
    let e = ([], [])
    (r, evl, msgs) <- return $ case runMSaxState (do
     expectTag True "HolExport"
     sl <- readL readStr "Strings"
     let strings = Map.fromList (zip [1 ..] sl)
     hol_types <- foldS (readSharedHolType strings)
                   Map.empty "SharedHolTypes"
     hol_terms <- foldS (readSharedHolTerm hol_types strings)
                   Map.empty "SharedHolTerms"
     libs <- readL (readTuple readWord
                    (whileM (readTuple readWord
                             (readMappedInt hol_terms)))) "Libs"
     liblinks <- readL (readTuple readWord readWord) "LibLinks"
     return (libs, liblinks)) (parsexml s) (verbose opts >= 6) of
      (de, msgs) -> (fromMaybe e de, "Next 5 items: "
       ++ show (take 5 $ fst msgs), fst $ snd msgs)
    case msgs of
      Just ms -> putIfVerbose opts 6 $ unlines (reverse ms) ++ evl
      Nothing -> return ()
    removeFile tempFile
    return r

getTypes :: Map.Map String Int -> HolType -> Map.Map String Int
getTypes m t = case t of
 TyVar _ -> m
 TyApp s ts -> let m' = foldl getTypes m ts in
                     Map.insert s (length ts) m'

mergeTypesOps :: (Map.Map String Int, Map.Map String HolType)
                 -> (Map.Map String Int, Map.Map String HolType)
                 -> (Map.Map String Int, Map.Map String HolType)
mergeTypesOps (ts1, ops1) (ts2, ops2) =
 (ts1 `Map.union` ts2, ops1 `Map.union` ops2)

getOps :: Term
           -> (Map.Map String Int, Map.Map String HolType)
getOps tm = case tm of
 Var _ t _ -> let ts = getTypes Map.empty t
                     in (ts, Map.empty)
 Const s t _ -> let ts = getTypes Map.empty t
                     in (ts, Map.insert s t Map.empty)
 Comb t1 t2 -> mergeTypesOps
                  (getOps t1)
                  (getOps t2)
 Abs t1 t2 -> mergeTypesOps
                  (getOps t1)
                  (getOps t2)

calcSig :: [(String, Term)] -> Sign
calcSig tm = let (ts, os) = foldl
                      (\ p (_, t) -> (mergeTypesOps (getOps t) p))
                      (Map.empty, Map.empty) tm
                 in Sign {
                   types = ts
                  , ops = os }

sigDepends :: Sign -> Sign -> Bool
sigDepends s1 s2 = (Map.size (Map.intersection (types s1) (types s2)) /= 0) ||
                   (Map.size (Map.intersection (ops s1) (ops s2)) /= 0)

prettifyTypeVarsTp :: HolType -> Map.Map String String
                      -> (HolType, Map.Map String String)
prettifyTypeVarsTp (TyVar s) m = case Map.lookup s m of
 Just s' -> (TyVar s', m)
 Nothing -> let s' = '\'' : (names !! Map.size m)
            in (TyVar s', Map.insert s s' m)
prettifyTypeVarsTp (TyApp s ts) m =
 let (ts', m') = foldl (\ (ts'', m'') t ->
      let (t', m''') = prettifyTypeVarsTp t m''
      in (t' : ts'', m''')) ([], m) ts
 in (TyApp s ts', m')

prettifyTypeVarsTm :: Term -> Map.Map String String
                      -> (Term, Map.Map String String)
prettifyTypeVarsTm (Const s t p) _ =
 let (t1, m1) = prettifyTypeVarsTp t Map.empty
 in (Const s t1 p, m1)
prettifyTypeVarsTm (Comb tm1 tm2) m =
 let (tm1', m1) = prettifyTypeVarsTm tm1 m
     (tm2', m2) = prettifyTypeVarsTm tm2 m1
 in (Comb tm1' tm2', m2)
prettifyTypeVarsTm (Abs tm1 tm2) m =
 let (tm1', m1) = prettifyTypeVarsTm tm1 m
     (tm2', m2) = prettifyTypeVarsTm tm2 m1
 in (Abs tm1' tm2', m2)
prettifyTypeVarsTm t m = (t, m)

prettifyTypeVars :: ([(String, [(String, Term)])], [(String, String)]) ->
                    ([(String, [(String, Term)])], [(String, String)])
prettifyTypeVars (libs, lnks) =
 let libs' = map (\ (s, terms) ->
      let terms' = foldl (\ tms (ts, t) ->
            let (t', _) = prettifyTypeVarsTm t Map.empty
            in ((ts, t') : tms))
             [] terms
      in (s, terms')
      ) libs
 in (libs', lnks)

treeLevels :: [(String, String)] -> Map.Map Int [(String, String)]
treeLevels l =
 let lk = foldr (\ (imp, t) l' ->
      case lookup t l' of
       Just (p, _) -> (imp, (p + 1, t)) : l'
       Nothing -> (imp, (1, t)) : (t, (0, "")) : l') [] l
 in foldl (\ m (imp, (p, t)) ->
  let s = Map.findWithDefault [] p m
  in Map.insert p ((imp, t) : s) m) Map.empty lk

makeNamedSentence :: String -> Term -> Named Sentence
makeNamedSentence n t = makeNamed n Sentence { term = t, proof = Nothing }

_insNodeDG :: Sign -> [Named Sentence] -> String
              -> (DGraph, Map.Map String
               (String, Data.Graph.Inductive.Graph.Node, DGNodeLab))
              -> (DGraph, Map.Map String
               (String, Data.Graph.Inductive.Graph.Node, DGNodeLab))
_insNodeDG sig sens n (dg, m) =
 let gt = G_theory HolLight Nothing (makeExtSign HolLight sig) startSigId
           (toThSens sens) startThId
     n' = snd (System.FilePath.splitFileName n)
     labelK = newInfoNodeLab
      (makeName (simpleIdToIRI $ mkSimpleId n'))
      (newNodeInfo DGEmpty)
      gt
     k = getNewNodeDG dg
     m' = Map.insert n (n, k, labelK) m
     insN = [InsertNode (k, labelK)]
     newDG = changesDGH dg insN
     labCh = [SetNodeLab labelK (k, labelK
      { globalTheory = computeLabelTheory Map.empty newDG
        (k, labelK) })]
     newDG1 = changesDGH newDG labCh in (newDG1, m')

anaHolLightFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaHolLightFile opts path = do
 (libs_, lnks_) <- importData opts path
 let (libs, lnks) = prettifyTypeVars (libs_, lnks_)
 let h = treeLevels lnks
 let fixLinks m l =
      case l of
       (l1 : l2 : l') ->
        if snd l1 == snd l2 && sigDepends
         (Map.findWithDefault emptySig (fst l1) m)
         (Map.findWithDefault emptySig (fst l2) m) then
          (fst l1, fst l2) : fixLinks m (l2 : l')
        else l1 : l2 : fixLinks m l'
       l' -> l'
 let uniteSigs = foldl (\ m' (s, t) ->
                  case resultToMaybe
                    (sigUnion (Map.findWithDefault emptySig s m')
                    (Map.findWithDefault emptySig t m')) of
                   Nothing -> m'
                   Just new_tsig -> Map.insert t new_tsig m')
 let m = foldl (\ m' (s, l) -> Map.insert s (calcSig l) m') Map.empty libs
 let (m', lnks') = foldr (\ lvl (m'', lnks_loc) ->
                    let lvl' = Map.findWithDefault [] lvl h
                        lnks_next = fixLinks m'' (reverse lvl')
{- we'd probably need to take care of dependencies on previously
imported files not imported by the file imported last -}
                    in (uniteSigs m'' lnks_next, lnks_next ++ lnks_loc)
                   ) (m, []) [0 .. (Map.size h - 1)]
 let (dg', node_m) = foldr (\ (lname, lterms) (dg, node_m') ->
           let sig = Map.findWithDefault emptySig lname m'
               sens = map (uncurry makeNamedSentence) lterms in
           _insNodeDG sig sens lname (dg, node_m')) (emptyDG, Map.empty) libs
     dg'' = foldr (\ (source, target) dg ->
      case Map.lookup source node_m of
       Just (n, k, _) ->
        case Map.lookup target node_m of
         Just (n1, k1, _) ->
          let sig = Map.findWithDefault emptySig n m'
              sig1 = Map.findWithDefault emptySig n1 m'
          in case resultToMaybe $
               subsig_inclusion HolLight sig sig1 of
              Nothing -> dg
              Just incl ->
               let inclM = gEmbed $ mkG_morphism HolLight incl
                   insE = [InsertEdge (k, k1, globDefLink inclM DGLinkImports)]
               in changesDGH dg insE
         Nothing -> dg
       Nothing -> dg) dg' lnks'
     le = Map.insert (emptyLibName
            (System.FilePath.takeBaseName path))
           dg'' Map.empty
 return (Just (emptyLibName
  (System.FilePath.takeBaseName path),
  computeLibEnvTheories le))
