{-# LANGUAGE Trustworthy, MultiParamTypeClasses, FunctionalDependencies, TypeOperators, FlexibleInstances, UndecidableInstances, ScopedTypeVariables #-}

module Data.CaseScheme where

-- | Inference of case schemes from sum of product representations.
import Generics.Pointless.Functors hiding (fmap, Functor)
import Generics.Pointless.Combinators

class Case1 t u v | t u -> v where
	precase :: t u -> v -> u

instance (Case1 t u w) => Case1 (Const v :*: t) u (v -> w) where
	precase (ProdF (ConsF x) f1) g = precase f1 (g x)

instance (Case1 t u w) => Case1 (Id :*: t) u (u -> w) where
	precase (ProdF (IdF x) f1) g = precase f1 (g x)

instance Case1 (Const t) u (t -> u) where
	precase (ConsF x) f = f x

instance Case1 Id u u where
	precase _ = id

class Case2 t u v | t u -> v where
	cases :: t u -> v

pointed :: forall t u v. (Pointed t, Case2 t u v) => Ann (t u) -> u -> v
pointed _ x = cases (point x :: t u)

instance (Case1 t1 u v1, Case2 t2 u v2, Pointed t2) => Case2 (t1 :+: t2) u (v1 -> v2) where
	cases (InlF f) x = pointed (_L :: Ann (t2 u)) (precase f x)
	cases (InrF f) _ = cases f :: v2

-- While this is morally (Case1 t u v) => Case2 t u v, it has to be
-- split into multiple instances.
instance (Case1 (t1 :*: t2) u v) => Case2 (t1 :*: t2) u (v -> u) where
	cases = precase

instance Case2 (Const t) u ((t -> u) -> u) where
	cases (ConsF x) f = f x

instance Case2 Id u (u -> u) where
	cases _ = id

-- | Pointeds are needed because of the constraint on :+: ..
class Pointed t where -- Redefined here
	point :: u -> t u

instance Pointed Id where
	point = IdF

instance (Pointed t1, Pointed t2) => Pointed (t1 :*: t2) where
	point x = ProdF (point x) (point x)

instance (Pointed t1, Pointed t2) => Pointed (t1 :+: t2) where
	point = InrF . point

instance (Pointed t1, Pointed t2) => Pointed (t1 :@: t2) where
	point = CompF . point . point

test = cases (InlF (ProdF (ConsF 1) (ProdF (ConsF 2) (ConsF True)))
		:: ((Const Int :*: (Const Int :*: Const Bool)) :+: Id) Bool)
	(\(n1 :: Int) n2 b -> (n1 + n2 == 3) == b)
	False