{- |
Module      :  ./TPTP/Parse.hs
Description :  A Parser for the TPTP Syntax v6.4.0.11
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 :  portable

A Parser for the TPTP Input Syntax v6.4.0.11 taken from
<http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>

References

[1] G. Sutcliffe et al.: The TPTP language grammar in BNF.
    <http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>

    Note: The implemented version is saved at TPTP/Documents/SyntaxBNF.html

    Note: The names of the data types are aligned with the names of the
    grammar rules at this reference page (modulo case).
-}

module Common.DebugParser where

import Text.ParserCombinators.Parsec hiding (space)

import Debug.Trace
import Text.Printf

parserTraceId :: String -> CharParser st a -> CharParser st a
parserTraceId :: String -> CharParser st a -> CharParser st a
parserTraceId _ p :: CharParser st a
p = CharParser st a
p

parserTraceLineNumber :: String -> CharParser st a -> CharParser st a
parserTraceLineNumber :: String -> CharParser st a -> CharParser st a
parserTraceLineNumber _ p :: CharParser st a
p = do
  State String st
s <- ParsecT String st Identity (State String st)
forall (m :: * -> *) s u. Monad m => ParsecT s u m (State s u)
getParserState
  if 1 Column -> Column -> Bool
forall a. Eq a => a -> a -> Bool
== (SourcePos -> Column
sourceColumn (SourcePos -> Column) -> SourcePos -> Column
forall a b. (a -> b) -> a -> b
$ State String st -> SourcePos
forall s u. State s u -> SourcePos
statePos State String st
s)
  then String
-> ParsecT String st Identity () -> ParsecT String st Identity ()
forall a. String -> a -> a
trace (Column -> String
forall a. Show a => a -> String
show (Column -> String) -> Column -> String
forall a b. (a -> b) -> a -> b
$ SourcePos -> Column
sourceLine (SourcePos -> Column) -> SourcePos -> Column
forall a b. (a -> b) -> a -> b
$ State String st -> SourcePos
forall s u. State s u -> SourcePos
statePos State String st
s) (ParsecT String st Identity () -> ParsecT String st Identity ())
-> ParsecT String st Identity () -> ParsecT String st Identity ()
forall a b. (a -> b) -> a -> b
$ () -> ParsecT String st Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  else () -> ParsecT String st Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  CharParser st a
p

parserTraceFull :: String -> CharParser st a -> CharParser st a
parserTraceFull :: String -> CharParser st a -> CharParser st a
parserTraceFull msg :: String
msg p :: CharParser st a
p = do
  State String st
s <- ParsecT String st Identity (State String st)
forall (m :: * -> *) s u. Monad m => ParsecT s u m (State s u)
getParserState
  if State String st -> Bool
forall p. p -> Bool
debug State String st
s
  then do
    let outBefore :: String
outBefore = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\ c :: Char
c -> Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '\n') (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Column -> String -> String
forall a. Column -> [a] -> [a]
take Column
width (State String st -> String
forall s u. State s u -> s
stateInput State String st
s)
    String
-> ParsecT String st Identity () -> ParsecT String st Identity ()
forall a. String -> a -> a
trace (State String st -> String -> String
forall t t s u. (PrintfArg t, PrintfType t) => State s u -> t -> t
parserMessage State String st
s String
outBefore) (ParsecT String st Identity () -> ParsecT String st Identity ())
-> ParsecT String st Identity () -> ParsecT String st Identity ()
forall a b. (a -> b) -> a -> b
$ () -> ParsecT String st Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    a
parsed <- CharParser st a
p
    State String st
s' <- ParsecT String st Identity (State String st)
forall (m :: * -> *) s u. Monad m => ParsecT s u m (State s u)
getParserState
    let outAfter :: String
outAfter = String -> State String st -> State String st -> String
forall s u. String -> State s u -> State s u -> String
takeConsumed String
outBefore State String st
s State String st
s'
    String -> CharParser st a -> CharParser st a
forall a. String -> a -> a
trace (State String st -> State String st -> String -> String -> String
forall t t t s u s u.
(PrintfArg t, PrintfArg t, PrintfType t) =>
State s u -> State s u -> t -> t -> t
successMessage State String st
s State String st
s' String
outBefore String
outAfter) (CharParser st a -> CharParser st a)
-> CharParser st a -> CharParser st a
forall a b. (a -> b) -> a -> b
$ a -> CharParser st a
forall (m :: * -> *) a. Monad m => a -> m a
return a
parsed
  else CharParser st a
p
  where
    width :: Column
width = 54 :: Int
    space :: Column
space = 5 :: Int
    parserWidth :: Column
parserWidth = 24 :: Int
    parsedWidth :: Column
parsedWidth = 24 :: Int
    debug :: p -> Bool
debug _ = Bool
True -- 6 == (sourceLine $ statePos s)
    -- alternative (useful if parsing a specific line is broken - here: line 6):
    -- debug s = 6 == (sourceLine $ statePos s)
    line :: State s u -> Column
line s :: State s u
s = SourcePos -> Column
sourceLine (SourcePos -> Column) -> SourcePos -> Column
forall a b. (a -> b) -> a -> b
$ State s u -> SourcePos
forall s u. State s u -> SourcePos
statePos State s u
s
    column :: State s u -> Column
column s :: State s u
s = SourcePos -> Column
sourceColumn (SourcePos -> Column) -> SourcePos -> Column
forall a b. (a -> b) -> a -> b
$ State s u -> SourcePos
forall s u. State s u -> SourcePos
statePos State s u
s
    parserMessage :: State s u -> t -> t
parserMessage s :: State s u
s out :: t
out =  String -> Column -> Column -> t -> String -> String -> t
forall r. PrintfType r => String -> r
printf ("%3d.%-4d - %" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Column -> String
forall a. Show a => a -> String
show Column
width String -> String -> String
forall a. [a] -> [a] -> [a]
++ "s%" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Column -> String
forall a. Show a => a -> String
show Column
space String -> String -> String
forall a. [a] -> [a] -> [a]
++ "s     %-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Column -> String
forall a. Show a => a -> String
show Column
parserWidth String -> String -> String
forall a. [a] -> [a] -> [a]
++ "s") (State s u -> Column
forall s u. State s u -> Column
line State s u
s) (State s u -> Column
forall s u. State s u -> Column
column State s u
s) t
out "" String
msg
    successMessage :: State s u -> State s u -> t -> t -> t
successMessage s :: State s u
s s' :: State s u
s' outBefore :: t
outBefore outAfter :: t
outAfter = String
-> Column
-> Column
-> String
-> String
-> String
-> t
-> Column
-> Column
-> t
-> t
forall r. PrintfType r => String -> r
printf ("%3d.%-4d - %" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Column -> String
forall a. Show a => a -> String
show Column
width String -> String -> String
forall a. [a] -> [a] -> [a]
++ "s%" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Column -> String
forall a. Show a => a -> String
show Column
space String -> String -> String
forall a. [a] -> [a] -> [a]
++ "s --> %-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Column -> String
forall a. Show a => a -> String
show Column
parserWidth String -> String -> String
forall a. [a] -> [a] -> [a]
++ "s  =  %-"String -> String -> String
forall a. [a] -> [a] -> [a]
++ Column -> String
forall a. Show a => a -> String
show Column
parsedWidth String -> String -> String
forall a. [a] -> [a] -> [a]
++"s  FROM  %3d.%-4d - %-s") (State s u -> Column
forall s u. State s u -> Column
line State s u
s') (State s u -> Column
forall s u. State s u -> Column
column State s u
s') "" "" String
msg t
outAfter (State s u -> Column
forall s u. State s u -> Column
line State s u
s) (State s u -> Column
forall s u. State s u -> Column
column State s u
s) t
outBefore
    takeConsumed :: String -> State s u -> State s u -> String
    takeConsumed :: String -> State s u -> State s u -> String
takeConsumed outBefore :: String
outBefore stateBefore :: State s u
stateBefore stateAfter :: State s u
stateAfter =
      let consumedLength :: Column
consumedLength = SourcePos -> Column
sourceColumn (State s u -> SourcePos
forall s u. State s u -> SourcePos
statePos State s u
stateAfter) Column -> Column -> Column
forall a. Num a => a -> a -> a
- SourcePos -> Column
sourceColumn (State s u -> SourcePos
forall s u. State s u -> SourcePos
statePos State s u
stateBefore)
      in Column -> String -> String
forall a. Column -> [a] -> [a]
take Column
consumedLength String
outBefore