{-# 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 NameTyOf Maybe where
        nameTyOf _c = ["Maybe"] `Mod` "Maybe"
instance FixityOf Maybe
instance ClassInstancesFor Maybe where
        proveConstraintFor _ (TyConst _ _ q :$ m)
         | Just HRefl <- proj_ConstKiTy @_ @Maybe m
         = 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 _ (tq@(TyConst _ _ q) :$ m:@a)
         | Just HRefl <- proj_ConstKiTy @_ @Maybe m
         = 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 (m:@a `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi @_ @Element f
         , Just HRefl <- proj_ConstKiTy @_ @Maybe m
         = Just a
        expandFamFor _c _len _fam _as = Nothing

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

-- ** 'Type's
tyMaybe :: Source src => LenInj 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'