content: {- |
  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 _ p = p
  
  parserTraceLineNumber :: String -> CharParser st a -> CharParser st a
  parserTraceLineNumber _ p = do
    s <- getParserState
    if 1 == (sourceColumn $ statePos s)
    then trace (show $ sourceLine $ statePos s) $ return ()
    else return ()
    p
  
  parserTraceFull :: String -> CharParser st a -> CharParser st a
  parserTraceFull msg p = do
    s <- getParserState
    if debug s
    then do
      let outBefore = takeWhile (\ c -> c /= '\n') $ take width (stateInput s)
      trace (parserMessage s outBefore) $ return ()
      parsed <- p
      s' <- getParserState
      let outAfter = takeConsumed outBefore s s'
      trace (successMessage s s' outBefore outAfter) $ return parsed
    else p
    where
      width = 54 :: Int
      space = 5 :: Int
      parserWidth = 24 :: Int
      parsedWidth = 24 :: Int
      debug _ = True -- 6 == (sourceLine $ statePos s)
      -- alternative (useful if parsing a specific line is broken - here: line 6):
      -- debug s = 6 == (sourceLine $ statePos s)
      line s = sourceLine $ statePos s
      column s = sourceColumn $ statePos s
      parserMessage s out =  printf ("%3d.%-4d - %" ++ show width ++ "s%" ++ show space ++ "s     %-" ++ show parserWidth ++ "s") (line s) (column s) out "" msg
      successMessage s s' outBefore outAfter = printf ("%3d.%-4d - %" ++ show width ++ "s%" ++ show space ++ "s --> %-" ++ show parserWidth ++ "s  =  %-"++ show parsedWidth ++"s  FROM  %3d.%-4d - %-s") (line s') (column s') "" "" msg outAfter (line s) (column s) outBefore
      takeConsumed :: String -> State s u -> State s u -> String
      takeConsumed outBefore stateBefore stateAfter =
        let consumedLength = sourceColumn (statePos stateAfter) - sourceColumn (statePos stateBefore)
        in take consumedLength outBefore
  