{- |
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 :: FilePath -> HetcatsOpts -> ResultT IO [LIB_DEFN]
parseCL_CLIF filename :: FilePath
filename opts :: HetcatsOpts
opts = do
  let dirFile :: (FilePath, FilePath)
dirFile@(dir :: FilePath
dir, _) = FilePath -> (FilePath, FilePath)
splitFileName FilePath
filename
  SpecMap
specMap <- HetcatsOpts
-> SpecMap
-> Set FilePath
-> Set FilePath
-> Bool
-> (FilePath, FilePath)
-> FilePath
-> ResultT IO SpecMap
downloadSpec HetcatsOpts
opts SpecMap
forall k a. Map k a
Map.empty Set FilePath
forall a. Set a
Set.empty Set FilePath
forall a. Set a
Set.empty Bool
False (FilePath, FilePath)
dirFile FilePath
dir
  [LIB_DEFN] -> ResultT IO [LIB_DEFN]
forall (m :: * -> *) a. Monad m => a -> m a
return ([LIB_DEFN] -> ResultT IO [LIB_DEFN])
-> [LIB_DEFN] -> ResultT IO [LIB_DEFN]
forall a b. (a -> b) -> a -> b
$ ((FilePath, BASIC_SPEC, FilePath) -> LIB_DEFN)
-> [(FilePath, BASIC_SPEC, FilePath)] -> [LIB_DEFN]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath, BASIC_SPEC, FilePath) -> LIB_DEFN
convertToLibDefN ([(FilePath, BASIC_SPEC, FilePath)] -> [LIB_DEFN])
-> [(FilePath, BASIC_SPEC, FilePath)] -> [LIB_DEFN]
forall a b. (a -> b) -> a -> b
$ Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
-> [(FilePath, BASIC_SPEC, FilePath)]
topSortSpecs
    (Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
 -> [(FilePath, BASIC_SPEC, FilePath)])
-> Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
-> [(FilePath, BASIC_SPEC, FilePath)]
forall a b. (a -> b) -> a -> b
$ ((BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
 -> (BASIC_SPEC, FilePath, Set FilePath))
-> SpecMap -> Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ (b :: BASIC_SPEC
b, f :: FilePath
f, _, _) ->
               (BASIC_SPEC
b, FilePath
f, (Token -> FilePath) -> Set Token -> Set FilePath
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (FilePath -> FilePath
rmSuffix (FilePath -> FilePath) -> (Token -> FilePath) -> Token -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> FilePath
tokStr) (Set Token -> Set FilePath) -> Set Token -> Set FilePath
forall a b. (a -> b) -> a -> b
$ BASIC_SPEC -> Set Token
directImports BASIC_SPEC
b)) SpecMap
specMap

-- call for CommonLogic CLIF-parser for a single file
parseCL_CLIF_contents :: FilePath -> String -> Either ParseError [BASIC_SPEC]
parseCL_CLIF_contents :: FilePath -> FilePath -> Either ParseError [BASIC_SPEC]
parseCL_CLIF_contents = GenParser Char (AnnoState ()) [BASIC_SPEC]
-> AnnoState ()
-> FilePath
-> FilePath
-> Either ParseError [BASIC_SPEC]
forall tok st a.
GenParser tok st a
-> st -> FilePath -> [tok] -> Either ParseError a
runParser (ParsecT FilePath (AnnoState ()) Identity BASIC_SPEC
-> GenParser Char (AnnoState ()) [BASIC_SPEC]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (PrefixMap -> ParsecT FilePath (AnnoState ()) Identity BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
CLIF.basicSpec PrefixMap
forall k a. Map k a
Map.empty) GenParser Char (AnnoState ()) [BASIC_SPEC]
-> ParsecT FilePath (AnnoState ()) Identity ()
-> GenParser Char (AnnoState ()) [BASIC_SPEC]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT FilePath (AnnoState ()) Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)
                        (() -> AnnoState ()
forall st. st -> AnnoState st
emptyAnnos ())

{- maps imports in basic spec to global definition links (extensions) in
development graph -}
convertToLibDefN :: (FilePath, BASIC_SPEC, FilePath) -> LIB_DEFN
convertToLibDefN :: (FilePath, BASIC_SPEC, FilePath) -> LIB_DEFN
convertToLibDefN (fp :: FilePath
fp, spec :: BASIC_SPEC
spec, realFp :: FilePath
realFp) = let
  i :: IRI
i = FilePath -> IRI
filePathToLibId (FilePath -> IRI) -> FilePath -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
rmSuffix FilePath
fp
  in LibName -> [Annoted LIB_ITEM] -> Range -> [Annotation] -> LIB_DEFN
Lib_defn (FilePath -> LibName -> LibName
setFilePath FilePath
realFp (LibName -> LibName) -> LibName -> LibName
forall a b. (a -> b) -> a -> b
$ IRI -> LibName
iriLibName IRI
i)
    (CommonLogic -> Annoted LIB_ITEM
forall lid. Language lid => lid -> Annoted LIB_ITEM
makeLogicItem CommonLogic
CommonLogic
    Annoted LIB_ITEM -> [Annoted LIB_ITEM] -> [Annoted LIB_ITEM]
forall a. a -> [a] -> [a]
: (IRI -> Annoted LIB_ITEM) -> [IRI] -> [Annoted LIB_ITEM]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> IRI -> Annoted LIB_ITEM
addDownload Bool
False) (BASIC_SPEC -> [IRI]
importsAsIris BASIC_SPEC
spec)
    [Annoted LIB_ITEM] -> [Annoted LIB_ITEM] -> [Annoted LIB_ITEM]
forall a. [a] -> [a] -> [a]
++ [BASIC_SPEC -> IRI -> Annoted LIB_ITEM
convertToLibItem BASIC_SPEC
spec IRI
i])
    Range
nullRange []

convertToLibItem :: BASIC_SPEC -> IRI -> Anno.Annoted LIB_ITEM
convertToLibItem :: BASIC_SPEC -> IRI -> Annoted LIB_ITEM
convertToLibItem b :: BASIC_SPEC
b i :: IRI
i = IRI -> Annoted SPEC -> Annoted LIB_ITEM
makeSpecItem IRI
i (Annoted SPEC -> Annoted LIB_ITEM)
-> Annoted SPEC -> Annoted LIB_ITEM
forall a b. (a -> b) -> a -> b
$ BASIC_SPEC -> Annoted SPEC
createSpec BASIC_SPEC
b

importsAsIris :: BASIC_SPEC -> [IRI]
importsAsIris :: BASIC_SPEC -> [IRI]
importsAsIris =
  (Token -> IRI) -> [Token] -> [IRI]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> IRI
filePathToLibId (FilePath -> IRI) -> (Token -> FilePath) -> Token -> IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> FilePath
rmSuffix (FilePath -> FilePath) -> (Token -> FilePath) -> Token -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> FilePath
tokStr) ([Token] -> [IRI])
-> (BASIC_SPEC -> [Token]) -> BASIC_SPEC -> [IRI]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Token -> [Token]
forall a. Set a -> [a]
Set.toList (Set Token -> [Token])
-> (BASIC_SPEC -> Set Token) -> BASIC_SPEC -> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BASIC_SPEC -> Set Token
directImports

createSpec :: BASIC_SPEC -> Anno.Annoted SPEC
createSpec :: BASIC_SPEC -> Annoted SPEC
createSpec b :: BASIC_SPEC
b = [IRI] -> Annoted SPEC -> Annoted SPEC
addImports (BASIC_SPEC -> [IRI]
importsAsIris BASIC_SPEC
b)
  (Annoted SPEC -> Annoted SPEC)
-> (G_basic_spec -> Annoted SPEC) -> G_basic_spec -> Annoted SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_basic_spec -> Annoted SPEC
makeSpec (G_basic_spec -> Annoted SPEC) -> G_basic_spec -> Annoted SPEC
forall a b. (a -> b) -> a -> b
$ CommonLogic -> BASIC_SPEC -> G_basic_spec
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> basic_spec -> G_basic_spec
G_basic_spec CommonLogic
CommonLogic BASIC_SPEC
b

specNameL :: [BASIC_SPEC] -> String -> [String]
specNameL :: [BASIC_SPEC] -> FilePath -> [FilePath]
specNameL bs :: [BASIC_SPEC]
bs def :: FilePath
def = case [BASIC_SPEC]
bs of
  [_] -> [FilePath
def]
  _ -> (Int -> FilePath) -> [Int] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> Int -> FilePath
specName FilePath
def) [0 .. ([BASIC_SPEC] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BASIC_SPEC]
bs)]

-- returns a unique name for a node
specName :: String -> Int -> String
specName :: FilePath -> Int -> FilePath
specName def :: FilePath
def i :: Int
i = FilePath
def FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "_" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i

fileCombine :: FilePath -> FilePath -> FilePath
fileCombine :: FilePath -> FilePath -> FilePath
fileCombine d :: FilePath
d = (\ s :: FilePath
s -> case FilePath
s of
   '.' : p :: Char
p : r :: FilePath
r | Char -> Bool
isPathSeparator Char
p -> FilePath
r
   _ -> FilePath
s) (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> FilePath -> FilePath
combine FilePath
d

httpCombine :: FilePath -> FilePath -> FilePath
httpCombine :: FilePath -> FilePath -> FilePath
httpCombine d :: FilePath
d f :: FilePath
f = if FilePath -> Bool
checkUri FilePath
f then FilePath
f else FilePath -> FilePath -> FilePath
fileCombine FilePath
d FilePath
f

collectDownloads :: HetcatsOpts -> String -> SpecMap -> (String, SpecInfo)
 -> ResultT IO SpecMap
collectDownloads :: HetcatsOpts
-> FilePath
-> SpecMap
-> (FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))
-> ResultT IO SpecMap
collectDownloads opts :: HetcatsOpts
opts baseDir :: FilePath
baseDir specMap :: SpecMap
specMap (n :: FilePath
n, (b :: BASIC_SPEC
b, _, topTexts :: Set FilePath
topTexts, importedBy :: Set FilePath
importedBy)) = do
  let directImps :: [FilePath]
directImps = Set FilePath -> [FilePath]
forall a. Set a -> [a]
Set.elems (Set FilePath -> [FilePath]) -> Set FilePath -> [FilePath]
forall a b. (a -> b) -> a -> b
$ (Token -> FilePath) -> Set Token -> Set FilePath
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Token -> FilePath
tokStr (Set Token -> Set FilePath) -> Set Token -> Set FilePath
forall a b. (a -> b) -> a -> b
$ BASIC_SPEC -> Set Token
directImports BASIC_SPEC
b
      newTopTexts :: Set FilePath
newTopTexts = FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => a -> Set a -> Set a
Set.insert FilePath
n Set FilePath
topTexts
      newImportedBy :: Set FilePath
newImportedBy = FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => a -> Set a -> Set a
Set.insert FilePath
n Set FilePath
importedBy
  (SpecMap -> FilePath -> ResultT IO SpecMap)
-> SpecMap -> [FilePath] -> ResultT IO SpecMap
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ sm :: SpecMap
sm d :: FilePath
d -> do
          let p :: (FilePath, FilePath)
p@(ddir :: FilePath
ddir, _) = FilePath -> (FilePath, FilePath)
splitFileName FilePath
d
              baseDir' :: FilePath
baseDir' = FilePath -> FilePath -> FilePath
httpCombine FilePath
baseDir FilePath
ddir
          SpecMap
newDls <- HetcatsOpts
-> SpecMap
-> Set FilePath
-> Set FilePath
-> Bool
-> (FilePath, FilePath)
-> FilePath
-> ResultT IO SpecMap
downloadSpec HetcatsOpts
opts SpecMap
sm Set FilePath
newTopTexts Set FilePath
newImportedBy Bool
True
              (FilePath, FilePath)
p FilePath
baseDir'
          SpecMap -> ResultT IO SpecMap
forall (m :: * -> *) a. Monad m => a -> m a
return (((BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
 -> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
 -> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))
-> SpecMap -> SpecMap -> SpecMap
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
unify SpecMap
newDls SpecMap
sm)
        ) SpecMap
specMap [FilePath]
directImps -- imports get @n@ as new "importedBy"

justErr :: a -> String -> ResultT IO a
justErr :: a -> FilePath -> ResultT IO a
justErr a :: a
a s :: FilePath
s = Result a -> ResultT IO a
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result a -> ResultT IO a) -> Result a -> ResultT IO a
forall a b. (a -> b) -> a -> b
$ a -> FilePath -> Range -> Result a
forall a. a -> FilePath -> Range -> Result a
plain_error a
a FilePath
s Range
nullRange

downloadSpec :: HetcatsOpts -> SpecMap -> Set.Set String -> Set.Set String
  -> Bool -> (String, String) -> String -> ResultT IO SpecMap
downloadSpec :: HetcatsOpts
-> SpecMap
-> Set FilePath
-> Set FilePath
-> Bool
-> (FilePath, FilePath)
-> FilePath
-> ResultT IO SpecMap
downloadSpec opts :: HetcatsOpts
opts specMap :: SpecMap
specMap topTexts :: Set FilePath
topTexts importedBy :: Set FilePath
importedBy isImport :: Bool
isImport dirFile :: (FilePath, FilePath)
dirFile baseDir :: FilePath
baseDir = do
  let fn :: FilePath
fn = FilePath -> FilePath
rmSuffix (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ (FilePath -> FilePath -> FilePath)
-> (FilePath, FilePath) -> FilePath
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry FilePath -> FilePath -> FilePath
httpCombine (FilePath, FilePath)
dirFile
  case FilePath
-> SpecMap
-> Maybe (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FilePath
fn SpecMap
specMap of
      Just info :: (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
info@(b :: BASIC_SPEC
b, f :: FilePath
f, t :: Set FilePath
t, _)
        | Bool
isImport Bool -> Bool -> Bool
&& FilePath -> Set FilePath -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member FilePath
fn Set FilePath
importedBy ->
           SpecMap -> FilePath -> ResultT IO SpecMap
forall a. a -> FilePath -> ResultT IO a
justErr SpecMap
specMap (FilePath -> ResultT IO SpecMap)
-> ([FilePath] -> FilePath) -> [FilePath] -> ResultT IO SpecMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate "\n "
             ([FilePath] -> ResultT IO SpecMap)
-> [FilePath] -> ResultT IO SpecMap
forall a b. (a -> b) -> a -> b
$ "unsupported cyclic imports:" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: Set FilePath -> [FilePath]
forall a. Set a -> [a]
Set.toList Set FilePath
importedBy
        | Set FilePath
t Set FilePath -> Set FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== Set FilePath
topTexts
          -> SpecMap -> ResultT IO SpecMap
forall (m :: * -> *) a. Monad m => a -> m a
return SpecMap
specMap
        | Bool
otherwise ->
          let newInfo :: (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
newInfo = (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
unify (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
info (BASIC_SPEC
b, FilePath
f, Set FilePath
topTexts, Set FilePath
importedBy)
              newSpecMap :: SpecMap
newSpecMap = FilePath
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> SpecMap
-> SpecMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FilePath
fn (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
newInfo SpecMap
specMap
          in HetcatsOpts
-> FilePath
-> SpecMap
-> (FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))
-> ResultT IO SpecMap
collectDownloads HetcatsOpts
opts FilePath
baseDir SpecMap
newSpecMap (FilePath
fn, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
newInfo)
      Nothing -> do
        Either FilePath (FilePath, FilePath)
mCont <- IO (Either FilePath (FilePath, FilePath))
-> ResultT IO (Either FilePath (FilePath, FilePath))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Either FilePath (FilePath, FilePath))
 -> ResultT IO (Either FilePath (FilePath, FilePath)))
-> IO (Either FilePath (FilePath, FilePath))
-> ResultT IO (Either FilePath (FilePath, FilePath))
forall a b. (a -> b) -> a -> b
$ HetcatsOpts
-> (FilePath, FilePath)
-> FilePath
-> IO (Either FilePath (FilePath, FilePath))
getCLIFContents HetcatsOpts
opts (FilePath, FilePath)
dirFile FilePath
baseDir
        case Either FilePath (FilePath, FilePath)
mCont of
          Left err :: FilePath
err -> SpecMap -> FilePath -> ResultT IO SpecMap
forall a. a -> FilePath -> ResultT IO a
justErr SpecMap
specMap (FilePath -> ResultT IO SpecMap) -> FilePath -> ResultT IO SpecMap
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
err
          Right (file :: FilePath
file, contents :: FilePath
contents) -> do
            IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 2 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Downloaded " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
file
            case FilePath -> FilePath -> Either ParseError [BASIC_SPEC]
parseCL_CLIF_contents FilePath
fn FilePath
contents of
              Left err :: ParseError
err -> SpecMap -> FilePath -> ResultT IO SpecMap
forall a. a -> FilePath -> ResultT IO a
justErr SpecMap
specMap (FilePath -> ResultT IO SpecMap) -> FilePath -> ResultT IO SpecMap
forall a b. (a -> b) -> a -> b
$ ParseError -> FilePath
forall a. Show a => a -> FilePath
show ParseError
err
              Right bs :: [BASIC_SPEC]
bs -> do
                let nbs :: [(FilePath, BASIC_SPEC)]
nbs = [FilePath] -> [BASIC_SPEC] -> [(FilePath, BASIC_SPEC)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([BASIC_SPEC] -> FilePath -> [FilePath]
specNameL [BASIC_SPEC]
bs FilePath
fn) [BASIC_SPEC]
bs
                [(FilePath, BASIC_SPEC)]
nbs2 <- ((FilePath, BASIC_SPEC) -> ResultT IO (FilePath, BASIC_SPEC))
-> [(FilePath, BASIC_SPEC)] -> ResultT IO [(FilePath, BASIC_SPEC)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: FilePath
n, b :: BASIC_SPEC
b) -> case
                    (Token -> FilePath) -> [Token] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> FilePath
rmSuffix (FilePath -> FilePath) -> (Token -> FilePath) -> Token -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> FilePath
tokStr) ([Token] -> [FilePath]) -> [Token] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ BASIC_SPEC -> [Token]
clTexts BASIC_SPEC
b of
                  [txt :: FilePath
txt] -> if FilePath
txt FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
fn then (FilePath, BASIC_SPEC) -> ResultT IO (FilePath, BASIC_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
n, BASIC_SPEC
b) else
                    Result (FilePath, BASIC_SPEC) -> ResultT IO (FilePath, BASIC_SPEC)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (FilePath, BASIC_SPEC)
 -> ResultT IO (FilePath, BASIC_SPEC))
-> Result (FilePath, BASIC_SPEC)
-> ResultT IO (FilePath, BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ (FilePath, BASIC_SPEC) -> FilePath -> Result (FilePath, BASIC_SPEC)
forall a. a -> FilePath -> Result a
justWarn (if Bool
isImport then FilePath
n else FilePath
txt, BASIC_SPEC
b)
                      (FilePath -> Result (FilePath, BASIC_SPEC))
-> FilePath -> Result (FilePath, BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ "filename " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
fn
                        FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " does not match cl-text " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
txt
                  [] -> Result (FilePath, BASIC_SPEC) -> ResultT IO (FilePath, BASIC_SPEC)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (FilePath, BASIC_SPEC)
 -> ResultT IO (FilePath, BASIC_SPEC))
-> Result (FilePath, BASIC_SPEC)
-> ResultT IO (FilePath, BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ (FilePath, BASIC_SPEC) -> FilePath -> Result (FilePath, BASIC_SPEC)
forall a. a -> FilePath -> Result a
justWarn (FilePath
n, BASIC_SPEC
b)
                    (FilePath -> Result (FilePath, BASIC_SPEC))
-> FilePath -> Result (FilePath, BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ "missing cl-text in " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
fn
                  ts :: [FilePath]
ts -> Result (FilePath, BASIC_SPEC) -> ResultT IO (FilePath, BASIC_SPEC)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (FilePath, BASIC_SPEC)
 -> ResultT IO (FilePath, BASIC_SPEC))
-> Result (FilePath, BASIC_SPEC)
-> ResultT IO (FilePath, BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ (FilePath, BASIC_SPEC) -> FilePath -> Result (FilePath, BASIC_SPEC)
forall a. a -> FilePath -> Result a
justWarn (FilePath
n, BASIC_SPEC
b)
                    (FilePath -> Result (FilePath, BASIC_SPEC))
-> FilePath -> Result (FilePath, BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ "multiple cl-text entries in "
                      FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unlines ((FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> FilePath
forall a. Show a => a -> FilePath
show [FilePath]
ts)
                  ) [(FilePath, BASIC_SPEC)]
nbs
                let nbtis :: [(FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))]
nbtis = ((FilePath, BASIC_SPEC)
 -> (FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)))
-> [(FilePath, BASIC_SPEC)]
-> [(FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: FilePath
n, b :: BASIC_SPEC
b) ->
                                 (FilePath
n, (BASIC_SPEC
b, FilePath
file, Set FilePath
topTexts, Set FilePath
importedBy))) [(FilePath, BASIC_SPEC)]
nbs2
                    newSpecMap :: SpecMap
newSpecMap = ((FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))
 -> SpecMap -> SpecMap)
-> SpecMap
-> [(FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))]
-> SpecMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (n :: FilePath
n, bti :: (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
bti) sm :: SpecMap
sm ->
                        ((BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
 -> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
 -> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))
-> FilePath
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> SpecMap
-> SpecMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
unify FilePath
n (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
bti SpecMap
sm
                      ) SpecMap
specMap [(FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))]
nbtis
                (SpecMap
 -> (FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))
 -> ResultT IO SpecMap)
-> SpecMap
-> [(FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))]
-> ResultT IO SpecMap
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ sm :: SpecMap
sm nbt :: (FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))
nbt -> do
                          SpecMap
newDls <- HetcatsOpts
-> FilePath
-> SpecMap
-> (FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))
-> ResultT IO SpecMap
collectDownloads HetcatsOpts
opts FilePath
baseDir SpecMap
sm (FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))
nbt
                          SpecMap -> ResultT IO SpecMap
forall (m :: * -> *) a. Monad m => a -> m a
return (((BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
 -> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
 -> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))
-> SpecMap -> SpecMap -> SpecMap
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
unify SpecMap
newDls SpecMap
sm)
                      ) SpecMap
newSpecMap [(FilePath, (BASIC_SPEC, FilePath, Set FilePath, Set FilePath))]
nbtis

unify :: SpecInfo -> SpecInfo -> SpecInfo
unify :: (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
-> (BASIC_SPEC, FilePath, Set FilePath, Set FilePath)
unify (_, _, s :: Set FilePath
s, p :: Set FilePath
p) (a :: BASIC_SPEC
a, b :: FilePath
b, t :: Set FilePath
t, q :: Set FilePath
q) = (BASIC_SPEC
a, FilePath
b, Set FilePath
s Set FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set FilePath
t, Set FilePath
p Set FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set FilePath
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 :: HetcatsOpts
-> (FilePath, FilePath)
-> FilePath
-> IO (Either FilePath (FilePath, FilePath))
getCLIFContents opts :: HetcatsOpts
opts dirFile :: (FilePath, FilePath)
dirFile baseDir :: FilePath
baseDir =
  let fn :: FilePath
fn = (FilePath -> FilePath -> FilePath)
-> (FilePath, FilePath) -> FilePath
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry FilePath -> FilePath -> FilePath
httpCombine (FilePath, FilePath)
dirFile
      uStr :: FilePath
uStr = HetcatsOpts -> FilePath -> FilePath
useCatalogURL HetcatsOpts
opts
        (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ if FilePath -> Bool
checkUri FilePath
baseDir then FilePath -> FilePath -> FilePath
httpCombine FilePath
baseDir FilePath
fn else FilePath
fn
  in HetcatsOpts
-> [FilePath]
-> FilePath
-> IO (Either FilePath (FilePath, FilePath))
getExtContent HetcatsOpts
opts { libdirs :: [FilePath]
libdirs = FilePath
baseDir FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: HetcatsOpts -> [FilePath]
libdirs HetcatsOpts
opts }
         [".clif", ".clf"] FilePath
uStr

-- retrieves all importations from the text
directImports :: BASIC_SPEC -> Set.Set NAME
directImports :: BASIC_SPEC -> Set Token
directImports (CL.Basic_spec items :: [Annoted BASIC_ITEMS]
items) = [Set Token] -> Set Token
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
  ([Set Token] -> Set Token) -> [Set Token] -> Set Token
forall a b. (a -> b) -> a -> b
$ (Annoted BASIC_ITEMS -> Set Token)
-> [Annoted BASIC_ITEMS] -> [Set Token]
forall a b. (a -> b) -> [a] -> [b]
map ([TEXT_META] -> Set Token
getImports_textMetas ([TEXT_META] -> Set Token)
-> (Annoted BASIC_ITEMS -> [TEXT_META])
-> Annoted BASIC_ITEMS
-> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BASIC_ITEMS -> [TEXT_META]
textsFromBasicItems (BASIC_ITEMS -> [TEXT_META])
-> (Annoted BASIC_ITEMS -> BASIC_ITEMS)
-> Annoted BASIC_ITEMS
-> [TEXT_META]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BASIC_ITEMS -> BASIC_ITEMS
forall a. Annoted a -> a
Anno.item) [Annoted BASIC_ITEMS]
items

clTexts :: BASIC_SPEC -> [NAME]
clTexts :: BASIC_SPEC -> [Token]
clTexts (CL.Basic_spec items :: [Annoted BASIC_ITEMS]
items) =
  (Annoted BASIC_ITEMS -> [Token])
-> [Annoted BASIC_ITEMS] -> [Token]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([TEXT_META] -> [Token]
getClTexts ([TEXT_META] -> [Token])
-> (Annoted BASIC_ITEMS -> [TEXT_META])
-> Annoted BASIC_ITEMS
-> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BASIC_ITEMS -> [TEXT_META]
textsFromBasicItems (BASIC_ITEMS -> [TEXT_META])
-> (Annoted BASIC_ITEMS -> BASIC_ITEMS)
-> Annoted BASIC_ITEMS
-> [TEXT_META]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BASIC_ITEMS -> BASIC_ITEMS
forall a. Annoted a -> a
Anno.item) [Annoted BASIC_ITEMS]
items

textsFromBasicItems :: BASIC_ITEMS -> [TEXT_META]
textsFromBasicItems :: BASIC_ITEMS -> [TEXT_META]
textsFromBasicItems (Axiom_items axs :: [Annoted TEXT_META]
axs) = (Annoted TEXT_META -> TEXT_META)
-> [Annoted TEXT_META] -> [TEXT_META]
forall a b. (a -> b) -> [a] -> [b]
map Annoted TEXT_META -> TEXT_META
forall a. Annoted a -> a
Anno.item [Annoted TEXT_META]
axs

getImports_textMetas :: [TEXT_META] -> Set.Set NAME
getImports_textMetas :: [TEXT_META] -> Set Token
getImports_textMetas = [Set Token] -> Set Token
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Token] -> Set Token)
-> ([TEXT_META] -> [Set Token]) -> [TEXT_META] -> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TEXT_META -> Set Token) -> [TEXT_META] -> [Set Token]
forall a b. (a -> b) -> [a] -> [b]
map (TEXT -> Set Token
getImports_text (TEXT -> Set Token)
-> (TEXT_META -> TEXT) -> TEXT_META -> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TEXT_META -> TEXT
getText)

getClTexts :: [TEXT_META] -> [NAME]
getClTexts :: [TEXT_META] -> [Token]
getClTexts = (TEXT_META -> [Token]) -> [TEXT_META] -> [Token]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TEXT -> [Token]
getClTextTexts (TEXT -> [Token]) -> (TEXT_META -> TEXT) -> TEXT_META -> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TEXT_META -> TEXT
getText)

getClTextTexts :: TEXT -> [NAME]
getClTextTexts :: TEXT -> [Token]
getClTextTexts txt :: TEXT
txt = case TEXT
txt of
  Named_text n :: Token
n t :: TEXT
t _ -> Token
n Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: TEXT -> [Token]
getClTextTexts TEXT
t
  _ -> []

getImports_text :: TEXT -> Set.Set NAME
getImports_text :: TEXT -> Set Token
getImports_text txt :: TEXT
txt = case TEXT
txt of
  Text p :: [PHRASE]
p _ -> [Token] -> Set Token
forall a. Ord a => [a] -> Set a
Set.fromList ([Token] -> Set Token) -> [Token] -> Set Token
forall a b. (a -> b) -> a -> b
$ (PHRASE -> Token) -> [PHRASE] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map PHRASE -> Token
impName ([PHRASE] -> [Token]) -> [PHRASE] -> [Token]
forall a b. (a -> b) -> a -> b
$ (PHRASE -> Bool) -> [PHRASE] -> [PHRASE]
forall a. (a -> Bool) -> [a] -> [a]
filter PHRASE -> Bool
isImportation [PHRASE]
p
  Named_text _ t :: TEXT
t _ -> TEXT -> Set Token
getImports_text TEXT
t

isImportation :: PHRASE -> Bool
isImportation :: PHRASE -> Bool
isImportation ph :: PHRASE
ph = case PHRASE
ph of
  Importation _ -> Bool
True
  _ -> Bool
False

impName :: PHRASE -> NAME
impName :: PHRASE -> Token
impName ph :: PHRASE
ph = case PHRASE
ph of
  Importation (Imp_name n :: Token
n) -> Token
n
  _ -> FilePath -> Token
forall a. HasCallStack => FilePath -> a
error "CL.impName"

topSortSpecs :: Map.Map FilePath (BASIC_SPEC, FilePath, Set.Set FilePath)
  -> [(FilePath, BASIC_SPEC, FilePath)]
topSortSpecs :: Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
-> [(FilePath, BASIC_SPEC, FilePath)]
topSortSpecs specMap :: Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
specMap =
  let (fm :: Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
fm, rm :: Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
rm) = ((BASIC_SPEC, FilePath, Set FilePath) -> Bool)
-> Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
-> (Map FilePath (BASIC_SPEC, FilePath, Set FilePath),
    Map FilePath (BASIC_SPEC, FilePath, Set FilePath))
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition (\ (_, _, is :: Set FilePath
is) -> Set FilePath -> Bool
forall a. Set a -> Bool
Set.null Set FilePath
is) Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
specMap
  in if Map FilePath (BASIC_SPEC, FilePath, Set FilePath) -> Bool
forall k a. Map k a -> Bool
Map.null Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
fm then [] else
     ((FilePath, (BASIC_SPEC, FilePath, Set FilePath))
 -> (FilePath, BASIC_SPEC, FilePath))
-> [(FilePath, (BASIC_SPEC, FilePath, Set FilePath))]
-> [(FilePath, BASIC_SPEC, FilePath)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: FilePath
n, (b :: BASIC_SPEC
b, f :: FilePath
f, _)) -> (FilePath
n, BASIC_SPEC
b, FilePath
f)) (Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
-> [(FilePath, (BASIC_SPEC, FilePath, Set FilePath))]
forall k a. Map k a -> [(k, a)]
Map.toList Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
fm) [(FilePath, BASIC_SPEC, FilePath)]
-> [(FilePath, BASIC_SPEC, FilePath)]
-> [(FilePath, BASIC_SPEC, FilePath)]
forall a. [a] -> [a] -> [a]
++ Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
-> [(FilePath, BASIC_SPEC, FilePath)]
topSortSpecs
         (((BASIC_SPEC, FilePath, Set FilePath)
 -> (BASIC_SPEC, FilePath, Set FilePath))
-> Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
-> Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ (b :: BASIC_SPEC
b, f :: FilePath
f, is :: Set FilePath
is) -> (BASIC_SPEC
b, FilePath
f, Set FilePath
is Set FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Map FilePath (BASIC_SPEC, FilePath, Set FilePath) -> Set FilePath
forall k a. Map k a -> Set k
Map.keysSet Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
fm)) Map FilePath (BASIC_SPEC, FilePath, Set FilePath)
rm)