a27e9e05958bc51ea09edb8d8d862fe8b125313bslive{- |

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveModule : $Header$

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveDescription : reading and parsing ATerms, CASL, HetCASL files

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveCopyright : (c) Klaus Luettich, C. Maeder, Uni Bremen 2002-2006

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

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveMaintainer : Christian.Maeder@dfki.de

51853aa2ebfdf9903a094467e1d02099f143639daaronStability : provisional

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivePortability : non-portable(DevGraph)

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivereading and parsing ATerms, CASL, HetCASL files as much as is needed for the

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivestatic analysis

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-}

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivemodule Driver.ReadFn where

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Logic.Grothendieck

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Syntax.AS_Library

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Syntax.Parse_AS_Library

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport ATC.Grothendieck

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport ATC.Sml_cats

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport ATC.LibName ()

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Driver.Options

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport ATerm.AbstractSyntax

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport ATerm.ReadWrite

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.AnnoState

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.Id

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.Result

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.DocUtils

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.LibName

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Text.ParserCombinators.Parsec

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport System.FilePath

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Data.List (isPrefixOf)

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Data.Maybe

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivereadLibDefnM :: Monad m => LogicGraph -> HetcatsOpts -> FilePath -> String

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive -> m LIB_DEFN

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivereadLibDefnM lgraph opts file input =

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

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive case intype opts of

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive ATermIn _ -> return $ from_sml_ATermString input

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

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive (emptyAnnos ()) file input of

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Left err -> fail (showErr err)

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Right ast -> return ast

51853aa2ebfdf9903a094467e1d02099f143639daaron

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivereadShATermFile :: ShATermLG a => LogicGraph -> FilePath -> IO (Result a)

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivereadShATermFile lg fp = do

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive str <- readFile fp

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive return $ fromShATermString lg str

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivefromVersionedATT :: ShATermLG a => LogicGraph -> ATermTable -> Result a

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivefromVersionedATT lg att =

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive case getATerm att of

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

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive if hetsVersion == snd (fromShATermLG lg versionnr att)

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive then Result [] (Just $ snd $ fromShATermLG lg aterm att)

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive else Result [Diag Warning

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive "Wrong version number ... re-analyzing"

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive nullRange] Nothing

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive _ -> Result [Diag Warning

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive "Couldn't convert ShATerm back from ATermTable"

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive nullRange] Nothing

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivefromShATermString :: ShATermLG a => LogicGraph -> String -> Result a

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivefromShATermString lg str = if null str then

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

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive else fromVersionedATT lg $ readATerm str

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivereadVerbose :: ShATermLG a => LogicGraph -> HetcatsOpts -> LibName -> FilePath

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive -> IO (Maybe a)

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivereadVerbose lg opts ln file = do

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive putIfVerbose opts 1 $ "Reading " ++ file

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive Result ds mgc <- readShATermFile lg file

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive showDiags opts ds

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele case mgc of

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele Nothing -> return Nothing

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

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele putIfVerbose opts 0 $ "incompatible library names: "

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele ++ showDoc ln " (requested) vs. "

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele ++ showDoc ln2 " (found)"

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele return Nothing

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele

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

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelelibNameToFile :: LibName -> FilePath

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelelibNameToFile ln = case getLibId ln of

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele IndirectLink file _ ofile _ ->

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele if null ofile then file

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele else rmSuffix ofile

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele DirectLink _ _ -> error "libNameToFile"

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelefindFileOfLibName :: HetcatsOpts -> FilePath -> IO (Maybe FilePath)

findFileOfLibName opts file = do

let fs = map (</> file) $ "" : libdirs opts

ms <- mapM (existsAnSource opts { intype = GuessIn }) fs

return $ case catMaybes ms of

[] -> Nothing

f : _ -> Just f

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

fileToLibName :: HetcatsOpts -> FilePath -> LibName

fileToLibName opts efile =

let paths = libdirs opts

file = rmSuffix efile -- cut of extension

pps = filter snd $ map (\ p -> (p, isPrefixOf p file)) paths

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

case pps of

[] -> file

(path, _) : _ -> drop (length path) file

-- cut off libdir prefix

in emptyLibName nfile