{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Typing.Syntax where

import qualified Data.List as List
import Data.Maybe
import Data.Type.Equality
import Data.String (IsString(..))

import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Constant
import Language.Symantic.Typing.Type
import Language.Symantic.Typing.Constraint

-- * Class 'AST'
class AST node where
	type Lexem node
	ast_lexem :: node -> Lexem node
	ast_nodes :: node -> [node]

instance AST (Syntax a) where
	type Lexem (Syntax a) = a
	ast_lexem (Syntax x _)  = x
	ast_nodes (Syntax _ ns) = ns

-- * Type 'At'
-- | Attach a location.
data At ast a
 =   At ast a
 deriving (Eq, Show)
instance Functor (At ast) where
	fmap f (At ast a) = At ast (f a)

-- * Type 'Syntax'
data Syntax a
 =   Syntax a [Syntax a]
 deriving (Eq)

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

-- * Type 'Error_Type'
data Error_Type cs ast
 =   Error_Type_Constant_unknown    (At ast ())
 |   Error_Type_Kind_mismatch       (At ast EKind) (At ast EKind)
 |   Error_Type_Kind_not_applicable (At ast EKind)
deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Type cs ast)
deriving instance (Show ast, Show (Lexem ast), Show_Const cs) => Show (Error_Type cs ast)

-- * Class 'Type_from'
-- | Try to build a 'Type' from raw data.
class Type_from ast cs where
	type_from
	 :: ast
	 -> (forall ki_h h. Type cs ki_h h -> Either (Error_Type cs ast) ret)
	 -> Either (Error_Type cs ast) ret

instance
 ( Proj_Con cs
 , Const_from (Lexem ast) cs
 , AST ast
 ) => Type_from ast cs where
	type_from ast kk =
		fromMaybe (Left $ Error_Type_Constant_unknown $ At ast ()) $
		const_from (ast_lexem ast) $ \c -> Just $
		go (ast_nodes ast) (TyConst c) kk
		where
		go :: forall ki h ret. [ast]
		 -> Type cs ki h
		 -> (forall ki' h'. Type cs ki' h' -> Either (Error_Type cs ast) ret)
		 -> Either (Error_Type cs ast) ret
		go [] ty k = k ty
		go (ast_x:ast_xs) ty_f k =
			type_from ast_x $ \ty_x ->
			case kind_of ty_f of
			 ki_f_a `SKiArrow` _ki_f_b ->
				let ki_x = kind_of ty_x in
				case testEquality ki_f_a ki_x of
				 Just Refl -> go ast_xs (ty_f :$ ty_x) k
				 Nothing -> Left $ Error_Type_Kind_mismatch
					 (At ast $ EKind ki_f_a)
					 (At ast_x $ EKind ki_x)
			 ki -> Left $ Error_Type_Kind_not_applicable $ At ast (EKind ki)

syBool :: IsString a => Syntax a
syBool = Syntax "Bool" []
syEq :: IsString a => [Syntax a] -> Syntax a
syEq = Syntax "Eq"
syFun :: IsString a => [Syntax a] -> Syntax a
syFun = Syntax "(->)"
syInt :: IsString a => Syntax a
syInt = Syntax "Int" []
syIO :: IsString a => [Syntax a] -> Syntax a
syIO = Syntax "IO"
syTraversable :: IsString a => [Syntax a] -> Syntax a
syTraversable = Syntax "Traversable"
syMonad :: IsString a => [Syntax a] -> Syntax a
syMonad = Syntax "Monad"
(.>) :: IsString a => Syntax a -> Syntax a -> Syntax a
a .> b = syFun [a, b]
infixr 3 .>