-- Copyright 2006, Sascha Boehme.




-- | This module defines a parser to create a 'NamedType' out of a string.
--   The parser itself is based on Parsec.

module FreeTheorems.TypeParser (
    parseNamedType,
    parseType,

    -- testing interface
--  testTypeParser
) where



import FreeTheorems.Declarations
import FreeTheorems.Preparation
import FreeTheorems.PrettyPrint
import FreeTheorems.Types
import Data.Char (isLower, isUpper, isAlphaNum, isSpace, isDigit)
import Text.ParserCombinators.Parsec

-- import FreeTheorems.Test.ArbitraryTypes
-- import Test.QuickCheck (quickCheck)





-- | Parses a Haskell type string and creates a named type.
--
--   The content of the string argument has to be conforming to the following
--   EBNF syntax:
--
-- > NamedType ::= Name :: TypeTerm
--
--   where @Name@ is a token starting with a lower letter or @_@, and
--   consisting of alphanumeric letters and the characters @_@ and @'@ from the
--   second character onwards. A @Name@ starting with @_@ has to be at least two
--   characters long, because @_@ is a reserved identifier in Haskell.
--
--   Alternatively, a @Name@ can also be an operator which has to be enclosed in
--   parentheses. Allowed characters of operators are
--
-- > ! | # | $ | % | & | * | + | . | / | < | = | > | ? | @ | \ | ^ | | | - | ~
--
--   and the colon @:@ from the second although character onwards.
--   Note that the following operators are restricted keywords in Haskell and
--   can not be used as names of types:
--
-- > .. | : | :: | = | \ | | | <- | -> | @ | ~ | =>
--
--   For the syntax of a @TypeTerm@ see 'parseType'.

parseNamedType :: String                            -- ^ The string to be
                                                    --   parsed.
                  -> Either ParseError NamedType    -- ^ Returns the parsed
                                                    --   named type or a parser
                                                    --   error.
parseNamedType string =
  case runParser namedType () "" string of
    Left error             -> Left error
    Right (NamedType tv t) -> Right (NamedType tv (prepare t))



-- | Parses a Haskell type string and creates a named type.
--
--   A type string has to be conforming to the following EBNF syntax:
--
-- > TypeTerm ::= SimpleTypeTerm
-- >            | SimpleTypeTerm "->" TypeTerm
-- >            | "forall" TypeVariableList "." TypeTerm
--
-- > SimpleTypeTerm ::= ATypeTerm
-- >                  | TypeConstructor ATypeTermList
-- >                  | "[]" ATypeTerm
-- >                  | "(,)" ATypeTerm ATypeTerm
-- >                  | "(,,)" ATypeTerm ATypeTerm ATypeTerm
-- >                  | ...
-- >                  | {- tuple in prefix notation of arity 15 -}
-- >                  | "(->)" ATypeTerm ATypeTerm
--
-- > ATypeTerm ::= "Char" | "Int" | "Integer" | "Float" | "Double"
-- >             | TypeVariable
-- >             | "()"
-- >             | "[" TypeTerm "]"
-- >             | "(" TypeTerm "," TypeTerm ")"
-- >             | "(" TypeTerm "," TypeTerm "," TypeTerm ")"
-- >             | ...
-- >             | {- tuple of arity 15 -}
-- >             | "(" TypeTerm ")"
--
-- > ATypeTermList ::= ATypeTerm
-- >                 | ATypeTermList ATypeTerm
--
-- > TypeVariableList ::= TypeVariable
-- >                    | TypeVariableList TypeVariable
--
--   where @TypeVariable@ is a token starting with a lower letter or @_@, while
--   @TypeConstructor@ starts with a capital letter. Every of these two tokens
--   may consist of alphanumeric letters and the characters @_@ and @'@ from the
--   second character onwards.
--   A @TypeVariable@ starting with @_@ has to be at least two characters long,
--   because @_@ is a reserved identifier in Haskell.
--   Type constructors can not be formed from symbols.
--
--   Although tuples are restricted to an arity of 15, tuples in the usual
--   non-prefixed way can be arbitrary large. However, applications should not
--   rely on this possibility.
--
--   An additional rule limits the valid type terms: The number of type
--   arguments for a type constructor must match the type constructors arity.

parseType :: (String -> Bool)       -- ^ When 'parseType' is trying to
                                    --   automatically create a name for the
                                    --   type, this function is asked if a name
                                    --   is acceptable.

             -> String              -- ^ The string to be parsed.

             -> Either ParseError NamedType
                                    -- ^ Returns the parsed named type with
                                    --   the generated name or an parser
                                    --   error.
parseType accept string =
  case runParser onlyType () "" string of
    Left error -> Left error
    Right t    -> Right (NamedType (newName (TV "t" 1) accept) (prepare t))
  where
    newName v@(TV t i) accept = if accept (printAsText v)
                                  then v
                                  else newName (TV t (i+1)) accept



--------------------------------------------------------------------------------



-- Parser for the above syntax.



-- | The parser type used throughout this module.
--   This type was just defined to make the type following annotations shorter.

type CLParser a = GenParser Char () a



-- | Parses a named type.
--   This is a top-level parser, i.e. it requests end of input when finished.

namedType :: CLParser NamedType
namedType = do
  skipSpace
  n <- (typeName <?> "name of a type")
  symbol "::"
  t <- typeTerm
  eof

  -- separate the parsed name in name and index, if possible
  let (rd, rn) = span isDigit $ reverse n
  let (n', digits) = (reverse rn, reverse rd)
  let tv = if (digits == [])
             then PV n'
             else TV n' (read digits)

  return (NamedType tv t)



-- | Parses a type only.
--   This is a top-level parser, i.e. it requests end of input when finished.

onlyType :: CLParser Type
onlyType = do
  skipSpace
  t <- typeTerm
  eof
  return t



-- | Parses a type term consisting of functions or type abstractions,
--   both of which are based on simple type terms.

typeTerm :: CLParser Type
typeTerm =

  -- parse type abstractions
  -- This is different to the above EBNF definition to allow for finding
  -- the keyword "forall" before any type variables. Thus, the parser gets
  -- a bit simpler.
      do try (keyword "forall")
         vs <- many1 typeVariable
         symbol "."
         t <- typeTerm
         return (foldr (\v t -> TypeForall v t) t vs)

  -- parse a simple type term possibly being part of a function type
  <|> simpleTypeTerm `chainr1` function



-- | Parses the function symbol and returns a function to create a function
--   type term out of two type terms.

function :: CLParser (Type -> Type -> Type)
function = do
  symbol "->"
  return (\t1 t2 -> TypeFun t1 t2)



-- | Parses a simple type term.

--   The cases are ordered so that first predefined type constructors in prefix
--   notatation are checked, then basic type terms, and finally type
--   constructors are parsed.

simpleTypeTerm :: CLParser Type
simpleTypeTerm =
      do try (symbol "[]" <?> "prefixed list constructor")
         t <- aTypeTerm
         return (TypeList t)

  <|> do n <- (tupleConstructor <?> "prefixed tuple constructor")
         ts <- count n aTypeTerm
         return (TypeTuple ts)

  <|> do try (symbol "(->)" <?> "prefixed function constructor")
         t1 <- aTypeTerm
         t2 <- aTypeTerm
         return (TypeFun t1 t2)

  <|> aTypeTerm

  <|> do (c, n) <- (typeConstructor <?> "type constructor")
         ts <- count n aTypeTerm
         return (TypeCon c ts)

  <?> "a simple type term"



-- | Parses a basic type term.

aTypeTerm :: CLParser Type
aTypeTerm =
      do try (keyword "Char")
         return (TypeBasic Char)
  <|> do try (keyword "Int")
         return (TypeBasic Int)
  <|> do try (keyword "Integer")
         return (TypeBasic Integer)
  <|> do try (keyword "Float")
         return (TypeBasic Float)
  <|> do try (keyword "Double")
         return (TypeBasic Double)

  <|> do v <- (typeVariable <?> "type variable")
         return (TypeVar v)

  <|> do t <- between (symbol "[") (symbol "]") typeTerm
         return (TypeList t)

  <|> do l <- between (symbol "(") (symbol ")") (typeTerm `sepBy` (symbol ","))
         return $ case l of
                    []        -> TypeUnit
                    [t]       -> t
                    otherwise -> (TypeTuple l)

  <?> ("a basic type, a type variable or a list or tuple type term "
       ++ "like [a] or (a,b)")


--------------------------------------------------------------------------------



-- The lexer for the above parser's tokens.
-- After every token, spaces are skipped.


-- | Parses a name (of an identifier).

name :: CLParser String
name =
      do c  <- char '_'
         cs <- (many1 hsID <?> "at least one more character after \"_\"")
         skipSpace
         return (c:cs)

  <|> do c  <- hsSmall
         cs <- many hsID
         skipSpace
         return (c:cs)



-- | Parses a name of a type which can be either an identifier or an operator.

typeName :: CLParser String
typeName =
     name
 <|> do char '('
        op1 <- hsOperator1
        ops <- many hsOperator
        let op = op1 : ops
        if any (== op) reservedOps
          then unexpected ("reserved operator \"" ++ op ++ "\"")
          else do char ')'
                  skipSpace
                  return ("(" ++ op ++ ")")
  where
    reservedOps =
      [ "..", ":", "::", "=", "\\", "|", "<-", "->", "@", "~", "=>" ]



-- | Parses a type variable. Note that there can not be a type variable called
--   "forall".

typeVariable :: CLParser TypeVariable
typeVariable = do
  n <- name
  if (n == "forall")
    then unexpected "reserved word \"forall\"" <?> "type variable"
    else return n



-- | Parses a type constructor.
--   This function checks, if the parsed type constructor is accepted in the
--   given language subset. If so, it returns also the arity of the type
--   constructor.
--   If the parsed type constructor is not valid, an error message is created.

typeConstructor :: CLParser (TypeConstructor, Int)
typeConstructor = do
  c  <- hsLarge
  cs <- many hsID
  let con = c:cs
  if (not $ isDefined con)
    then unexpected ("type constructor '" ++ con ++ "' " ++
                     "(this type constructor is not declared)")
    else do
      let Just n = getArity con
      skipSpace
      return (con, n)



-- | Parses a tuple type constructor as @(,)@ or @(,,)@.
--   Returns the arity of the parsed tuple type constructor.

tupleConstructor :: CLParser Int
tupleConstructor = do
  try (string "(,")
  cs <- many (char ',')
  char ')'
  skipSpace
  return (length cs + 2)



-- | Checks if a symbol (consisting of operator characters) is at the current
--   position of the input.

symbol :: String -> CLParser ()
symbol s = do
  string s
  skipSpace
  return ()



-- | Checks if a keyword (consisting of alphanumeric characters) is at the
--   current position of the input. Assures also, that after this keyword no
--   other alphanumeric character is following.

keyword :: String -> CLParser ()
keyword s = do
  string s
  notFollowedBy hsID
  skipSpace
  return ()



-- | Skips zero or more space characters.

skipSpace :: CLParser ()
skipSpace = skipMany hsSpace



-- | Returns a lower letter character (see 'name').

hsSmall :: CLParser Char
hsSmall = satisfy $ \c -> isLower c



-- | Returns a capital letter character (see 'typeConstructor').

hsLarge :: CLParser Char
hsLarge = satisfy $ \c -> isUpper c



-- | Returns an alphanumeric character of which keywords and identifiers can be
--   formed.

hsID :: CLParser Char
hsID = satisfy $ \c -> isAlphaNum c || (c == '_') || (c == '\'')



-- | Returns a symbol which can be the first character of an operator function.

hsOperator1 :: CLParser Char
hsOperator1 = satisfy $ \c -> any (== c) "!#$%&*+./<=>?@\\^|-~"



-- | Returns a symbol of which operators can be formed.

hsOperator :: CLParser Char
hsOperator = satisfy $ \c -> any (== c) "!#$%&*+./<=>?@\\^|-~:"



-- | Returns a space character.

hsSpace :: CLParser Char
hsSpace = satisfy $ \c -> isSpace c



--------------------------------------------------------------------------------



-- Helper function



-- | Returns the arity of a type constructor or @Nothing@ if the type
--   constructor is not accepted in the given language subset.

getArity :: TypeConstructor -> Maybe Int
getArity con =
  case (getDataDecl con) of
    Just (DataDecl _ len _) -> Just len
    Nothing                 ->
      case (getTypeDecl con) of
        Just (TypeDecl _ len _) -> Just len
        Nothing                 -> Nothing



--------------------------------------------------------------------------------



-- A list of tests for this module.

{-
testTypeParser = do
  putStr "parser for named types works ... "
  quickCheck prop_parser_NamedType
  putStr "parser for types works ... "
  quickCheck prop_parser_Type
-}



-- Checks the type parser for named types.

prop_parser_NamedType nt =
  case parseNamedType (printAsText nt) of
    Left _    -> False
    Right nt' -> let NamedType tv t = nt
                 in  NamedType tv (prepare t) == nt'



-- Checks the type parser for types only.

prop_parser_Type t =
  let nt   = NamedType (PV "t") t
      text = drop 4 (printAsText nt)
  in  case parseType (\_ -> True) text of
        Left _                 -> False
        Right (NamedType _ t') -> prepare t == t'