{-# 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 GHC.Prim (Constraint)

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 'Type_Type1'
-- | A type of kind @(k -> *)@.
data Type_Type1 px (root:: * -> *) h where
	Type_Type1 :: px -> root a -> Type_Type1 px root ((Host1_of px) a)

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

instance -- Eq_Type
 Eq_Type root =>
 Eq_Type (Type_Type1 (Proxy h1) root) where
	eq_type (Type_Type1 _px1 a1) (Type_Type1 _px2 a2)
	 | Just Refl <- a1 `eq_type` a2
	 = Just Refl
	eq_type _ _ = Nothing
instance -- Eq_Type
 Eq_Type root =>
 Eq_Type (Type_Type1 EPeano root) where
	eq_type (Type_Type1 p1 a1)
	        (Type_Type1 p2 a2)
	 | p1 == p2
	 , Just Refl <- a1 `eq_type` a2
	 = Just Refl
	eq_type _ _ = Nothing
instance -- Eq
 Eq_Type root =>
 Eq (Type_Type1 (Proxy h1) root h) where
	x == y = isJust $ eq_type x y
instance -- Eq
 Eq_Type root =>
 Eq (Type_Type1 EPeano root h) where
	x == y = isJust $ eq_type x y
instance -- Eq_Type1
 Eq_Type1 (Type_Type1 (Proxy t1) root) where
	eq_type1 Type_Type1{} Type_Type1{}
	 = Just Refl
instance -- Show
 String_from_Type (Type_Type1 px root) =>
 Show (Type_Type1 px root h) where
	show = string_from_type

-- | Inject a 'Type_Type1' within a root type.
type_type1
 :: forall root h1 a.
 Lift_Type_Root (Type_Type1 (Proxy h1)) root
 => root a -> root (h1 a)
type_type1 = lift_type_root . Type_Type1 (Proxy::Proxy h1)

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

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

-- * Class 'Constraint_Type1'
-- | Test if a type constructor satisfies a given 'Constraint',
-- returning an Haskell type-level proof
-- of that satisfaction when it holds.
class Constraint_Type1 (c:: (* -> *) -> Constraint) (ty:: * -> *) where
	constraint_type1 :: forall h1 h. Proxy c -> ty (h1 h) -> Maybe (Dict (c h1))
	constraint_type1 _c _ = Nothing
instance -- Type_Root
 Constraint_Type1 c (ty (Type_Root ty)) =>
 Constraint_Type1 c (Type_Root ty) where
	constraint_type1 c (Type_Root ty) = constraint_type1 c ty
instance -- Type_Alt
 ( Constraint_Type1 c (curr root)
 , Constraint_Type1 c (next root)
 ) => Constraint_Type1 c (Type_Alt curr next root) where
	constraint_type1 c (Type_Alt_Curr ty) = constraint_type1 c ty
	constraint_type1 c (Type_Alt_Next ty) = constraint_type1 c ty
instance Constraint_Type1 c (Type_Type0 px 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 ::
	 ( Lift_Error_Type (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
 ( Eq_Type (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
 ( Eq_Type (curr root)
 , Type1_from ast (curr root)
 , Type1_from ast (next root)
 , Root_of_Type (curr root) ~ root
 , Root_of_Type (next root) ~ root
 , Unlift_Error_Type (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 unlift_error_type err of
			 Just (Error_Type_Unsupported_here (_::ast)) ->
				type1_from (Proxy::Proxy (next root)) ast k
			 _ -> Left err

-- ** Type 'Lift_Type1'
data Lift_Type1 px root tys
 =   Lift_Type1 ( forall {-(root:: * -> *)-} h
                . Type_Type1 px root h -> tys root h
                )

-- ** Type 'Unlift_Type1'
class Unlift_Type1 ty where
	unlift_type1
	 :: forall (root:: * -> *) ret h.
	 ty root h
	 -> (forall (px:: *).
	     ( Type_Type1 px root h
	     , Lift_Type1 px root ty
	     ) -> Maybe ret)
	 -> Maybe ret
	unlift_type1 _ty _k = Nothing
instance Unlift_Type1 (Type_Type1 px) where
	unlift_type1 ty k = k (ty, Lift_Type1 id)
instance -- Type_Alt
 ( Unlift_Type1 curr
 , Unlift_Type1 next
 ) => Unlift_Type1 (Type_Alt curr next) where
	unlift_type1 (Type_Alt_Curr ty) k =
		fromMaybe Nothing $ unlift_type1 ty $ \(t, Lift_Type1 l) ->
			Just $ k (t, Lift_Type1 $ Type_Alt_Curr . l)
	unlift_type1 (Type_Alt_Next ty) k =
		fromMaybe Nothing $ unlift_type1 ty $ \(t, Lift_Type1 l) ->
			Just $ k (t, Lift_Type1 $ Type_Alt_Next . l)
instance -- Type_Type0 px
 Unlift_Type1 (Type_Type0 px)

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