{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Type.Type0 where

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

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

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

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

instance -- Type0_Eq
 Type0_Eq (Type0 (Proxy h0) root) where
	type0_eq Type0{} Type0{} = Just Refl
instance -- Type0_Eq
 Type0_Eq (Type0 EPeano root) where
	type0_eq (Type0 p1) (Type0 p2) | p1 == p2 = Just Refl
	type0_eq _ _ = Nothing
instance -- Eq
 Type0_Eq (Type0 px root) =>
 Eq (Type0 px root h) where
	x == y = isJust $ x `type0_eq` y
instance -- Show
 String_from_Type (Type0 (Proxy h0) root) =>
 Show (Type0 (Proxy h0) root h0) where
	show = string_from_type

-- | Inject a 'Type0' within a root type.
type0 :: Type_Root_Lift (Type0 (Proxy h0)) root => root h0
type0 = type_root_lift (Type0 (Proxy::Proxy h0))

-- ** Type family 'Host0_of'
type family Host0_of px :: *
type instance Host0_of (Proxy h0) = h0

-- ** Type 'Type0_Lift'
-- | Apply 'Peano_of_Type' on 'Type0_LiftP'.
type Type0_Lift ty tys
 =   Type0_LiftP (Peano_of_Type ty tys) ty tys
instance
 Type0_Lift ty root =>
 Type_Root_Lift ty (Type_Root root) where
	type_root_lift = Type_Root . type0_lift

-- *** 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 'Type0_LiftP'
-- | 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 Type0_LiftP (p:: *) ty tys where
	type0_liftP :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
instance Type0_LiftP Zero curr curr where
	type0_liftP _ = id
instance Type0_LiftP Zero curr (Type_Alt curr next) where
	type0_liftP _ = Type_Alt_Curr
instance
 Type0_LiftP p other next =>
 Type0_LiftP (Succ p) other (Type_Alt curr next) where
	type0_liftP _ = Type_Alt_Next . type0_liftP (Proxy::Proxy p)

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

-- ** Type 'Type0_Unlift'
-- | Apply 'Peano_of_Type' on 'Type0_UnliftP'.
type Type0_Unlift ty tys
 =   Type0_UnliftP (Peano_of_Type ty tys) ty tys

-- *** Class 'Type0_UnliftP'
-- | 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 Type0_UnliftP (p:: *) ty tys where
	type0_unliftP :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
instance Type0_UnliftP Zero curr curr where
	type0_unliftP _ = Just
instance Type0_UnliftP Zero curr (Type_Alt curr next) where
	type0_unliftP _ (Type_Alt_Curr x) = Just x
	type0_unliftP _ (Type_Alt_Next _) = Nothing
instance
 Type0_UnliftP p other next =>
 Type0_UnliftP (Succ p) other (Type_Alt curr next) where
	type0_unliftP _ (Type_Alt_Next x) = type0_unliftP (Proxy::Proxy p) x
	type0_unliftP _ (Type_Alt_Curr _) = Nothing

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

-- * Class 'Type0_Eq'
-- | Test two types for equality,
-- returning an Haskell type-level proof
-- of the equality when it holds.
class Type0_Eq (ty:: * -> *) where
	type0_eq :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
instance -- Type_Root
 Type0_Eq (ty (Type_Root ty)) =>
 Type0_Eq (Type_Root ty) where
	type0_eq (Type_Root x) (Type_Root y) = x `type0_eq` y
instance -- Eq Type_Root
 Type0_Eq (Type_Root ty) =>
 Eq (Type_Root ty h) where
	x == y = isJust $ x `type0_eq` y
instance -- Type_Alt
 ( Type0_Eq (curr root)
 , Type0_Eq (next root)
 ) => Type0_Eq (Type_Alt curr next root) where
	type0_eq (Type_Alt_Curr x) (Type_Alt_Curr y) = x `type0_eq` y
	type0_eq (Type_Alt_Next x) (Type_Alt_Next y) = x `type0_eq` y
	type0_eq _ _ = Nothing
instance -- Eq Type_Alt
 ( Type0_Eq (curr root)
 , Type0_Eq (next root)
 ) => Eq (Type_Alt curr next root h) where
	x == y = isJust $ x `type0_eq` y

-- * Class 'Type0_From'
-- | Parse given @ast@ into a 'Root_of_Type',
-- or return an 'Error_of_Type'.
--
-- NOTE: making a distinction between @ty@ and 'Root_of_Type'@ ty@,
-- instead of having only a @root@ variable
-- is what enables to define many instances, one per type.
class Type0_From ast (ty:: * -> *) where
	type0_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
instance -- Type_Root
 ( Type0_Eq (Type_Root ty)
 , Type0_From ast (ty (Type_Root ty))
 , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 ) => Type0_From ast (Type_Root ty) where
	type0_from _ty = type0_from (Proxy::Proxy (ty (Type_Root ty)))
instance -- Type_Alt
 ( Type0_Eq (curr root)
 , Type0_From ast (curr root)
 , Type0_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)
 ) => Type0_From ast (Type_Alt curr next root) where
	type0_from _ty ast k =
		case type0_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)) ->
				type0_from (Proxy::Proxy (next root)) ast k
			 _ -> Left err

-- * Class 'String_from_Type'
-- | Return a 'String' from a type.
class String_from_Type ty where
	string_from_type :: ty h -> String
instance -- Type_Root
 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 Type_Root
 String_from_Type (Type_Root ty) =>
 Show (Type_Root ty h) where
	show = string_from_type
instance -- Type_Alt
 ( 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 'Exists_Type0'
-- | Existential data type wrapping the index of a 'Type0'.
data Exists_Type0 ty
 = forall h. Exists_Type0 (ty h)
instance -- Eq
 Type0_Eq ty =>
 Eq (Exists_Type0 ty) where
	Exists_Type0 xh == Exists_Type0 yh =
		isJust $ xh `type0_eq` yh
instance -- Show
 String_from_Type ty =>
 Show (Exists_Type0 ty) where
	show (Exists_Type0 ty) = string_from_type ty

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