module ARIParser where

import TRS
import Text.ParserCombinators.Parsec
        
-- Scanners

comment :: Parser ()
comment = do
  _ <- char ';'
  skipMany (noneOf "\n")

whitespaces :: Parser ()
whitespaces = skipMany (do { _ <- space; return () } <|> comment)

simple_identifier :: Parser String
simple_identifier = do
  whitespaces
  s <- many1 (noneOf "|(); \t\r\n")
  whitespaces
  return s

quoted_identifier :: Parser String
quoted_identifier = do
  whitespaces
  _ <- char '|'
  s <- many1 (noneOf "| \t\r\n")
  _ <- char '|'
  whitespaces
  return ("|" ++ s ++ "|")

identifier :: Parser String
identifier = simple_identifier <|> quoted_identifier

number :: Parser Int
number = do
  whitespaces
  s <- many1 digit
  whitespaces
  return (read s :: Int)

keyword :: String -> Parser ()
keyword s = do
  whitespaces
  _ <- string s
  whitespaces

param :: String -> a -> Parser a
param s x = do
  keyword s
  return x
            
-- Parsing functions.

parse_format :: Parser ()
parse_format = do
  keyword "("
  keyword "format"
  keyword "TRS"
  keyword ")"

parse_fun :: Parser (String, Int)
parse_fun = do
  keyword "("
  keyword "fun"
  f <- identifier
  n <- number
  keyword ")"
  return (f, n)

parse_term :: Signature -> Parser Term
parse_term sig = 
  try (parse_variable_or_constant sig) <|> 
  parse_function sig

parse_variable_or_constant :: Signature -> Parser Term
parse_variable_or_constant sig = do
  x <- identifier
  case lookup x sig of
    Nothing -> return (V x)
    Just 0  -> return (F x [])
    Just _  -> error (x ++ " is not a constant.")

parse_function :: Signature -> Parser Term
parse_function sig = do
  keyword "("
  f <- identifier
  ts <- many (parse_term sig)
  keyword ")"
  case lookup f sig of
    Nothing            -> error (f ++ " is not declared")
    Just n | m == n    -> return (F f ts)
           | m < n     -> error (f ++ " takes too few arguemnts")
           | otherwise -> error (f ++ " takes too many arguments")
      where m = length ts

parse_rule :: Signature -> Parser Rule
parse_rule sig = do
  keyword "("
  keyword "rule"
  l <- parse_term sig
  r <- parse_term sig
  keyword ")"
  return (l, r)

parse_ari :: Parser (Signature, TRS)
parse_ari = do
  parse_format
  sig <- many (try parse_fun)
  rules <- many (parse_rule sig)
  eof
  return (sig, rules)

-- A reader function.

read_ari :: String -> IO (Either ParseError (Signature, TRS))
read_ari file = parseFromFile parse_ari file