{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-missing-methods #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Type variable.
module Language.Symantic.Type.Var
 ( module Language.Symantic.Type.Var
 , module Language.Symantic.Lib.Data.Peano
 ) where

import qualified Data.MonoTraversable as MT
import Data.Type.Equality ((:~:)(Refl))

import Language.Symantic.Lib.Data.Peano
import Language.Symantic.Type.Root
import Language.Symantic.Type.Type0
import Language.Symantic.Type.Type1
import Language.Symantic.Type.Constraint
import Language.Symantic.Type.Family

-- * Type 'Var0'
newtype Var0 = Var0 EPeano
type instance Host0_of EPeano = Var0

-- | Undefined instance required to build errors.
instance Eq Var0
-- | Undefined instance required to build errors.
instance Ord Var0
-- | Undefined instance required to build errors.
instance Monoid Var0

-- * Type 'Var1'
newtype Var1 a = Var1 EPeano
type instance Host1_of EPeano = Var1

-- * Type 'Type_Var0'
-- | The variable type of kind @*@.
type Type_Var0 = Type0 EPeano

pattern Type_Var0 :: SPeano p -> Type_Var0 root Var0
pattern Type_Var0 p = Type0 (EPeano p)

instance Type1_Eq (Type_Var0 root) where
instance Type0_Constraint Eq             (Type_Var0 root)
instance Type0_Constraint Monoid         (Type_Var0 root)
instance Type0_Constraint Ord            (Type_Var0 root)
instance Type0_Constraint Num            (Type_Var0 root)
instance Type0_Constraint Integral       (Type_Var0 root)
instance Type0_Constraint MT.MonoFunctor (Type_Var0 root)
instance Type0_Family Type_Family_MonoElement (Type_Var0 root)
instance String_from_Type (Type_Var0 root) where
	string_from_type (Type0 (EPeano p)) =
		"t" ++ show (integral_from_peano p::Integer)

-- | Inject 'Type_Var0' within a root type.
type_var0 :: Type_Root_Lift Type_Var0 root => SPeano p -> root Var0
type_var0 = type_root_lift . Type0 . EPeano

-- * Type 'Type_Var1'
-- | The variable type of kind @* -> *@.
type Type_Var1 = Type1 EPeano

pattern Type_Var1 :: SPeano p -> root a -> Type_Var1 root (Var1 a)
pattern Type_Var1 p a = Type1 (EPeano p) a

instance Type0_Constraint Eq             (Type_Var1 root)
instance Type0_Constraint Ord            (Type_Var1 root)
instance Type0_Constraint Monoid         (Type_Var1 root)
instance Type0_Constraint Num            (Type_Var1 root)
instance Type0_Constraint Integral       (Type_Var1 root)
instance Type0_Constraint MT.MonoFunctor (Type_Var1 root)
instance Type1_Constraint Applicative    (Type_Var1 root)
instance Type1_Constraint Foldable       (Type_Var1 root)
instance Type1_Constraint Functor        (Type_Var1 root)
instance Type1_Constraint Monad          (Type_Var1 root)
instance Type1_Constraint Traversable    (Type_Var1 root)
instance Type0_Family Type_Family_MonoElement (Type_Var1 root)
instance Type1_Eq (Type_Var1 root) where
	type1_eq (Type1 p1 _) (Type1 p2 _) | p1 == p2 = Just Refl
	type1_eq _ _ = Nothing
instance -- String_from_Type
 String_from_Type root =>
 String_from_Type (Type_Var1 root) where
	string_from_type (Type1 (EPeano p) a) =
		"t_" ++ show (integral_from_peano p::Integer) ++
		" " ++ string_from_type a

-- | Inject 'Type_Var1' within a root type.
type_var1 :: Type_Root_Lift Type_Var1 root => SPeano p -> root a -> root (Var1 a)
type_var1 p = type_root_lift . Type_Var1 p