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

import Data.Maybe (isJust)
import Data.Peano
import Data.Proxy
import Data.Type.Equality ((:~:))

-- * Class 'Type_Eq'

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

-- * Class 'Type_from'
-- | Parse some @raw@ data into a 'Root_of_Type',
-- or return 'Nothing' if the @raw@ value is not supported
-- or an 'Error_Type' if it is not well-formed.
class Type_Eq ty =>
      Type_from raw (ty:: * -> *) where
	type_from
	 :: Proxy ty
	 -> raw
	 -> (forall h. Root_of_Type ty h
	            -> Either (Maybe (Error_of_Type raw (Root_of_Type ty))) ret)
	 ->            Either (Maybe (Error_of_Type raw (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 (raw:: *) (ty:: * -> *) :: *

-- * 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 raw (Type_Root ty)
 =            Error_of_Type raw (ty (Type_Root ty))
 -- NOTE: require UndecidableInstances.
instance -- Type_Eq
 Type_Eq (ty (Type_Root ty)) =>
 Type_Eq (Type_Root ty) where
	type_eq (Type_Root x) (Type_Root y) = x `type_eq` y
instance -- Eq
 Type_Eq (Type_Root ty) =>
 Eq (Type_Root ty h) where
	x == y = isJust $ type_eq x y
instance -- Type_from
 ( Type_Eq (Type_Root ty)
 , Type_from raw (ty (Type_Root ty))
 , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 ) => Type_from raw (Type_Root ty) where
	type_from _px_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_Cons'
-- | Combine two types into one.
data Type_Cons curr next (root:: * -> *) h
 =   Type_Curr (curr root h)
 |   Type_Next (next root h)
type instance Root_of_Type (Type_Cons curr next root) = root
type instance Error_of_Type raw (Type_Cons curr next root)
 = Error_Type_Cons (Error_of_Type raw (curr root))
                   (Error_of_Type raw (next root))
instance -- Type_Eq
 ( Type_Eq (curr root)
 , Type_Eq (next root)
 ) => Type_Eq (Type_Cons curr next root) where
	type_eq (Type_Curr x) (Type_Curr y) = x `type_eq` y
	type_eq (Type_Next x) (Type_Next y) = x `type_eq` y
	type_eq _ _ = Nothing
instance -- Eq
 ( Type_Eq (curr root)
 , Type_Eq (next root)
 ) => Eq (Type_Cons curr next root h) where
	x == y = isJust $ type_eq x y
instance -- Type_from
 ( Type_Eq (curr root)
 , Type_from raw (curr root)
 , Type_from raw (next root)
 , Root_of_Type (curr root) ~ root
 , Root_of_Type (next root) ~ root
 ) => Type_from raw (Type_Cons curr next root) where
	type_from _px_ty raw k =
		case type_from (Proxy::Proxy (curr root)) raw (Right . k) of
		 Right ret -> ret
		 Left Nothing -> type_from (Proxy::Proxy (next root)) raw k
		 Left err -> Left err
instance -- String_from_Type
 ( String_from_Type (curr root)
 , String_from_Type (next root)
 ) => String_from_Type (Type_Cons curr next root) where
	string_from_type (Type_Curr t) = string_from_type t
	string_from_type (Type_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.
type family Peano_of_Type
 (ty::  (* -> *) -> * -> *)
 (tys:: (* -> *) -> * -> *) :: Peano where
	Peano_of_Type ty ty                       = 'Zero
	Peano_of_Type ty (Type_Cons ty next)      = 'Zero
	Peano_of_Type other (Type_Cons curr next) = 'Succ (Peano_of_Type other next)

-- *** Class 'Type_LiftN'
-- | Construct the sequence of 'Type_Curr' and 'Type_Next'
-- lifting a given type to the top of a given type stack.
class Type_LiftN (n::Peano) ty tys where
	type_liftN :: forall (root:: * -> *) h. Proxy n -> ty root h -> tys root h
instance Type_LiftN 'Zero curr curr where
	type_liftN _ = id
instance Type_LiftN 'Zero curr (Type_Cons curr next) where
	type_liftN _ = Type_Curr
instance
 Type_LiftN n other next =>
 Type_LiftN ('Succ n) other (Type_Cons curr next) where
	type_liftN _ = Type_Next . type_liftN (Proxy::Proxy n)

-- | Lift a type within a type stack to its top,
-- using a 'Peano' number calculated by 'Peano_of_Type'
-- to avoid the overlapping of the 'Type_LiftN' instances.
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'
-- | Deconstruct a sequence of 'Type_Curr' and 'Type_Next'
-- trying to unlift a given extension out of a given extension stack.
class Type_UnliftN (n::Peano) ty tys where
	type_unliftN :: forall (root:: * -> *) h. Proxy n -> tys root h -> Maybe (ty root h)
instance Type_UnliftN 'Zero curr curr where
	type_unliftN _ = Just
instance Type_UnliftN 'Zero curr (Type_Cons curr next) where
	type_unliftN _ (Type_Curr x) = Just x
	type_unliftN _ (Type_Next _) = Nothing
instance
 Type_UnliftN n other next =>
 Type_UnliftN ('Succ n) other (Type_Cons curr next) where
	type_unliftN _ (Type_Next x) = type_unliftN (Proxy::Proxy n) x
	type_unliftN _ (Type_Curr _) = Nothing

-- | Unlift an extension within an extension stack,
-- using a 'Peano' number calculated by 'Peano_of_Type'
-- to avoid the overlapping of the 'Type_UnliftN' instances.
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 'Error_Type_Cons'
-- | Combine two error types into one.
data Error_Type_Cons curr next
 =   Error_Type_Curr curr
 |   Error_Type_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:: *) :: Peano where
	Peano_of_Error_Type err err                           = 'Zero
	Peano_of_Error_Type err (Error_Type_Cons err next)    = 'Zero
	Peano_of_Error_Type other (Error_Type_Cons curr next) = 'Succ (Peano_of_Error_Type other next)

-- *** Class 'Error_Type_LiftN'
-- | Construct the sequence of 'Error_Type_Curr' and 'Error_Type_Next'
-- lifting a given error type to the top of a given error type stack.
class Error_Type_LiftN (n::Peano) err errs where
	error_type_liftN :: Proxy n -> err -> errs
instance Error_Type_LiftN 'Zero curr curr where
	error_type_liftN _ = id
instance Error_Type_LiftN 'Zero curr (Error_Type_Cons curr next) where
	error_type_liftN _ = Error_Type_Curr
instance
 Error_Type_LiftN n other next =>
 Error_Type_LiftN ('Succ n) other (Error_Type_Cons curr next) where
	error_type_liftN _ = Error_Type_Next . error_type_liftN (Proxy::Proxy n)

-- | Lift an error type within a type stack to its top,
-- using a 'Peano' number calculated by 'Peano_of_Error_Type'
-- to avoid the overlapping of the 'Error_Type_LiftN' instances.
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))

-- * 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 to wrap an indexed type.
data Exists_Type ty
 = forall h. Exists_Type (ty h)
instance -- Eq
 Type_Eq ty =>
 Eq (Exists_Type ty) where
	Exists_Type xh == Exists_Type yh =
		isJust $ type_eq xh yh
instance -- Show
 String_from_Type ty =>
 Show (Exists_Type ty) where
	show (Exists_Type ty) = string_from_type ty

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