{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Constrained.FunctionSymbol where

import Constrained.List

import Data.Kind
import Data.Typeable

-- ========================================================================
-- Useful for testing if two function symbols are `the same` for some notion of `the same`

sameFunSym ::
  forall (t1 :: [Type] -> Type -> Type) d1 r1 (t2 :: [Type] -> Type -> Type) d2 r2.
  ( Typeable t1
  , Typeable d1
  , Typeable r1
  , Typeable t2
  , Typeable d2
  , Typeable r2
  , Eq (t1 d1 r1)
  ) =>
  t1 d1 r1 ->
  t2 d2 r2 ->
  Maybe (t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym :: forall (t1 :: [*] -> * -> *) (d1 :: [*]) r1 (t2 :: [*] -> * -> *)
       (d2 :: [*]) r2.
(Typeable t1, Typeable d1, Typeable r1, Typeable t2, Typeable d2,
 Typeable r2, Eq (t1 d1 r1)) =>
t1 d1 r1 -> t2 d2 r2 -> Maybe (t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym t1 d1 r1
x t2 d2 r2
y = do
  t1 :~: t2
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @t1 @t2
  d1 :~: d2
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @d1 @d2
  r1 :~: r2
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @r1 @r2
  if t1 d1 r1
x forall a. Eq a => a -> a -> Bool
== t2 d2 r2
y
    then forall a. a -> Maybe a
Just (forall {k} (a :: k). a :~: a
Refl, forall {k} (a :: k). a :~: a
Refl, forall {k} (a :: k). a :~: a
Refl)
    else forall a. Maybe a
Nothing

-- | Here we only care about the Type 't', the dom, and the rng can be
-- anything. Useful for defining patterns.
getWitness ::
  forall t t' d r.
  ( Typeable t
  , Typeable d
  , Typeable r
  , Typeable t'
  ) =>
  t d r -> Maybe (t' d r)
getWitness :: forall {k} {k} (t :: k -> k -> *) (t' :: k -> k -> *) (d :: k)
       (r :: k).
(Typeable t, Typeable d, Typeable r, Typeable t') =>
t d r -> Maybe (t' d r)
getWitness = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast

-- | Semantic operations are ones that give the function symbol, meaning as a function.
--   I.e. how to apply the function to a list of arguments and return a value.
class Semantics (t :: [Type] -> Type -> Type) where
  semantics :: t d r -> FunTy d r -- e.g. FunTy '[a, Int] Bool ~ a -> Int -> Bool