{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Type.Type1 where

import Data.Maybe (isJust, fromMaybe)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))

import Language.Symantic.Lib.Data.Peano
import Language.Symantic.Lib.Data.Bool
import Language.Symantic.Type.Root
import Language.Symantic.Type.Alt
import Language.Symantic.Type.Error
import Language.Symantic.Type.Type0

-- * Type 'Type1'
-- | A type of kind @(* -> *)@.
data Type1 px (root:: * -> *) h where
	Type1 :: px -> root a -> Type1 px root ((Host1_of px) a)

type instance Root_of_Type      (Type1 px root) = root
type instance Error_of_Type ast (Type1 px root) = No_Error_Type

instance -- Type0_Eq
 Type0_Eq root =>
 Type0_Eq (Type1 (Proxy h1) root) where
	type0_eq (Type1 _px1 a1) (Type1 _px2 a2)
	 | Just Refl <- a1 `type0_eq` a2
	 = Just Refl
	type0_eq _ _ = Nothing
instance -- Type0_Eq
 Type0_Eq root =>
 Type0_Eq (Type1 EPeano root) where
	type0_eq (Type1 p1 a1)
	        (Type1 p2 a2)
	 | p1 == p2
	 , Just Refl <- a1 `type0_eq` a2
	 = Just Refl
	type0_eq _ _ = Nothing
instance -- Eq
 Type0_Eq root =>
 Eq (Type1 (Proxy h1) root h) where
	x == y = isJust $ type0_eq x y
instance -- Eq
 Type0_Eq root =>
 Eq (Type1 EPeano root h) where
	x == y = isJust $ type0_eq x y
instance -- Type1_Eq
 Type1_Eq (Type1 (Proxy t1) root) where
	type1_eq Type1{} Type1{} = Just Refl
instance -- Show
 String_from_Type (Type1 px root) =>
 Show (Type1 px root h) where
	show = string_from_type

-- | Inject a 'Type1' within a root type.
type1
 :: forall root h1 a.
 Type_Root_Lift (Type1 (Proxy h1)) root
 => root a -> root (h1 a)
type1 = type_root_lift . Type1 (Proxy::Proxy h1)

-- ** Type family 'Host1_of'
type family Host1_of px :: * -> *
type instance Host1_of (Proxy h1) = h1

-- * Class 'Type1_Eq'
-- | Test two type constructors for equality,
-- returning an Haskell type-level proof
-- of the equality when it holds.
class Type1_Eq (ty:: * -> *) where
	type1_eq :: forall h1 h2 a1 a2. ty (h1 a1) -> ty (h2 a2) -> Maybe (h1 :~: h2)
	type1_eq = error "type1_eq"
instance -- Type_Root
 Type1_Eq (ty (Type_Root ty)) =>
 Type1_Eq (Type_Root ty) where
	type1_eq (Type_Root x) (Type_Root y) = x `type1_eq` y
instance -- Type_Alt
 ( Type1_Eq (curr root)
 , Type1_Eq (next root)
 ) => Type1_Eq (Type_Alt curr next root) where
	type1_eq (Type_Alt_Curr x) (Type_Alt_Curr y) = x `type1_eq` y
	type1_eq (Type_Alt_Next x) (Type_Alt_Next y) = x `type1_eq` y
	type1_eq _ _ = Nothing
instance -- Type0 (Proxy h0)
 Type1_Eq (Type0 (Proxy h0) root)

-- * Class 'Type1_From'
-- | Parse given @ast@ into a 'Root_of_Type' constructor,
-- or return an 'Error_of_Type'.
class Type1_From ast (ty:: * -> *) where
	type1_from
	 :: Proxy ty
	 -> ast
	 -> (forall (h1:: * -> *). Proxy h1
	            -> (forall h. Root_of_Type ty h -> Root_of_Type ty (h1 h))
	            -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
	 ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
	default type1_from ::
	 ( Error_Type_Lift (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
	 , IBool (Is_Last_Type ty (Root_of_Type ty))
	 ) => Proxy ty
	 -> ast
	 -> (forall (h1:: * -> *). Proxy h1
	            -> (forall h. Root_of_Type ty h -> Root_of_Type ty (h1 h))
	            -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
	 ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
	type1_from ty ast _k =
		Left $ error_type_unsupported ty ast
instance -- Type_Root
 ( Type0_Eq (Type_Root ty)
 , Type1_From ast (ty (Type_Root ty))
 , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 ) => Type1_From ast (Type_Root ty) where
	type1_from _ty = type1_from (Proxy::Proxy (ty (Type_Root ty)))

instance -- Type_Alt
 ( Type0_Eq (curr root)
 , Type1_From ast (curr root)
 , Type1_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)
 ) => Type1_From ast (Type_Alt curr next root) where
	type1_from _ty ast k =
		case type1_from (Proxy::Proxy (curr root)) ast (\f ty -> Right $ k f ty) of
		 Right ret -> ret
		 Left err ->
			case error_type_unlift err of
			 Just (Error_Type_Unsupported_here (_::ast)) ->
				type1_from (Proxy::Proxy (next root)) ast k
			 _ -> Left err

-- ** Type 'Type1_Lift'
data Type1_Lift px root tys
 =   Type1_Lift (forall h. Type1 px root h -> tys root h)

-- ** Type 'Type1_Unlift'
class Type1_Unlift ty where
	type1_unlift
	 :: forall (root:: * -> *) ret h.
	 ty root h
	 -> (forall (px:: *).
	     ( Type1 px root h
	     , Type1_Lift px root ty
	     ) -> Maybe ret)
	 -> Maybe ret
instance Type1_Unlift (Type0 px) where
	type1_unlift _ty _k = Nothing
instance Type1_Unlift (Type1 px) where
	type1_unlift ty k = k (ty, Type1_Lift id)
instance -- Type_Alt
 ( Type1_Unlift curr
 , Type1_Unlift next
 ) => Type1_Unlift (Type_Alt curr next) where
	type1_unlift (Type_Alt_Curr ty) k =
		fromMaybe Nothing $ type1_unlift ty $ \(t, Type1_Lift l) ->
			Just $ k (t, Type1_Lift $ Type_Alt_Curr . l)
	type1_unlift (Type_Alt_Next ty) k =
		fromMaybe Nothing $ type1_unlift ty $ \(t, Type1_Lift l) ->
			Just $ k (t, Type1_Lift $ Type_Alt_Next . l)

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