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

-- | Types suported by the modular transition systems.
module Copilot.Theorem.TransSys.Type
  ( Type (..)
  , U (..)
  ) where

import Data.Type.Equality

-- | A type at both value and type level.
--
-- Real numbers are mapped to 'Double's.
data Type a where
  Bool    :: Type Bool
  Integer :: Type Integer
  Real    :: Type Double

-- | Proofs of type equality.
instance TestEquality Type where
  testEquality :: forall a b. Type a -> Type b -> Maybe (a :~: b)
testEquality Type a
Bool    Type b
Bool     = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality Type a
Integer Type b
Integer  = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality Type a
Real    Type b
Real     = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality Type a
_       Type b
_        = Maybe (a :~: b)
forall a. Maybe a
Nothing

-- | Unknown types.
--
-- For instance, 'U Expr' is the type of an expression of unknown type
data U f = forall t . U (f 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"