Language/LOL/Symantic/Type/Var.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE Rank2Types #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# LANGUAGE TypeOperators #-}
   8 {-# LANGUAGE UndecidableInstances #-}
   9 -- | Type variable.
  10 module Language.LOL.Symantic.Type.Var where
  11
  12 import Data.Maybe (isJust)
  13
  14 import Language.LOL.Symantic.AST
  15 import Language.LOL.Symantic.Type.Common
  16 import Language.LOL.Symantic.Lib.Data.Peano
  17
  18 -- * Type 'Type_Var'
  19 -- | The variable type.
  20 data Type_Var (root:: * -> *) p where
  21         Type_Var :: SPeano p -> Type_Var root p
  22 type instance Root_of_Type      (Type_Var root) = root
  23 type instance Error_of_Type ast (Type_Var root) = ()
  24
  25 instance -- Type_Eq
  26  Type_Eq (Type_Var root) where
  27         type_eq (Type_Var x) (Type_Var y) = x `peano_eq` y
  28 instance -- Eq
  29  Eq (Type_Var root h) where
  30         x == y = isJust $ x `type_eq` y
  31 instance -- String_from_Type
  32  String_from_Type (Type_Var root) where
  33         string_from_type (Type_Var p) =
  34                 "a" ++ show (integral_from_peano p::Integer)
  35 instance -- Show
  36  Show (Type_Var root h) where
  37         show = string_from_type
  38 instance -- Type_from AST
  39  ( Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
  40  , Implicit_HBool (Is_Last_Type (Type_Var root) root)
  41  ) => Type_from AST (Type_Var root) where
  42         type_from px_ty ast _k =
  43                 Left $ error_type_unsupported px_ty ast
  44
  45 -- | Convenient alias to include a 'Type_Var' within a type.
  46 type_var :: Type_Root_Lift Type_Var root => SPeano p -> root p
  47 type_var = type_root_lift . Type_Var