{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
-- | Symantic for 'Maybe'.
module Language.Symantic.Compiling.Maybe where

import Control.Monad
import qualified Data.Function as Fun
import qualified Data.Maybe as Maybe
import Data.Proxy
import Data.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (maybe)

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_Maybe_Lam'
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 :: Trans t term => t term (Maybe a)
	default _Just    :: Trans t term => t term a -> t term (Maybe a)
	default maybe    :: Trans t term => t term b -> t term (a -> b) -> t term (Maybe a) -> t term b
	
	_Nothing = trans_lift _Nothing
	_Just    = trans_map1 _Just
	maybe    = trans_map3 maybe

type instance Sym_of_Iface (Proxy Maybe) = Sym_Maybe
type instance Consts_of_Iface (Proxy Maybe) = Proxy Maybe ': Consts_imported_by Maybe
type instance Consts_imported_by Maybe =
 [ Proxy Applicative
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 , Proxy Traversable
 ]

instance Sym_Maybe HostI where
	_Nothing = HostI Nothing
	_Just    = liftM Just
	maybe    = liftM3 Maybe.maybe
instance Sym_Maybe TextI where
	_Nothing = textI_app0 "Nothing"
	_Just    = textI_app1 "Just"
	maybe    = textI_app3 "maybe"
instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
	_Nothing = dupI0 sym_Maybe _Nothing
	_Just    = dupI1 sym_Maybe _Just
	maybe    = dupI3 sym_Maybe maybe

instance Const_from Text cs => Const_from Text (Proxy Maybe ': cs) where
	const_from "Maybe" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
	show_const ConstZ{} = "Maybe"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs Maybe
 , Proj_Consts cs (Consts_imported_by Maybe)
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy Maybe) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy Maybe)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
		 _ -> Nothing
	proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy Maybe)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monoid)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Const_from (Lexem ast) (Consts_of_Ifaces is)
 , Inj_Const  (Consts_of_Ifaces is) Maybe
 , Inj_Const  (Consts_of_Ifaces is) (->)
 , Term_from is ast
 ) => Term_fromI is (Proxy Maybe) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "Nothing" -> _Nothing_from
		 "Just"    -> _Just_from
		 "maybe"   -> maybe_from
		 _ -> Left $ Error_Term_unsupported
		where
		_Nothing_from =
		 -- Nothing :: Maybe a
			from_ast1 ast $ \ast_ty_a as ->
			either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
			type_from ast_ty_a $ \ty_a -> Right $
			check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
			k as (tyMaybe :$ ty_a) $ TermLC $
			Fun.const _Nothing
		_Just_from =
		 -- Just :: a -> Maybe a
			from_ast1 ast $ \ast_a as ->
			term_from ast_a ctx $ \ty_a (TermLC a) ->
			k as (tyMaybe :$ ty_a) $ TermLC $
			 \c -> _Just (a c)
		maybe_from =
		 -- maybe :: b -> (a -> b) -> Maybe a -> b
			from_ast2 ast $ \ast_b ast_a2b as ->
			term_from ast_b   ctx $ \ty_b   (TermLC b) ->
			term_from ast_a2b ctx $ \ty_a2b (TermLC a2b) ->
			check_type2 tyFun ast_a2b ty_a2b $ \Refl ty_a2b_a ty_a2b_b ->
			check_type (At (Just ast_a2b) ty_a2b_b) (At (Just ast_b) ty_b) $ \Refl ->
			k as (tyMaybe :$ ty_a2b_a ~> ty_b) $ TermLC $
			 \c -> lam $ maybe (b c) (a2b c)

-- | The 'Maybe' 'Type'
tyMaybe :: Inj_Const cs Maybe => Type cs Maybe
tyMaybe = TyConst inj_const

sym_Maybe :: Proxy Sym_Maybe
sym_Maybe = Proxy

syMaybe :: IsString a => [Syntax a] -> Syntax a
syMaybe = Syntax "Maybe"

syNothing :: IsString a => [Syntax a] -> Syntax a
syNothing = Syntax "Nothing"

syJust :: IsString a => [Syntax a] -> Syntax a
syJust = Syntax "Just"