{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Type.Common where

import Data.Maybe (isJust)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Language.Symantic.Lib.Data.Peano
import GHC.Prim (Constraint)

-- * Class 'Eq_Type'

-- | Test two types for equality,
-- returning an Haskell type-level proof
-- of the equality when it holds.
class Eq_Type (ty:: * -> *) where
	eq_type :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)

-- * Class 'Constraint_Type'
-- | Test if a type satisfies a given 'Constraint',
-- returning an Haskell type-level proof
-- of that satisfaction when it holds.
class Constraint_Type (c:: * -> Constraint) (ty:: * -> *) where
	constraint_type :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
	constraint_type _c _ = Nothing

-- * Class 'Constraint1_Type'
class Constraint1_Type (c:: (* -> *) -> Constraint) (ty:: * -> *) where
	constraint1_type :: forall f a. Proxy c -> ty (f a) -> Maybe (Dict (c f))
	constraint1_type _c _ = Nothing

-- ** Type 'Dict'
-- | 'Dict' captures the dictionary of a 'Constraint':
-- pattern matching on the 'Dict' constructor
-- brings the 'Constraint' into scope.
data Dict :: Constraint -> * where
	Dict :: c => Dict c

-- * Type 'Exists_Dict'
data Exists_Dict
 = forall c. Exists_Dict (Dict c)

-- * Class 'Type_from'
-- | Parse given @ast@ into a 'Root_of_Type',
-- or return an 'Error_of_Type'.
class Eq_Type ty => Type_from ast (ty:: * -> *) where
	type_from
	 :: Proxy ty
	 -> ast
	 -> (forall h. Root_of_Type ty h
	            -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
	 ->            Either (Error_of_Type ast (Root_of_Type ty)) ret

-- ** Type family 'Root_of_Type'
-- | Return the root type of a type.
type family Root_of_Type (ty:: * -> *) :: * -> *

-- ** Type family 'Error_of_Type'
-- | Return the error type of a type.
type family Error_of_Type (ast:: *) (ty:: * -> *) :: *

-- * Type 'No_Type'
-- | A discarded type.
data No_Type (root:: * -> *) h
 =   No_Type (root h)
 deriving (Eq, Show)

-- * Type 'Type_Root'
-- | The root type, passing itself as parameter to the given type.
newtype Type_Root (ty:: (* -> *) -> * -> *) h
 =      Type_Root { unType_Root :: ty (Type_Root ty) h }
type instance Root_of_Type (Type_Root ty) = Type_Root ty
-- type instance Root_of_Type (ty (Type_Root ty)) = Type_Root ty
type instance Error_of_Type ast (Type_Root ty)
 = Error_Type_Alt (Error_Type ast)
                  (Error_of_Type ast (ty (Type_Root ty)))
instance -- Eq_Type
 Eq_Type (ty (Type_Root ty)) =>
 Eq_Type (Type_Root ty) where
	eq_type (Type_Root x) (Type_Root y) = x `eq_type` y
instance -- Eq
 Eq_Type (Type_Root ty) =>
 Eq (Type_Root ty h) where
	x == y = isJust $ x `eq_type` y
instance -- Constraint_Type c Type_Root
 Constraint_Type c (ty (Type_Root ty)) =>
 Constraint_Type c (Type_Root ty) where
	constraint_type c (Type_Root ty) = constraint_type c ty
instance -- Constraint1_Type c Type_Root
 Constraint1_Type c (ty (Type_Root ty)) =>
 Constraint1_Type c (Type_Root ty) where
	constraint1_type c (Type_Root ty) = constraint1_type c ty
instance -- Type_from
 ( Eq_Type (Type_Root ty)
 , Type_from ast (ty (Type_Root ty))
 , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 ) => Type_from ast (Type_Root ty) where
	type_from _ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
instance -- String_from_Type
 String_from_Type (ty (Type_Root ty)) =>
 String_from_Type (Type_Root ty) where
	string_from_type (Type_Root ty) = string_from_type ty
instance -- Show
 String_from_Type (Type_Root ty) =>
 Show (Type_Root ty h) where
	show = string_from_type

-- ** Class 'Type_Root_Lift'
-- | Lift a given type to a given root type.
class Type_Root_Lift ty root where
	type_root_lift :: forall h. ty root h -> root h
instance
 Type_Lift ty root =>
 Type_Root_Lift ty (Type_Root root) where
	type_root_lift = Type_Root . type_lift

-- * Type 'Type_Alt'
-- | Type making an alternative between two types.
data Type_Alt curr next (root:: * -> *) h
 =   Type_Alt_Curr (curr root h)
 |   Type_Alt_Next (next root h)
-- | Convenient alias. Requires @TypeOperators@.
type (:|:) = Type_Alt
infixr 5 :|:
type instance Root_of_Type (Type_Alt curr next root) = root
type instance Error_of_Type ast (Type_Alt curr next root)
 = Error_of_Type_Alt ast (Error_of_Type ast (curr root))
                         (Error_of_Type ast (next root))
-- ** Type family 'Error_of_Type_Alt'
-- | Remove 'No_Type' type when building 'Error_of_Type'.
type family Error_of_Type_Alt ast curr next where
	Error_of_Type_Alt ast curr          No_Error_Type = curr
	Error_of_Type_Alt ast No_Error_Type next          = next
	Error_of_Type_Alt ast curr          next          = Error_Type_Alt curr next

-- ** Type 'No_Error_Type'
-- | A discarded error.
data No_Error_Type
 =   No_Error_Type
 deriving (Eq, Show)

instance -- Eq_Type
 ( Eq_Type (curr root)
 , Eq_Type (next root)
 ) => Eq_Type (Type_Alt curr next root) where
	eq_type (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type` y
	eq_type (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type` y
	eq_type _ _ = Nothing
instance -- Eq
 ( Eq_Type (curr root)
 , Eq_Type (next root)
 ) => Eq (Type_Alt curr next root h) where
	x == y = isJust $ x `eq_type` y
instance -- Constraint_Type c Type_Alt
 ( Constraint_Type c (curr root)
 , Constraint_Type c (next root)
 ) => Constraint_Type c (Type_Alt curr next root) where
	constraint_type c (Type_Alt_Curr ty) = constraint_type c ty
	constraint_type c (Type_Alt_Next ty) = constraint_type c ty
instance -- Constraint1_Type c Type_Alt
 ( Constraint1_Type c (curr root)
 , Constraint1_Type c (next root)
 ) => Constraint1_Type c (Type_Alt curr next root) where
	constraint1_type c (Type_Alt_Curr ty) = constraint1_type c ty
	constraint1_type c (Type_Alt_Next ty) = constraint1_type c ty
instance -- Type_from
 ( Eq_Type (curr root)
 , Type_from ast (curr root)
 , Type_from ast (next root)
 , Root_of_Type (curr root) ~ root
 , Root_of_Type (next root) ~ root
 , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
 ) => Type_from ast (Type_Alt curr next root) where
	type_from _ty ast k =
		case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
		 Right ret -> ret
		 Left err ->
			case error_type_unlift err of
			 Just (Error_Type_Unsupported_here (_::ast)) ->
				type_from (Proxy::Proxy (next root)) ast k
			 _ -> Left err
instance -- String_from_Type
 ( String_from_Type (curr root)
 , String_from_Type (next root)
 ) => String_from_Type (Type_Alt curr next root) where
	string_from_type (Type_Alt_Curr t) = string_from_type t
	string_from_type (Type_Alt_Next t) = string_from_type t

-- ** Type 'Type_Lift'
-- | Apply 'Peano_of_Type' on 'Type_LiftN'.
type Type_Lift ty tys
 =   Type_LiftN (Peano_of_Type ty tys) ty tys

-- *** Type 'Peano_of_Type'
-- | Return a 'Peano' number derived from the location
-- of a given type within a given type stack,
-- which is used to avoid @OverlappingInstances@.
type family Peano_of_Type
 (ty::  (* -> *) -> * -> *)
 (tys:: (* -> *) -> * -> *) :: * where
	Peano_of_Type ty    ty                   = Zero
	Peano_of_Type ty    (Type_Alt ty   next) = Zero
	Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)

-- *** Class 'Type_LiftN'
-- | Lift a given type to the top of a given type stack including it,
-- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
class Type_LiftN (p:: *) ty tys where
	type_liftN :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
instance Type_LiftN Zero curr curr where
	type_liftN _ = id
instance Type_LiftN Zero curr (Type_Alt curr next) where
	type_liftN _ = Type_Alt_Curr
instance
 Type_LiftN p other next =>
 Type_LiftN (Succ p) other (Type_Alt curr next) where
	type_liftN _ = Type_Alt_Next . type_liftN (Proxy::Proxy p)

-- | Convenient wrapper around 'type_liftN',
-- passing it the 'Peano' number from 'Peano_of_Type'.
type_lift
 :: forall ty tys (root:: * -> *) h.
 Type_Lift ty tys =>
 ty root h -> tys root h
type_lift = type_liftN (Proxy::Proxy (Peano_of_Type ty tys))

-- ** Type 'Type_Unlift'
-- | Apply 'Peano_of_Type' on 'Type_UnliftN'.
type Type_Unlift ty tys
 =   Type_UnliftN (Peano_of_Type ty tys) ty tys

-- *** Class 'Type_UnliftN'
-- | Try to unlift a given type out of a given type stack including it,
-- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
class Type_UnliftN (p:: *) ty tys where
	type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
instance Type_UnliftN Zero curr curr where
	type_unliftN _ = Just
instance Type_UnliftN Zero curr (Type_Alt curr next) where
	type_unliftN _ (Type_Alt_Curr x) = Just x
	type_unliftN _ (Type_Alt_Next _) = Nothing
instance
 Type_UnliftN p other next =>
 Type_UnliftN (Succ p) other (Type_Alt curr next) where
	type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
	type_unliftN _ (Type_Alt_Curr _) = Nothing

-- | Convenient wrapper around 'type_unliftN',
-- passing it the 'Peano' number from 'Peano_of_Type'.
type_unlift
 :: forall ty tys (root:: * -> *) h.
 Type_Unlift ty tys =>
 tys root h -> Maybe (ty root h)
type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))

-- * Type 'Type_Type1'
data Type_Type1 f (root:: * -> *) h where
	Type_Type1 :: Proxy f -> root a -> Type_Type1 f root (f a)
type instance Root_of_Type      (Type_Type1 f root) = root
type instance Error_of_Type ast (Type_Type1 f root) = No_Error_Type

instance -- Eq_Type
 Eq_Type root =>
 Eq_Type (Type_Type1 f root) where
	eq_type (Type_Type1 _f1 a1) (Type_Type1 _f2 a2)
	 | Just Refl <- a1 `eq_type` a2
	 = Just Refl
	eq_type _ _ = Nothing
instance -- Eq
 Eq_Type root =>
 Eq (Type_Type1 f root h) where
	x == y = isJust $ eq_type x y
instance -- Show
 String_from_Type (Type_Type1 f root) =>
 Show (Type_Type1 f root h) where
	show = string_from_type

-- * Type 'Type1_f'
type Type1_f tys
 =   Type1_fN (Peano_of_Type1 tys) tys

-- ** Type 'Type1_fN'
type family   Type1_fN (p:: *) (tys:: (* -> *) -> * -> *) :: * -> *
type instance Type1_fN Zero     (Type_Type1 f)                 = f
type instance Type1_fN Zero     (Type_Alt (Type_Type1 f) next) = f
type instance Type1_fN (Succ p) (Type_Alt curr next)           = Type1_fN p next

-- ** Type 'Peano_of_Type1'
type family Peano_of_Type1
 (tys:: (* -> *) -> * -> *) :: * where
	Peano_of_Type1 (Type_Type1 f)                 = Zero
	Peano_of_Type1 (Type_Alt (Type_Type1 f) next) = Zero
	Peano_of_Type1 (Type_Alt curr next)           = Succ (Peano_of_Type1 next)

-- ** Type 'Type_Unlift1'
-- | Apply 'Peano_of_Type1' on 'Type_Unlift1N'.
type Type_Unlift1 tys
 =   Type_Unlift1N (Peano_of_Type1 tys) tys

-- *** Class 'Type_Unlift1N'
-- | Try to unlift1 a given type out of a given type stack including it,
-- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
class Type_Unlift1N (p:: *) tys where
	type_unlift1N
	 :: forall (root:: * -> *) h
	 .  Proxy p
	 -> tys root h
	 -> Maybe ( Type_Type1 (Type1_fN p tys) root h
	          , Type_Lift1 (Type1_fN p tys) tys )
data Type_Lift1 f tys
 =   Type_Lift1 ( forall (root:: * -> *) h
                . Type_Type1 f root h -> tys root h
                )
instance Type_Unlift1N Zero (Type_Type1 f) where
	type_unlift1N _ ty = Just (ty, Type_Lift1 id)
instance Type_Unlift1N Zero (Type_Alt (Type_Type1 f) next) where
	type_unlift1N _ (Type_Alt_Curr x) = Just (x, Type_Lift1 Type_Alt_Curr)
	type_unlift1N _ (Type_Alt_Next _) = Nothing
instance
 Type_Unlift1N p next =>
 Type_Unlift1N (Succ p) (Type_Alt curr next) where
	type_unlift1N _ (Type_Alt_Next x) =
		((\(Type_Lift1 cons) -> Type_Lift1 $ Type_Alt_Next . cons) <$>) <$>
		type_unlift1N (Proxy::Proxy p) x
	type_unlift1N _ (Type_Alt_Curr _) = Nothing

-- | Convenient wrapper around 'type_unlift1N',
-- passing it the 'Peano' number from 'Peano_of_Type1'.
type_unlift1
 :: forall tys (root:: * -> *) h
 .  Type_Unlift1 tys
 => tys root h
 -> Maybe ( Type_Type1 (Type1_fN (Peano_of_Type1 tys) tys) root h
          , Type_Lift1 (Type1_fN (Peano_of_Type1 tys) tys) tys )
type_unlift1 = type_unlift1N (Proxy::Proxy (Peano_of_Type1 tys))

-- ** Type family 'Is_Last_Type'
-- | Return whether a given type is the last one in a given type stack.
--
-- NOTE: each type parser uses this type family
-- when it encounters unsupported syntax:
-- to know if it is the last type parser component that will be tried
-- (and thus return 'Error_Type_Unsupported')
-- or if some other type parser component shall be tried
-- (and thus return 'Error_Type_Unsupported_here',
-- which is then handled accordingly by the 'Type_from' instance of 'Type_Alt').
type family Is_Last_Type (ty:: * -> *) (tys:: * -> *) :: Bool where
	Is_Last_Type ty ty                               = 'True
	Is_Last_Type ty        (Type_Root tys)           = Is_Last_Type ty (tys (Type_Root tys))
	Is_Last_Type (ty root) (Type_Alt ty   next root) = 'False
	Is_Last_Type other     (Type_Alt curr next root) = Is_Last_Type other (next root)

-- * Type 'Error_Type_Alt'
-- | Error type making an alternative between two error types.
data Error_Type_Alt curr next
 =   Error_Type_Alt_Curr curr
 |   Error_Type_Alt_Next next
 deriving (Eq, Show)

-- ** Type 'Error_Type_Lift'
type Error_Type_Lift err errs
 =   Error_Type_LiftN (Peano_of_Error_Type err errs) err errs

-- *** Type 'Peano_of_Error_Type'
-- | Return a 'Peano' number derived from the location
-- of a given error type within a given error type stack.
type family Peano_of_Error_Type (err:: *) (errs:: *) :: * where
	Peano_of_Error_Type err   err                        = Zero
	Peano_of_Error_Type err   (Error_Type_Alt err  next) = Zero
	Peano_of_Error_Type other (Error_Type_Alt curr next) = Succ (Peano_of_Error_Type other next)

-- *** Class 'Error_Type_LiftN'
-- | Lift a given error type to the top of a given error type stack including it,
-- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
class Error_Type_LiftN (p:: *) err errs where
	error_type_liftN :: Proxy p -> err -> errs
instance Error_Type_LiftN Zero curr curr where
	error_type_liftN _ = id
instance Error_Type_LiftN Zero curr (Error_Type_Alt curr next) where
	error_type_liftN _ = Error_Type_Alt_Curr
instance
 Error_Type_LiftN p other next =>
 Error_Type_LiftN (Succ p) other (Error_Type_Alt curr next) where
	error_type_liftN _ = Error_Type_Alt_Next . error_type_liftN (Proxy::Proxy p)

-- | Convenient wrapper around 'error_type_unliftN',
-- passing it the 'Peano' number from 'Peano_of_Error_Type'.
error_type_lift
 :: forall err errs.
 Error_Type_Lift err errs =>
 err -> errs
error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))

-- ** Type 'Error_Type_Unlift'
-- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
type Error_Type_Unlift ty tys
 =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys

-- | Convenient wrapper around 'error_type_unliftN',
-- passing it the 'Peano' number from 'Peano_of_Error_Type'.
error_type_unlift
 :: forall ty tys.
 Error_Type_Unlift ty tys =>
 tys -> Maybe ty
error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))

-- *** Class 'Error_Type_UnliftN'
-- | Try to unlift a given type error out of a given type error stack including it,
-- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
class Error_Type_UnliftN (p:: *) ty tys where
	error_type_unliftN :: Proxy p -> tys -> Maybe ty
instance Error_Type_UnliftN Zero curr curr where
	error_type_unliftN _ = Just
instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
	error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
	error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
instance
 Error_Type_UnliftN p other next =>
 Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
	error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
	error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing

-- ** Type 'Error_Type_Read'
-- | Common type errors.
data Error_Type ast
 =   Error_Type_Unsupported ast
 -- ^ Given syntax is supported by none
 -- of the type parser components
 -- of the type stack.
 |   Error_Type_Unsupported_here ast
 -- ^ Given syntax not supported by the current type parser component.
 |   Error_Type_Wrong_number_of_arguments ast Int
 deriving (Eq, Show)

-- | Convenient wrapper around 'error_type_lift',
-- passing the type family boilerplate.
error_type
 :: Error_Type_Lift (Error_Type ast)
                    (Error_of_Type ast (Root_of_Type ty))
 => Proxy ty
 -> Error_Type ast
 -> Error_of_Type ast (Root_of_Type ty)
error_type _ = error_type_lift

error_type_unsupported
 :: forall ast ty.
 ( Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
 , Error_Type_Lift (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 ) => Proxy ty -> ast
 -> Error_of_Type ast (Root_of_Type ty)
error_type_unsupported ty ast =
	case hbool :: HBool (Is_Last_Type ty (Root_of_Type ty)) of
	 HTrue  -> error_type ty $ Error_Type_Unsupported ast
	 HFalse -> error_type ty $ Error_Type_Unsupported_here ast

-- * Class 'String_from_Type'
-- | Return a 'String' from a type.
class String_from_Type ty where
	string_from_type :: ty h -> String

-- * Type 'Exists_Type'
-- | Existential data type wrapping the index of a type.
data Exists_Type ty
 = forall h. Exists_Type (ty h)
instance -- Eq
 Eq_Type ty =>
 Eq (Exists_Type ty) where
	Exists_Type xh == Exists_Type yh =
		isJust $ xh `eq_type` yh
instance -- Show
 String_from_Type ty =>
 Show (Exists_Type ty) where
	show (Exists_Type ty) = string_from_type ty

-- * Type 'Exists_Type1'
-- | Existential data type wrapping the index of a type1.
data Exists_Type1 ty
 = forall h. Exists_Type1 (ty h -> ty h)

-- * Type 'Exists_Type_and_Repr'
data Exists_Type_and_Repr ty repr
 =   forall h.
     Exists_Type_and_Repr (ty h) (repr h)

-- * Type family 'HBool'
-- | Host-type equality.
type family HEq x y :: Bool where
	HEq x x = 'True
	HEq x y = 'False
-- ** Type 'HBool'
-- | Boolean singleton.
data HBool b where
	HTrue  :: HBool 'True
	HFalse :: HBool 'False
-- ** Class 'Implicit_HBool'
-- | Construct a host-term boolean singleton from a host-type boolean.
class    Implicit_HBool b      where hbool :: HBool b
instance Implicit_HBool 'True  where hbool = HTrue
instance Implicit_HBool 'False where hbool = HFalse