{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Calculus.Lambda.Omega.Explicit.Read where

import Control.Applicative (Alternative(..), Applicative(..), (<$>), (<$))
import qualified Control.Applicative as Applicative
import Control.Monad
import Data.Bool
import Data.Char (Char)
import qualified Data.Char as Char
import Data.Either (Either(..))
import Data.Eq (Eq(..))
import Data.Foldable (Foldable(..))
import Data.Function (($), (.), flip)
import qualified Data.List as List
import Data.Maybe (Maybe(..))
import Data.Maybe (catMaybes)
import Data.Text (Text)
import Data.String (String)
import qualified Data.Text as Text
import Text.Parsec ((<?>))
import qualified Text.Parsec as R
import Text.Show (Show(..))

-- import Debug.Trace

import Calculus.Abstraction.DeBruijn.Generalized
import Calculus.Lambda.Omega.Explicit

-- * Type 'Lexer'
type Lexer s m a
 =  R.Stream  s m Char
 => R.ParsecT s Lexer_State m a
type Lexer_State = ()

-- ** Type 'Token'
-- | A lexed token.
data Token
 =   Token_Arrow
 |   Token_Type_0
 |   Token_Equal
 |   Token_Colon
 |   Token_Lambda
 |   Token_Name Text
 |   Token_Paren_Close
 |   Token_Paren_Open
 |   Token_Pi
 deriving (Eq, Show)

-- | A lexed token with location information attached
data Lexed_Token
 =   Lexed_Token Token R.SourcePos
 deriving (Show)

-- | Remove location information from a 'Lexed_Token'
lexed_token :: Lexed_Token -> Token
lexed_token (Lexed_Token tok _) = tok

lex
 :: R.Stream s m Char
 => Lexer s m a
 -> s -> m (Either R.ParseError a)
lex l = R.runParserT l () ""

lex_all :: Lexer s m [Lexed_Token]
lex_all =
	catMaybes
	 <$> R.many lex_token_or_whitespace
	 <*  R.eof

-- | Lex either one token or some whitespace
lex_token_or_whitespace :: Lexer s m (Maybe Lexed_Token)
lex_token_or_whitespace =
	(<|>)
	 (Nothing <$  R.try lex_whitespace)
	 (Just    <$> lex_token)

lex_whitespace :: Lexer s m ()
lex_whitespace =
	R.choice
	 [ () <$ Applicative.some R.space
	 , lex_comment_block
	 , lex_comment_line
	 ]

-- | Lex a @{- ... -}@ comment (perhaps nested).
lex_comment_block :: Lexer s m ()
lex_comment_block = R.try (R.string "{-") *> lex_comment_body

-- | Lex a block comment, without the opening.
lex_comment_body :: Lexer s m ()
lex_comment_body =
	R.choice
	 [ lex_comment_block     *> lex_comment_body
	 , R.try (R.string "-}") *> return ()
	 , R.anyChar             *> lex_comment_body
	 ]

lex_comment_line :: Lexer s m ()
lex_comment_line =
  R.try (R.string "--")
  *> R.manyTill R.anyChar (R.eof <|> (() <$ R.newline))
  *> return ()

lex_token :: Lexer s m Lexed_Token
lex_token =
	Lexed_Token
	 <$> R.choice
	  [ lex_symbol
	  , lex_word
	  -- , Token_Int . fromInteger <$> R.natural R.haskell
	  ]
	 <*> R.getPosition

-- | Lex one non-alphanumeric token
lex_symbol :: Lexer s m Token
lex_symbol = R.choice
  [ Token_Arrow       <$  (R.try (R.string "->") <|> R.string "→")
  , Token_Colon       <$  R.char ':'
  , Token_Equal       <$  R.char '='
  , Token_Lambda      <$  (R.char '\\' <|> R.char 'λ')
  , Token_Type_0      <$  R.char '*'
  , Token_Paren_Close <$  R.char ')'
  , Token_Paren_Open  <$  R.char '('
  , Token_Pi          <$  (R.string "\\/" <|> R.string "Π" <|> R.string "∀")
  ]

lex_word :: Lexer s m Token
lex_word = tokenify <$> lex_name
	where
	tokenify name = Token_Name (Text.pack name)

lex_name :: Lexer s m String
lex_name = (:)
	 <$> (R.letter <|> R.char '_')
	 <*> (R.many (R.alphaNum <|> R.char '_'))

-- * Type 'Parser'
type Parser m a
 =  R.Stream  [Lexed_Token] m Lexed_Token
 => R.ParsecT [Lexed_Token] Parser_State m a
type Parser_State = ()

read
 :: (R.Stream s m Char, Monad m)
 => Parser m a -> s -> m (Either R.ParseError a)
read p s = do
	toks <- lex lex_all s
	case toks of
	 Left err -> return $ Left err
	 Right ts -> parse p ts

parse
 :: R.Stream [Lexed_Token] m Lexed_Token
 => Parser m a
 -> [Lexed_Token]
 -> m (Either R.ParseError a)
parse p = R.runParserT (p <* R.eof) () ""

-- | Like 'R.updatePosChar' but working on 'Lexed_Token'.
updatePosToken
 :: R.SourcePos   -- ^ position of the current token
 -> Lexed_Token   -- ^ current token
 -> [Lexed_Token] -- ^ remaining tokens
 -> R.SourcePos   -- ^ position of the next token
updatePosToken pos _ [] = pos
updatePosToken _   _ (Lexed_Token _ pos : _) = pos

-- | Parse a nullary token.
parse_token
 :: Token -> Parser m ()
parse_token t =
	R.tokenPrim
	 show updatePosToken
	 (guard . (t ==) . lexed_token)

-- | Parse an unary token.
parse_token_1
 :: (Token -> Maybe a)
 -> Parser m a
parse_token_1 untoken =
	R.tokenPrim
	 show updatePosToken
	 (untoken . lexed_token)

-- | 'parse_term' @::=@ 'parse_term_abst' @|@ 'parse_type_abst'
parse_term :: Parser m (Term Var_Name)
parse_term =
	R.try parse_term_abst
	 <|> parse_type_abst
	 <?> "term"

parse_sort :: Parser m (Type Var_Name)
parse_sort =
	Type_Sort . (Type_Level_0,)
	 <$  parse_token Token_Type_0
	 <*> R.option Type_Morphism_Mono
		 (parse_token_1 $ \tok -> case tok of
			 Token_Name "m" -> Just Type_Morphism_Mono
			 Token_Name "p" -> Just Type_Morphism_Poly
			 _              -> Nothing)
	 <?> "sort"

parse_var_name :: Parser m Var_Name
parse_var_name =
	parse_token_1 (\tok ->
		case tok of
		 Token_Name "_" -> Nothing
		 Token_Name n   -> Just n
		 _              -> Nothing)
	 <?> "variable-name"

parse_var_def :: Parser m Var_Name
parse_var_def =
	parse_token_1 (\tok ->
		case tok of
		 Token_Name "_" -> Just ""
		 Token_Name n   -> Just n
		 _              -> Nothing)
	 <?> "variable-definition"

parse_var :: Parser m (Term Var_Name)
parse_var =
	TeTy_Var
	 <$> parse_var_name
	 <?> "variable"

-- | 'parse_app' @::=@ 'parse_atom'@+@
parse_app :: Parser m (Term Var_Name)
parse_app =
	List.foldl1 TeTy_App
	 <$> R.many1 (R.try parse_atom)
	 <?> "application"

-- | 'parse_atom' @::=@ 'parse_sort' @|@ 'parse_var' @|@ @"("@ 'parse_term @")"@
parse_atom :: Parser m (Term Var_Name)
parse_atom =
	R.try parse_sort
	 <|> R.try parse_var
	 <|> R.between
		 (parse_token Token_Paren_Open)
		 (parse_token Token_Paren_Close)
		 parse_term
	 <?> "atom"

-- | 'parse_term_abst' @::=@ @"\"@ 'parse_term_abst_decl'@+@ @"->"@ 'parse_term'
parse_term_abst :: Parser m (Term Var_Name)
parse_term_abst =
	(flip $ foldr (\(x, f_in) t ->
		Term_Abst (Suggest x) f_in ((x =?) `abstract` t)))
	 <$  parse_token Token_Lambda
	 <*> R.many1 parse_term_abst_decl
	 <*  parse_token Token_Arrow
	 <*> parse_term
	 <?> "term_abst"

-- | 'parse_term_abst_decl' @::=@ @"("@ 'parse_var_def' @":"@ 'parse_type' @")"@
parse_term_abst_decl :: Parser m (Var_Name, Type Var_Name)
parse_term_abst_decl =
	(,)
	 <$  parse_token Token_Paren_Open
	 <*> parse_var_def
	 <*  parse_token Token_Colon
	 <*> parse_type
	 <*  parse_token Token_Paren_Close
	 <?> "term_abst_decl"

-- | 'parse_type_abst_decl' @::=@ @"("@ @(@ 'parse_var_def' @":"@ @)?@ 'parse_type' @")"@
parse_type_abst_decl :: Parser m (Var_Name, Type Var_Name)
parse_type_abst_decl =
	(,)
	 <$  parse_token Token_Paren_Open
	 <*> R.option "" (R.try parse_var_def <* parse_token Token_Colon)
	 <*> parse_type
	 <*  parse_token Token_Paren_Close
	 <?> "type_abst_decl"

-- | 'parse_type_abst' @::=@ @(@ 'parse_app' @|@ 'parse_type_abst_decl' @)@ @"->"@ 'parse_type_abst' @|@ 'parse_app'
parse_type_abst :: Parser m (Term Var_Name)
parse_type_abst =
	(R.try
		((\(x, f_in) f_out ->
			Type_Abst (Suggest x) f_in ((x =?) `abstract` f_out))
		 <$> (
			 (R.try (("",) <$> parse_app))
			<|>
			 (R.option () (parse_token Token_Pi)
				 *> parse_type_abst_decl)
		 )
		 <*  parse_token Token_Arrow
		 <*> parse_type_abst))
	 <|> parse_app
	 <?> "type_abst"

-- | 'parse_type' @::=@ 'parse_term'
parse_type :: Parser m (Term Var_Name)
parse_type =
	parse_term <?> "type"

parse_let_or_term :: Parser m (Either (Var_Name, Maybe (Type Var_Name), Term Var_Name) (Term Var_Name))
parse_let_or_term =
	R.option
	 Right
	 (R.try ((\name args maybe_ty te ->
		Left
		 ( name
		 , (\ty -> foldr (\(x, x_ty) t ->
			Type_Abst (Suggest x) x_ty ((x =?) `abstract` t)) ty args
			 ) <$> maybe_ty
			, foldr (\(x, x_ty) t ->
				Term_Abst (Suggest x) x_ty ((x =?) `abstract` t)) te args
		 )
		)<$> parse_var_name
		 <*> R.many parse_term_abst_decl
		 <*> (<|>)
			 (R.try (Just
				 <$  parse_token Token_Colon
				 <*> parse_type))
			 (pure Nothing)
		 <* parse_token Token_Equal
	 ))
	 <*> parse_term

-- | 'parse_let' @::=@ 'parse_var_name' @(@'parse_term_abst_decl'@)*@ @"="@ 'parse_term'
parse_let :: Parser m (Var_Name, Maybe (Type Var_Name), Term Var_Name)
parse_let =
	(\name args maybe_ty te ->
		( name
		, (\ty -> foldr (\(x, x_ty) t ->
			Type_Abst (Suggest x) x_ty ((x =?) `abstract` t)) ty args
		 ) <$> maybe_ty
		, foldr (\(x, x_ty) t ->
			Term_Abst (Suggest x) x_ty ((x =?) `abstract` t)) te args
		)
	)<$> parse_var_name
	 <*> R.many parse_term_abst_decl
	 <*> (<|>)
		 (R.try (Just
			 <$  parse_token Token_Colon
			 <*> parse_type))
		 (pure Nothing)
	 <*  parse_token Token_Equal
	 <*> parse_term
	 <?> "let"

-- | 'parse_assume' @::=@ 'parse_var_name' @":"@ 'parse_type'
parse_assume :: Parser m (Var_Name, Type Var_Name)
parse_assume =
	(,)
	 <$> parse_var_name
	 <*  parse_token Token_Colon
	 <*> parse_type
	 <?> "axiom"

parse_command
 :: R.Stream  s m Char
 => R.ParsecT s () m (String, String)
parse_command =
	(,)
	 <$> (R.option "" (R.try (
			R.char ':'
			 *> R.many (R.satisfy Char.isLetter <|> R.char '_')
			 <* (R.option () $ void $ R.many (void $ R.char ' '))
			 )))
	 <*> R.many (R.try (
		(<|>)
			 (R.try R.newline <* R.lookAhead (R.char ' ' <|> R.char '\t'))
			 (R.satisfy is_horizontal)
	 ))
	where
		is_horizontal c = case c of {'\n' -> False; '\r' -> False; _ -> True}

parse_commands
 :: R.Stream  s m Char
 => R.ParsecT s () m [(String, String)]
parse_commands =
	R.many $ do
		_ <- R.many $ do
			_ <- R.many (R.satisfy is_horizontal_space)
			R.newline
		(c, s) <- parse_command
		_ <- R.many1 $ do
			_ <- R.try (R.many (R.satisfy is_horizontal_space))
			R.newline
		return (c,s)
	where
	is_horizontal_space c = case c of {' ' -> True; '\t' -> True; _ -> False}