{- |

Module : ./CommonLogic/ParseCLAsLibDefn.hs

Copyright : Eugen Kuksa 2011

License : GPLv2 or higher, see LICENSE.txt

Maintainer : eugenk@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable (imports Logic.Logic)

Analyses CommonLogic files.

-}

module CommonLogic.ParseCLAsLibDefn (parseCL_CLIF) where

import Common.Id

import Common.IRI

import Common.LibName

import Common.AS_Annotation as Anno

import Common.AnnoState

import Common.Parsec

import Common.Result

import Common.ResultT

import Driver.Options

import Driver.ReadFn

import Text.ParserCombinators.Parsec

import Logic.Grothendieck

import CommonLogic.AS_CommonLogic as CL

import CommonLogic.Logic_CommonLogic

import qualified CommonLogic.Parse_CLIF as CLIF (basicSpec)

import Syntax.AS_Library

import Syntax.AS_Structured

import Control.Monad (foldM)

import Control.Monad.Trans

import qualified Data.Set as Set

import qualified Data.Map as Map

import Data.List

import System.FilePath

type SpecMap = Map.Map FilePath SpecInfo

type SpecInfo = (BASIC_SPEC, FilePath, Set.Set String, Set.Set FilePath)

-- (spec, topTexts, importedBy)

-- | call for CommonLogic CLIF-parser with recursive inclusion of importations

parseCL_CLIF :: FilePath -> HetcatsOpts -> ResultT IO [LIB_DEFN]

parseCL_CLIF filename opts = do

let dirFile@(dir, _) = splitFileName filename

specMap <- downloadSpec opts Map.empty Set.empty Set.empty False dirFile dir

return $ map convertToLibDefN $ topSortSpecs

$ Map.map (\ (b, f, _, _) ->

(b, f, Set.map (rmSuffix . tokStr) $ directImports b)) specMap

-- call for CommonLogic CLIF-parser for a single file

parseCL_CLIF_contents :: FilePath -> String -> Either ParseError [BASIC_SPEC]

parseCL_CLIF_contents = runParser (many (CLIF.basicSpec Map.empty) << eof)

(emptyAnnos ())

{- maps imports in basic spec to global definition links (extensions) in

development graph -}

convertToLibDefN :: (FilePath, BASIC_SPEC, FilePath) -> LIB_DEFN

convertToLibDefN (fp, spec, realFp) = let

i = filePathToLibId $ rmSuffix fp

in Lib_defn (setFilePath realFp $ iriLibName i)

(makeLogicItem CommonLogic

: map (addDownload False) (importsAsIris spec)

++ [convertToLibItem spec i])

nullRange []

convertToLibItem :: BASIC_SPEC -> IRI -> Anno.Annoted LIB_ITEM

convertToLibItem b i = makeSpecItem i $ createSpec b

importsAsIris :: BASIC_SPEC -> [IRI]

importsAsIris =

map (filePathToLibId . rmSuffix . tokStr) . Set.toList . directImports

createSpec :: BASIC_SPEC -> Anno.Annoted SPEC

createSpec b = addImports (importsAsIris b)

. makeSpec $ G_basic_spec CommonLogic b

specNameL :: [BASIC_SPEC] -> String -> [String]

specNameL bs def = case bs of

[_] -> [def]

_ -> map (specName def) [0 .. (length bs)]

-- returns a unique name for a node

specName :: String -> Int -> String

specName def i = def ++ "_" ++ show i

fileCombine :: FilePath -> FilePath -> FilePath

fileCombine d = (\ s -> case s of

'.' : p : r | isPathSeparator p -> r

_ -> s) . combine d

httpCombine :: FilePath -> FilePath -> FilePath

httpCombine d f = if checkUri f then f else fileCombine d f

collectDownloads :: HetcatsOpts -> String -> SpecMap -> (String, SpecInfo)

-> ResultT IO SpecMap

collectDownloads opts baseDir specMap (n, (b, _, topTexts, importedBy)) = do

let directImps = Set.elems $ Set.map tokStr $ directImports b

newTopTexts = Set.insert n topTexts

newImportedBy = Set.insert n importedBy

foldM (\ sm d -> do

let p@(ddir, _) = splitFileName d

baseDir' = httpCombine baseDir ddir

newDls <- downloadSpec opts sm newTopTexts newImportedBy True

p baseDir'

return (Map.unionWith unify newDls sm)

) specMap directImps -- imports get @n@ as new "importedBy"

justErr :: a -> String -> ResultT IO a

justErr a s = liftR $ plain_error a s nullRange

downloadSpec :: HetcatsOpts -> SpecMap -> Set.Set String -> Set.Set String

-> Bool -> (String, String) -> String -> ResultT IO SpecMap

downloadSpec opts specMap topTexts importedBy isImport dirFile baseDir = do

let fn = rmSuffix $ uncurry httpCombine dirFile

case Map.lookup fn specMap of

Just info@(b, f, t, _)

| isImport && Set.member fn importedBy ->

justErr specMap . intercalate "\n "

$ "unsupported cyclic imports:" : Set.toList importedBy

| t == topTexts

-> return specMap

| otherwise ->

let newInfo = unify info (b, f, topTexts, importedBy)

newSpecMap = Map.insert fn newInfo specMap

in collectDownloads opts baseDir newSpecMap (fn, newInfo)

Nothing -> do

mCont <- lift $ getCLIFContents opts dirFile baseDir

case mCont of

Left err -> justErr specMap $ show err

Right (file, contents) -> do

lift $ putIfVerbose opts 2 $ "Downloaded " ++ file

case parseCL_CLIF_contents fn contents of

Left err -> justErr specMap $ show err

Right bs -> do

let nbs = zip (specNameL bs fn) bs

nbs2 <- mapM (\ (n, b) -> case

map (rmSuffix . tokStr) $ clTexts b of

[txt] -> if txt == fn then return (n, b) else

liftR $ justWarn (if isImport then n else txt, b)

$ "filename " ++ show fn

++ " does not match cl-text " ++ show txt

[] -> liftR $ justWarn (n, b)

$ "missing cl-text in " ++ show fn

ts -> liftR $ justWarn (n, b)

$ "multiple cl-text entries in "

++ show fn ++ "\n" ++ unlines (map show ts)

) nbs

let nbtis = map (\ (n, b) ->

(n, (b, file, topTexts, importedBy))) nbs2

newSpecMap = foldr (\ (n, bti) sm ->

Map.insertWith unify n bti sm

) specMap nbtis

foldM (\ sm nbt -> do

newDls <- collectDownloads opts baseDir sm nbt

return (Map.unionWith unify newDls sm)

) newSpecMap nbtis

unify :: SpecInfo -> SpecInfo -> SpecInfo

unify (_, _, s, p) (a, b, t, q) = (a, b, s `Set.union` t, p `Set.union` q)

{- one could add support for uri fragments/query

(perhaps select a text from the file) -}

getCLIFContents :: HetcatsOpts -> (String, String) -> String

-> IO (Either String (FilePath, String))

getCLIFContents opts dirFile baseDir =

let fn = uncurry httpCombine dirFile

uStr = useCatalogURL opts

$ if checkUri baseDir then httpCombine baseDir fn else fn

in getExtContent opts { libdirs = baseDir : libdirs opts }

[".clif", ".clf"] uStr

-- retrieves all importations from the text

directImports :: BASIC_SPEC -> Set.Set NAME

directImports (CL.Basic_spec items) = Set.unions

$ map (getImports_textMetas . textsFromBasicItems . Anno.item) items

clTexts :: BASIC_SPEC -> [NAME]

clTexts (CL.Basic_spec items) =

concatMap (getClTexts . textsFromBasicItems . Anno.item) items

textsFromBasicItems :: BASIC_ITEMS -> [TEXT_META]

textsFromBasicItems (Axiom_items axs) = map Anno.item axs

getImports_textMetas :: [TEXT_META] -> Set.Set NAME

getImports_textMetas = Set.unions . map (getImports_text . getText)

getClTexts :: [TEXT_META] -> [NAME]

getClTexts = concatMap (getClTextTexts . getText)

getClTextTexts :: TEXT -> [NAME]

getClTextTexts txt = case txt of

Named_text n t _ -> n : getClTextTexts t

_ -> []

getImports_text :: TEXT -> Set.Set NAME

getImports_text txt = case txt of

Text p _ -> Set.fromList $ map impName $ filter isImportation p

Named_text _ t _ -> getImports_text t

isImportation :: PHRASE -> Bool

isImportation ph = case ph of

Importation _ -> True

_ -> False

impName :: PHRASE -> NAME

impName ph = case ph of

Importation (Imp_name n) -> n

_ -> error "CL.impName"

topSortSpecs :: Map.Map FilePath (BASIC_SPEC, FilePath, Set.Set FilePath)

-> [(FilePath, BASIC_SPEC, FilePath)]

topSortSpecs specMap =

let (fm, rm) = Map.partition (\ (_, _, is) -> Set.null is) specMap

in if Map.null fm then [] else

map (\ (n, (b, f, _)) -> (n, b, f)) (Map.toList fm) ++ topSortSpecs

(Map.map (\ (b, f, is) -> (b, f, is Set.\\ Map.keysSet fm)) rm)