--------------------------------------------------------------------------------

{-# LANGUAGE ExistentialQuantification, GADTs #-}
{-# LANGUAGE Safe #-}

module Copilot.Theorem.TransSys.Type
  ( Type (..)
  , U (..)
  , U2 (..)
  ) where

import Copilot.Core.Type.Equality

--------------------------------------------------------------------------------

data Type a where
  Bool    :: Type Bool
  Integer :: Type Integer
  Real    :: Type Double

instance EqualType Type where
  Type a
Bool    =~= :: Type a -> Type b -> Maybe (Equal a b)
=~= Type b
Bool     = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  Type a
Integer =~= Type b
Integer  = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  Type a
Real    =~= Type b
Real     = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  Type a
_       =~= Type b
_        = Maybe (Equal a b)
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------

-- For instance, 'U Expr' is the type of an expression of unknown type

data U f = forall t . U (f t)
data U2 f g = forall t . U2 (f t) (g t)

--------------------------------------------------------------------------------

instance Show (Type t) where
  show :: Type t -> String
show Type t
Integer = String
"Int"
  show Type t
Bool    = String
"Bool"
  show Type t
Real    = String
"Real"

--------------------------------------------------------------------------------