{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module Arith.NonBase where

import Data.Kind
import Data.Type.Equality

-- import NonBaseTH


data Typ t where
  TInt :: Typ Int
  TBool :: Typ Bool
  TPair :: Typ a -> Typ b -> Typ (a, b)
  TFun :: Typ a -> Typ b -> Typ (a -> b)
deriving instance Show (Typ t)

instance TestEquality Typ where
  testEquality TInt TInt = Just Refl
  testEquality TBool TBool = Just Refl
  testEquality (TPair a b) (TPair a' b')
    | Just Refl <- testEquality a a'
    , Just Refl <- testEquality b b'
    = Just Refl
  testEquality (TFun a b) (TFun a' b')
    | Just Refl <- testEquality a a'
    , Just Refl <- testEquality b b'
    = Just Refl
  testEquality _ _ = Nothing

data PrimOp a b where
  POAddI :: PrimOp (Int, Int) Int
  POMulI :: PrimOp (Int, Int) Int
  POEqI :: PrimOp (Int, Int) Bool
deriving instance Show (PrimOp a b)

type Arith :: Type -> Type
data Arith t where
  A_Var :: Typ t -> String -> Arith t
  A_Let :: String -> Typ a -> Arith a -> Arith b -> Arith b
  A_Prim :: PrimOp a b -> Arith a -> Arith b
  A_Pair :: Arith a -> Arith b -> Arith (a, b)
  A_If :: Arith Bool -> Arith a -> Arith a -> Arith a
  A_Mono :: Arith Bool -> Arith Bool