{- |

Module : $Header$

Description : reading and parsing ATerms, CASL, HetCASL files

Copyright : (c) Klaus L�ttich, C. Maeder, Uni Bremen 2002-2006

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

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : non-portable(DevGraph)

reading and parsing ATerms, CASL, HetCASL files

-}

module Driver.ReadFn where

import Logic.Grothendieck

import Syntax.AS_Library

import Syntax.Parse_AS_Library

import Syntax.Print_AS_Library()

import Static.DevGraph

import Proofs.EdgeUtils

import ATC.AS_Library()

import ATC.DevGraph()

import ATC.GlobalAnnotations()

import ATC.Sml_cats

import Common.ATerm.Lib

import Common.ATerm.ReadWrite

import qualified Data.Map as Map

import Common.AnnoState

import Common.Id

import Common.Result

import Common.DocUtils

import Text.ParserCombinators.Parsec

import Driver.Options

import System.Time

import Control.Monad

import Data.List

read_LIB_DEFN_M :: Monad m => LogicGraph -> HetcatsOpts

-> FilePath -> String -> ClockTime -> m LIB_DEFN

read_LIB_DEFN_M lgraph opts file input mt =

if null input then fail ("empty input file: " ++ file) else

case intype opts of

ATermIn _ -> return $ from_sml_ATermString input

ASTreeIn _ -> fail "Abstract Syntax Trees aren't implemented yet"

_ -> case runParser (library lgraph { currentLogic = defLogic opts })

(emptyAnnos ()) file input of

Left err -> fail (showErr err)

Right ast -> return $ setFilePath file mt ast

readShATermFile :: ShATermConvertible a => FilePath -> IO (Result a)

readShATermFile fp = do

str <- readFile fp

return $ fromShATermString str

fromVersionedATT :: ShATermConvertible a => ATermTable -> Result a

fromVersionedATT att =

case getATerm att of

ShAAppl "hets" [versionnr,aterm] [] ->

if hetsVersion == snd (fromShATermAux versionnr att)

then Result [] (Just $ snd $ fromShATermAux aterm att)

else Result [Diag Warning

"Wrong version number ... re-analyzing"

nullRange] Nothing

_ -> Result [Diag Warning

"Couldn't convert ShATerm back from ATermTable"

nullRange] Nothing

fromShATermString :: ShATermConvertible a => String -> Result a

fromShATermString str = if null str then

Result [Diag Warning "got empty string from file" nullRange] Nothing

else fromVersionedATT $ readATerm str

readVerbose :: ShATermConvertible a => HetcatsOpts -> LIB_NAME -> FilePath

-> IO (Maybe a)

readVerbose opts ln file = do

putIfVerbose opts 1 $ "Reading " ++ file

Result ds mgc <- readShATermFile file

showDiags opts ds

case mgc of

Nothing -> return Nothing

Just (ln2, a) -> if ln2 == ln then return $ Just a else do

putIfVerbose opts 0 $ "incompatible library names: "

++ showDoc ln " (requested) vs. "

++ showDoc ln2 " (found)"

return Nothing

-- | create a file name without suffix from a library name

libNameToFile :: HetcatsOpts -> LIB_NAME -> FilePath

libNameToFile opts ln =

case getLIB_ID ln of

Indirect_link file _ ofile _ ->

let path = libdir opts

-- add trailing "/" if necessary

in if null ofile then pathAndBase path file else ofile

Direct_link _ _ -> error "libNameToFile"

-- | convert a file name that may have a suffix to a library name

fileToLibName :: HetcatsOpts -> FilePath -> LIB_NAME

fileToLibName opts efile =

let path = libdir opts

file = rmSuffix efile -- cut of extension

nfile = dropWhile (== '/') $ -- cut off leading slashes

if isPrefixOf path file

then drop (length path) file -- cut off libdir prefix

else file

in Lib_id $ Indirect_link nfile nullRange "" noTime

readPrfFile :: HetcatsOpts -> LibEnv -> LIB_NAME -> IO LibEnv

readPrfFile opts ps ln = do

let fname = libNameToFile opts ln

prfFile = rmSuffix fname ++ prfSuffix

recent <- checkRecentEnv opts prfFile fname

h <- if recent then

fmap (maybe [emptyHistory] id) $ readVerbose opts ln prfFile

else return [emptyHistory]

return $ Map.update (Just . applyProofHistory h) ln ps

readPrfFiles :: HetcatsOpts -> LibEnv -> IO LibEnv

readPrfFiles opts le = do

foldM (readPrfFile opts) le $ Map.keys le