content: {- |
  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)
  