{-# 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 Data.Type.Equality ((:~:)(Refl))
import Language.Symantic.Type.Common
import Language.Symantic.Lib.Data.Peano

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

-- | Undefined instance required to build errors.
instance Eq Var0
-- | Undefined instance required to build errors.
instance Ord 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 = Type_Type0 EPeano

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

instance Eq_Type1 (Type_Var0 root) where
instance -- String_from_Type
 String_from_Type (Type_Var0 root) where
	string_from_type (Type_Type0 (EPeano p)) =
		"t" ++ show (integral_from_peano p::Integer)
instance Constraint_Type Eq (Type_Var0 root) where
	constraint_type _c Type_Type0{} = Just Dict

-- | Inject 'Type_Var0' within a root type.
type_var0 :: Lift_Type_Root Type_Var0 root => SPeano p -> root Var0
type_var0 = lift_type_root . Type_Type0 . EPeano

-- * Type 'Type_Var1'
-- | The variable type of kind @* -> *@.
type Type_Var1 = Type_Type1 EPeano
instance Constraint_Type Eq (Type_Var1 root)

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

instance Eq_Type1 (Type_Var1 root) where
	eq_type1 (Type_Type1 p1 _) (Type_Type1 p2 _)
	 | p1 == p2
	 = Just Refl
	eq_type1 _ _ = Nothing
instance -- String_from_Type
 String_from_Type root =>
 String_from_Type (Type_Var1 root) where
	string_from_type (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 :: Lift_Type_Root Type_Var1 root => SPeano p -> root a -> root (Var1 a)
type_var1 p = lift_type_root . Type_Var1 p