{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Maybe'.
module Language.Symantic.Lib.Maybe where

import Control.Monad
import Prelude hiding (maybe)
import qualified Data.Maybe as Maybe
import qualified Data.MonoTraversable as MT

import Language.Symantic
import Language.Symantic.Lib.Function (a0, b1)
import Language.Symantic.Lib.MonoFunctor (Element)

-- * Class 'Sym_Maybe'
type instance Sym Maybe = Sym_Maybe
class Sym_Maybe term where
	_Nothing :: term (Maybe a)
	_Just    :: term a -> term (Maybe a)
	maybe    :: term b -> term (a -> b) -> term (Maybe a) -> term b
	
	default _Nothing :: Sym_Maybe (UnT term) => Trans term => term (Maybe a)
	default _Just    :: Sym_Maybe (UnT term) => Trans term => term a -> term (Maybe a)
	default maybe    :: Sym_Maybe (UnT term) => Trans term => term b -> term (a -> b) -> term (Maybe a) -> term b
	
	_Nothing = trans _Nothing
	_Just    = trans1 _Just
	maybe    = trans3 maybe

-- Interpreting
instance Sym_Maybe Eval where
	_Nothing = Eval  Nothing
	_Just    = eval1 Just
	maybe    = eval3 Maybe.maybe
instance Sym_Maybe View where
	_Nothing = view0 "Nothing"
	_Just    = view1 "Just"
	maybe    = view3 "maybe"
instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (Dup r1 r2) where
	_Nothing = dup0 @Sym_Maybe _Nothing
	_Just    = dup1 @Sym_Maybe _Just
	maybe    = dup3 @Sym_Maybe maybe

-- Transforming
instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term)

-- Typing
instance FixityOf Maybe
instance ClassInstancesFor Maybe where
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
	 | Just HRefl <- proj_ConstKiTy @_ @Maybe c
	 = case () of
		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
		   | Just Refl <- proj_Const @Foldable q    -> Just Dict
		   | Just Refl <- proj_Const @Functor q     -> Just Dict
		   | Just Refl <- proj_Const @Monad q       -> Just Dict
		   | Just Refl <- proj_Const @Traversable q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
	 | Just HRefl <- proj_ConstKiTy @_ @Maybe c
	 = case () of
		 _ | Just Refl <- proj_Const @Eq q
		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
		   | Just Refl <- proj_Const @Monoid q
		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
		   | Just Refl <- proj_Const @Show q
		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
		   | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Maybe where
	expandFamFor _c _len f (TyApp _ c a `TypesS` TypesZ)
	 | Just HRefl <- proj_ConstKi @_ @Element f
	 , Just HRefl <- proj_ConstKiTy @_ @Maybe c
	 = Just a
	expandFamFor _c _len _fam _as = Nothing

-- Compiling
instance Gram_Term_AtomsFor src ss g Maybe
instance (Source src, Inj_Sym ss Maybe) => ModuleFor src ss Maybe where
	moduleFor = ["Maybe"] `moduleWhere`
	 [ "Nothing" := teMaybe_Nothing
	 , "Just"    := teMaybe_Just
	 , "maybe"   := teMaybe_maybe
	 ]

-- ** 'Type's
tyMaybe :: Source src => Inj_Len vs => Type src vs a -> Type src vs (Maybe a)
tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)

-- ** 'Term's
teMaybe_Nothing :: TermDef Maybe '[Proxy a] (() #> Maybe a)
teMaybe_Nothing = Term noConstraint (tyMaybe a0) $ teSym @Maybe $ _Nothing

teMaybe_Just :: TermDef Maybe '[Proxy a] (() #> (a -> Maybe a))
teMaybe_Just = Term noConstraint (a0 ~> tyMaybe a0) $ teSym @Maybe $ lam1 _Just

teMaybe_maybe :: TermDef Maybe '[Proxy a, Proxy b] (() #> (b -> (a -> b) -> Maybe a -> b))
teMaybe_maybe = Term noConstraint (b1 ~> (a0 ~> b1) ~> tyMaybe a0 ~> b1) $ teSym @Maybe $ lam1 $ \b' -> lam $ lam . maybe b'