{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ConstrainedClassMethods #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Parsing.Test where

import qualified Data.Char as Char
import qualified Data.MonoTraversable as MT
import qualified Data.Kind as Kind
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.List as List
import Data.String (IsString(..))
import Data.Proxy

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling (TokenT(..))

-- * Type 'Syntax'
data Syntax a
 =   Syntax a [Syntax a]
 deriving (Eq)
instance Monoid (Syntax Text) where
	mempty = Syntax "" []
	mappend (Syntax "" []) x = x
	mappend x (Syntax "" []) = x
	mappend x y = Syntax " " [x, y]

-- * Class 'Sy'
class Sy c where
	type SyT c
	sy ::
	 ( Show_Const '[Proxy c]
	 , Inj_Const  '[Proxy c] c
	 ) => SyT c
instance Sy (c::Kind.Type) where
	type SyT c = Syntax Text
	sy = Syntax (Text.pack $ show_const (inj_const::Const '[Proxy c] c)) []
instance Sy (c::a -> b) where
	type SyT c = [Syntax Text] -> Syntax Text
	sy = Syntax (Text.pack $ show_const (inj_const::Const '[Proxy c] c))

-- | Custom 'Show' instance a little bit more readable
-- than the automatically derived one.
instance Show (Syntax Text) where
	showsPrec p ast@(Syntax name args) =
		let n = Text.unpack name in
		case ast of
		 Syntax _ [] -> showString n
		 Syntax "(->)" [a] ->
			showParen (p Prelude.<= prec_arrow) $
			showString (""++n++" ") .
			showsPrec prec_arrow a
		 Syntax "(->)" [a, b] ->
			showParen (p Prelude.<= prec_arrow) $
			showsPrec prec_arrow a .
			showString (" -> ") .
			showsPrec (prec_arrow Prelude.+ 1) b
		 Syntax "\\" [var, typ, body] ->
			showParen (p Prelude.<= prec_lambda) $
			showString ("\\(") .
			showsPrec prec_lambda var .
			showString (":") .
			showsPrec prec_lambda typ .
			showString (") -> ") .
			showsPrec prec_lambda body
		 Syntax " " (fun:as) ->
			showParen (p Prelude.<= prec_app) $
			showsPrec prec_dollar fun .
			List.foldl
			 (\acc arg ->
				acc . showString (" ") .
				showsPrec prec_dollar arg)
			 (showString ("")) as
		 Syntax "$" [fun, arg] ->
			showParen (p Prelude.<= prec_dollar) $
			showsPrec prec_dollar fun .
			showString (" $ ") .
			showsPrec prec_dollar arg
		 _ ->
			showParen (p Prelude.<= prec_app) $
			showString n .
			showString " " .
			showString (List.unwords $ show Prelude.<$> args)
		where
		prec_arrow  = 1
		prec_lambda = 1
		prec_dollar = 1
		prec_app    = 10

-- * Class 'Tokenize'
type Tokenize ast meta ts = TokenizeR ast meta ts ts

tokenize :: forall meta ast ts. Tokenize ast meta ts
 => ast -> Either (Error_Syntax ast) (EToken meta ts)
tokenize = tokenizeR (Proxy::Proxy ts)

-- ** Class 'TokenizeR'
class TokenizeR ast meta ts rs where
	tokenizeR :: Proxy rs -> ast -> Either (Error_Syntax ast) (EToken meta ts)
instance
 ( TokenizeT ast meta ts (Proxy Token_Var)
 , TokenizeR ast meta ts ts
 , Inj_Token meta ts (->)
 , Monoid meta
 ) => TokenizeR ast meta ts '[] where
	tokenizeR _rs ast =
		case tokenizeT (Proxy::Proxy (Proxy Token_Var)) ast of
		 Nothing -> Left $ Error_Syntax_unsupported ast
		 Just (Left err) -> Left err
		 Just (Right (as, tok)) ->
			List.foldl (\mf ma -> do
				a <- tokenize ma
				f <- mf
				Right $ EToken $ inj_token (meta_of f `mappend` meta_of a) $
					Token_Term_App f a
			 ) (Right tok) as
instance
 ( TokenizeT ast meta ts t
 , TokenizeR ast meta ts ts
 , TokenizeR ast meta ts rs
 , Inj_Token meta ts (->)
 ) => TokenizeR ast meta ts (t ': rs) where
	tokenizeR _ ast =
		case tokenizeT (Proxy::Proxy t) ast of
		 Nothing -> tokenizeR (Proxy::Proxy rs) ast
		 Just (Left err) -> Left err
		 Just (Right (as, tok)) ->
			List.foldl (\mf ma -> do
				a <- tokenize ma
				f <- mf
				Right $ EToken $ inj_token (meta_of f {-`mappend` meta_of a-}) $
					Token_Term_App f a
			 ) (Right tok) as

-- Type 'Token_Var'
data Token_Var
instance
 Inj_Token (Syntax Text) ts (->) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy Token_Var) where
	tokenizeT _t meta@(Syntax x as)
	 | Just (x0, xs) <- Text.uncons x
	 , Char.isLetter x0 && Char.isLower x0
	 , MT.oall (\c -> Char.isLetter c || Char.isNumber c) xs
	 = Just $ Right $ (as,) $ EToken $ inj_token meta $
		Token_Term_Var x
	tokenizeT _t _sy = Nothing

-- ** Class 'TokenizeT'
class TokenizeT ast meta ts t where
	tokenizeT :: Proxy t -> ast
	 -> Maybe ( Either (Error_Syntax ast)
	                   ([ast], EToken meta ts) )
instance
 ( Inj_Token (Syntax Text) ts (->)
 , Tokenize (Syntax Text) (Syntax Text) ts ) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy (->)) where
	tokenizeT _t (Syntax "\\" (Syntax n [] : ast_ty : ast_te : as)) = Just $ do
		tok_ty <- tokenize_type ast_ty
		tok_te <- tokenize ast_te
		Right $ (as,) $ EToken $
			inj_token (Syntax "\\" [Syntax n [], ast_ty, ast_te]) $
			Token_Term_Abst n tok_ty tok_te
	tokenizeT _t (Syntax " " (ast_f : ast_x : as)) = Just $ do
		tok_f <- tokenize ast_f
		tok_x <- tokenize ast_x
		Right $ (as,) $ EToken $
			inj_token (Syntax " " [ast_f, ast_x]) $
			Token_Term_App tok_f tok_x
	tokenizeT _t (Syntax "let" (Syntax n [] : ast_te : ast_in : as)) = Just $ do
		tok_te <- tokenize ast_te
		tok_in <- tokenize ast_in
		Right $ (as,) $ EToken $
			inj_token (Syntax "let" [Syntax n [], ast_te, ast_in]) $
			Token_Term_Let n tok_te tok_in
	tokenizeT _t _sy = Nothing
instance
 ( Inj_Token (Syntax Text) ts Int
 {-, Tokenize (Syntax Text) (Syntax Text) ts-} ) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy Int) where
	tokenizeT _t (Syntax "int" (ast_i : as)) = Just $ do
		i <- read_syntax ast_i
		Right $ (as,) $ EToken $ inj_token (Syntax "int" [ast_i]) $
			Token_Term_Int i
	tokenizeT _t _sy = Nothing
instance
 ( Inj_Token (Syntax Text) ts []
 , Tokenize (Syntax Text) (Syntax Text) ts ) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy []) where
	tokenizeT _t meta@(Syntax "list" (ast_ty : ast_as)) = Just $ do
		typ <- tokenize_type ast_ty
		as <- tokenize `mapM` ast_as
		Right $ ([],) $ EToken $ inj_token meta $
			Token_Term_List_list typ as
	tokenizeT _t (Syntax "zipWith" (ast_f : as)) = Just $ do
		f <- tokenize ast_f
		Right $ (as,) $ EToken $ inj_token (Syntax "zipWith" [ast_f]) $
			Token_Term_List_zipWith f
	tokenizeT _t _sy = Nothing
instance
 ( Inj_Token (Syntax Text) ts Char ) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy Char) where
	tokenizeT _t (Syntax "char" (ast_c : as)) = Just $ do
		c <- read_syntax ast_c
		Right $ (as,) $ EToken $ inj_token (Syntax "char" [ast_c]) $
			Token_Term_Char c
	tokenizeT _t (Syntax "Char.toUpper" as) = Just $
		Right $ (as,) $ EToken $ inj_token (Syntax "Char.toUpper" []) $
			Token_Term_Char_toUpper
	tokenizeT _t _sy = Nothing
instance
 ( Inj_Token (Syntax Text) ts Text ) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy Text) where
	tokenizeT _t (Syntax "text" (ast_t : as)) = Just $ do
		t <- read_syntax ast_t
		Right $ (as,) $ EToken $ inj_token (Syntax "text" [ast_t]) $
			Token_Term_Text t
	tokenizeT _t _sy = Nothing
instance
 ( Inj_Token (Syntax Text) ts Maybe
 , Tokenize (Syntax Text) (Syntax Text) ts ) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy Maybe) where
	tokenizeT _t (Syntax "Just" (ast_a : as)) = Just $ do
		a <- tokenize ast_a
		Right $ (as,) $ EToken $ inj_token (Syntax "Just" [ast_a]) $
			Token_Term_Maybe_Just a
	tokenizeT _t _sy = Nothing
instance
 ( Inj_Token (Syntax Text) ts (,)
 , Tokenize (Syntax Text) (Syntax Text) ts ) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy (,)) where
	tokenizeT _t (Syntax "(,)" (ast_a : ast_b : as)) = Just $ do
		a <- tokenize ast_a
		b <- tokenize ast_b
		Right $ (as,) $ EToken $ inj_token (Syntax "(,)" [ast_a, ast_b]) $
			Token_Term_Tuple2 a b
	tokenizeT _t (Syntax "fst" (ast_t : as)) = Just $ do
		t <- tokenize ast_t
		Right $ (as,) $ EToken $ inj_token (Syntax "fst" [ast_t]) $
			Token_Term_Tuple2_fst t
	tokenizeT _t (Syntax "snd" (ast_t : as)) = Just $ do
		t <- tokenize ast_t
		Right $ (as,) $ EToken $ inj_token (Syntax "snd" [ast_t]) $
			Token_Term_Tuple2_snd t
	tokenizeT _t _sy = Nothing
instance
 ( Inj_Token (Syntax Text) ts Num
 , Tokenize (Syntax Text) (Syntax Text) ts ) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy Num) where
	tokenizeT _t (Syntax "(+)" (ast_x : as)) = Just $ do
		x <- tokenize ast_x
		Right $ (as,) $ EToken $ inj_token (Syntax "(+)" [ast_x]) $
			Token_Term_Num_add x
	tokenizeT _t _sy = Nothing
instance
 ( Inj_Token (Syntax Text) ts Monoid
 , Tokenize (Syntax Text) (Syntax Text) ts ) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy Monoid) where
	tokenizeT _t (Syntax "mappend" (ast_x : as)) = Just $ do
		x <- tokenize ast_x
		Right $ (as,) $ EToken $ inj_token (Syntax "mappend" [ast_x]) $
			Token_Term_Monoid_mappend x
	tokenizeT _t _sy = Nothing

tokenize_type
 :: Inj_Token (Syntax Text) ts Token_Type
 => Syntax Text
 -> Either (Error_Syntax (Syntax Text)) (EToken (Syntax Text) ts)
tokenize_type meta@(Syntax n as)
 | Just (c, _) <- Text.uncons n
 , (Char.isUpper c && MT.oall Char.isLetter n)
 || MT.oall (\x -> Char.isSymbol x || Char.isPunctuation x)  n =
	EToken . inj_token meta . Token_Type n
	 <$> sequence (tokenize_type <$> as)
tokenize_type syn = Left $ Error_Syntax_unsupported syn

-- * Type 'Error_Syntax'
data Error_Syntax ast
 =   Error_Syntax_read ast Text
 |   Error_Syntax_unsupported ast
 deriving (Eq, Show)

syLam x typ te = Syntax "\\" [syVar x, typ, te]
syVar x = Syntax x []
syApp f x = Syntax " " [f, x]
syLet x b i = Syntax "let" [syVar x, b, i]

syLit :: forall c.
 ( Show_Const '[Proxy c]
 , Inj_Const  '[Proxy c] c
 , Show c
 ) => c -> Syntax Text
syLit x = Syntax n [Syntax (Text.pack $ show x) []]
	where
	c:cs = show_const (inj_const::Const '[Proxy c] c)
	n = Text.cons (Char.toLower c) $ Text.pack cs

syFun :: IsString a => [Syntax a] -> Syntax a
syFun = Syntax "(->)"

(.>) :: IsString a => Syntax a -> Syntax a -> Syntax a
a .> b = syFun [a, b]
infixr 3 .>

read_syntax :: Read a => Syntax Text -> Either (Error_Syntax (Syntax Text)) a
read_syntax ast@(Syntax t as) =
	case reads $ Text.unpack t of
	 [(x, "")] | List.null as -> Right x
	 _ -> Left $ Error_Syntax_read ast t

maybeRight :: Either l r -> Maybe r
maybeRight (Right r) = Just r
maybeRight Left{}    = Nothing