{- |
Module      :  ./TPTP/ParseAsLibDefn.hs
Description :  Methods to parse TPTP as a LibDefn
Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Eugen Kuksa <kuksa@iks.cs.ovgu.de>
Stability   :  provisional
Portability :  non-portable (imports Logic)

-}

module TPTP.ParseAsLibDefn (parseTPTP) where

import TPTP.AS as AS
import TPTP.Common
import TPTP.Logic_TPTP as Logic
import TPTP.Parser

import Common.AnnoState
import Common.AS_Annotation (Annoted (..), item)
import Common.Id
import Common.IRI
import Common.LibName
import Common.Parsec
import Common.Result (fatal_error)
import Common.ResultT
import Driver.Options
import Logic.Grothendieck
import Syntax.AS_Library
import Syntax.AS_Structured

import Data.Maybe
import Data.List
import qualified Data.Map as Map
import System.FilePath.Posix
import Text.ParserCombinators.Parsec

parseTPTP :: HetcatsOpts -> FilePath -> String -> ResultT IO [LIB_DEFN]
parseTPTP :: HetcatsOpts -> FilePath -> FilePath -> ResultT IO [LIB_DEFN]
parseTPTP opts :: HetcatsOpts
opts file :: FilePath
file input :: FilePath
input = do
  let tptpParser :: ParsecT FilePath (AnnoState st) Identity [BASIC_SPEC]
tptpParser = ParsecT FilePath (AnnoState st) Identity BASIC_SPEC
-> ParsecT FilePath (AnnoState st) Identity [BASIC_SPEC]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (PrefixMap -> ParsecT FilePath (AnnoState st) Identity BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
parseBasicSpec PrefixMap
forall k a. Map k a
Map.empty) ParsecT FilePath (AnnoState st) Identity [BASIC_SPEC]
-> ParsecT FilePath (AnnoState st) Identity ()
-> ParsecT FilePath (AnnoState st) Identity [BASIC_SPEC]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT FilePath (AnnoState st) Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof
  case 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 GenParser Char (AnnoState ()) [BASIC_SPEC]
forall st. ParsecT FilePath (AnnoState st) Identity [BASIC_SPEC]
tptpParser (() -> AnnoState ()
forall st. st -> AnnoState st
emptyAnnos ())  FilePath
file FilePath
input of
    Left err :: ParseError
err -> do
      Result Any -> ResultT IO Any
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result Any -> ResultT IO Any) -> Result Any -> ResultT IO Any
forall a b. (a -> b) -> a -> b
$ FilePath -> Range -> Result Any
forall a. FilePath -> Range -> Result a
fatal_error (ParseError -> FilePath
forall a. Show a => a -> FilePath
show ParseError
err) Range
nullRange
      [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 -> LIB_DEFN
emptyLibDefn FilePath
file]
    Right basicSpecs :: [BASIC_SPEC]
basicSpecs -> [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
$ (BASIC_SPEC -> LIB_DEFN) -> [BASIC_SPEC] -> [LIB_DEFN]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts -> FilePath -> BASIC_SPEC -> LIB_DEFN
convertToLibDefn HetcatsOpts
opts FilePath
file) [BASIC_SPEC]
basicSpecs
  where

convertToLibDefn :: HetcatsOpts -> FilePath -> BASIC_SPEC -> LIB_DEFN
convertToLibDefn :: HetcatsOpts -> FilePath -> BASIC_SPEC -> LIB_DEFN
convertToLibDefn opts :: HetcatsOpts
opts filepath :: FilePath
filepath spec :: BASIC_SPEC
spec = LibName -> [Annoted LIB_ITEM] -> Range -> [Annotation] -> LIB_DEFN
Lib_defn LibName
libName [Annoted LIB_ITEM]
libItems Range
nullRange []
  where
    -- For the library name, use the part of the @filepath@ that comes after the
    -- library directory.
    -- The lirary directory is the first of the libdirs given by the command
    -- line option --hets-libdirs. If there is no such option, then it is the
    -- directory of the @filepath@.
    libName :: LibName
libName = IRI -> LibName
iriLibName IRI
specName
    specName' :: IRI
specName' = Maybe IRI -> IRI
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe IRI -> IRI) -> Maybe IRI -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe IRI
parseIRICurie (FilePath -> Maybe IRI) -> FilePath -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
escapeTPTPFilePath FilePath
filename
    specName :: IRI
specName = IRI -> IRI
unescapeTPTPFileIRI IRI
specName'
    filename :: FilePath
filename = case FilePath -> FilePath -> Maybe FilePath
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix FilePath
libdir FilePath
filepath of
      Just suffix :: FilePath
suffix -> FilePath
suffix
      Nothing -> FilePath
filename'
    libdir :: FilePath
libdir = case HetcatsOpts -> [FilePath]
libdirs HetcatsOpts
opts of
      l :: FilePath
l : _ -> if FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf "/" FilePath
l then FilePath
l else FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/"
      [] -> FilePath
dirname
    (dirname :: FilePath
dirname, filename' :: FilePath
filename') = FilePath -> (FilePath, FilePath)
splitFileName FilePath
filepath

    libItems :: [Annoted LIB_ITEM]
libItems = TPTP -> Annoted LIB_ITEM
forall lid. Language lid => lid -> Annoted LIB_ITEM
makeLogicItem TPTP
Logic.TPTP Annoted LIB_ITEM -> [Annoted LIB_ITEM] -> [Annoted LIB_ITEM]
forall a. a -> [a] -> [a]
: [Annoted LIB_ITEM]
includedLibs [Annoted LIB_ITEM] -> [Annoted LIB_ITEM] -> [Annoted LIB_ITEM]
forall a. [a] -> [a] -> [a]
++ [Annoted LIB_ITEM
specItem]
    includedLibs :: [Annoted LIB_ITEM]
includedLibs = (IRI -> Annoted LIB_ITEM) -> [IRI] -> [Annoted LIB_ITEM]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> IRI -> Annoted LIB_ITEM
addDownload Bool
False) [IRI]
includes
    includes :: [IRI]
includes = BASIC_SPEC -> [IRI]
directIncludes BASIC_SPEC
spec
    specItem :: Annoted LIB_ITEM
specItem = IRI -> Annoted SPEC -> Annoted LIB_ITEM
makeSpecItem IRI
specName Annoted SPEC
annotedSpec
    annotedSpec :: Annoted SPEC
annotedSpec = [IRI] -> Annoted SPEC -> Annoted SPEC
addImports [IRI]
includes (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
$ TPTP -> 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 TPTP
Logic.TPTP BASIC_SPEC
spec

emptyLibDefn :: FilePath -> LIB_DEFN
emptyLibDefn :: FilePath -> LIB_DEFN
emptyLibDefn filepath :: FilePath
filepath =
  LibName -> [Annoted LIB_ITEM] -> Range -> [Annotation] -> LIB_DEFN
Lib_defn (FilePath -> LibName
emptyLibName (FilePath -> FilePath
convertFileToLibStr FilePath
filepath)) [] Range
nullRange []

-- Retrieves all includes from a basic spec, without recursing into the
-- included documents
directIncludes :: BASIC_SPEC -> [SPEC_NAME]
directIncludes :: BASIC_SPEC -> [IRI]
directIncludes (AS.Basic_spec itemsTPTP :: [Annoted TPTP]
itemsTPTP) = [TPTP] -> [IRI]
importsTPTP ([TPTP] -> [IRI]) -> [TPTP] -> [IRI]
forall a b. (a -> b) -> a -> b
$ (Annoted TPTP -> TPTP) -> [Annoted TPTP] -> [TPTP]
forall a b. (a -> b) -> [a] -> [b]
map Annoted TPTP -> TPTP
forall a. Annoted a -> a
item [Annoted TPTP]
itemsTPTP
  where
    importsTPTP :: [AS.TPTP] -> [SPEC_NAME]
    importsTPTP :: [TPTP] -> [IRI]
importsTPTP = (TPTP -> [IRI]) -> [TPTP] -> [IRI]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TPTP -> [IRI]
includesInTPTP

    includesInTPTP :: AS.TPTP -> [SPEC_NAME]
    includesInTPTP :: TPTP -> [IRI]
includesInTPTP = (TPTP_input -> [IRI]) -> [TPTP_input] -> [IRI]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TPTP_input -> [IRI]
includes ([TPTP_input] -> [IRI]) -> (TPTP -> [TPTP_input]) -> TPTP -> [IRI]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TPTP -> [TPTP_input]
inputsFromTPTP

    inputsFromTPTP :: AS.TPTP -> [TPTP_input]
    inputsFromTPTP :: TPTP -> [TPTP_input]
inputsFromTPTP (AS.TPTP inputs :: [TPTP_input]
inputs) = [TPTP_input]
inputs

    includes :: TPTP_input -> [SPEC_NAME]
    includes :: TPTP_input -> [IRI]
includes tptp_input :: TPTP_input
tptp_input = case TPTP_input
tptp_input of
      TPTP_include (Include filename :: IRI
filename _) -> [IRI
filename]
      _ -> []