{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'NonNull'.
module Language.Symantic.Compiling.NonNull where

import Control.Monad (liftM)
import Data.MonoTraversable (MonoFoldable)
import qualified Data.MonoTraversable as MT
import Data.NonNull (NonNull)
import qualified Data.NonNull as NonNull
import Data.Proxy
import Data.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Maybe (tyMaybe)
import Language.Symantic.Compiling.MonoFunctor
import Language.Symantic.Compiling.MonoFoldable
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_NonNull'
class Sym_NonNull term where
	fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
	toNullable :: MonoFoldable o => term (NonNull o) -> term o
	default fromNullable :: (Trans t term, MonoFoldable o) => t term o -> t term (Maybe (NonNull o))
	default toNullable :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term o
	fromNullable = trans_map1 fromNullable
	toNullable   = trans_map1 toNullable

type instance Sym_of_Iface (Proxy NonNull) = Sym_NonNull
type instance Consts_of_Iface (Proxy NonNull) = Proxy NonNull ': Consts_imported_by NonNull
type instance Consts_imported_by NonNull =
 [ Proxy Eq
 , Proxy Maybe
 , Proxy Ord
 , Proxy MT.MonoFoldable
 , Proxy MT.MonoFunctor
 ]

instance Sym_NonNull HostI where
	fromNullable = liftM NonNull.fromNullable
	toNullable   = liftM NonNull.toNullable
instance Sym_NonNull TextI where
	fromNullable = textI_app1 "fromNullable"
	toNullable   = textI_app1 "toNullable"
instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (DupI r1 r2) where
	fromNullable = dupI1 sym_NonNull fromNullable
	toNullable   = dupI1 sym_NonNull toNullable

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

instance -- Fam_MonoElement
 ( Proj_Const cs NonNull
 , Proj_Fam cs Fam_MonoElement
 ) => Proj_FamC cs Fam_MonoElement NonNull where
	proj_famC _c _fam ((TyConst c :$ ty_o) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy NonNull)
	 = proj_fam Fam_MonoElement (ty_o `TypesS` TypesZ)
	proj_famC _c _fam _ty = Nothing
instance -- Proj_ConC
 ( Proj_Const cs NonNull
 , Proj_Consts cs (Consts_imported_by NonNull)
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy NonNull) where
	proj_conC _ (t@(TyConst q) :$ (TyConst c :$ o))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy NonNull)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
		   , Just Con  <- proj_con (t :$ o) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFoldable)
		   , Just Con  <- proj_con (t :$ o) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFunctor)
		   , Just Con  <- proj_con (t :$ o) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)
		   , Just Con  <- proj_con (t :$ o) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) NonNull
 , Inj_Const (Consts_of_Ifaces is) Maybe
 , Inj_Const (Consts_of_Ifaces is) MonoFoldable
 , Proj_Con  (Consts_of_Ifaces is)
 , Term_from is ast
 ) => Term_fromI is (Proxy NonNull) ast where
	term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy NonNull ': rs)
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "fromNullable" -> fromNullable_from
		 "toNullable"   -> toNullable_from
		 _ -> Left $ Error_Term_unsupported
		where
		fromNullable_from =
		 -- fromNullable :: MonoFoldable o => o -> Maybe (NonNull o)
			from_ast1 ast $ \ast_o as ->
			term_from ast_o ctx $ \ty_o (TermLC o) ->
			check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
			k as (tyMaybe :$ (tyNonNull :$ ty_o)) $ TermLC $
			 \c -> fromNullable (o c)
		toNullable_from =
		 -- toNullable :: MonoFoldable o => NonNull o -> o
			from_ast1 ast $ \ast_n as ->
			term_from ast_n ctx $ \ty_n (TermLC n) ->
			check_type1 tyNonNull ast_n ty_n $ \Refl ty_o ->
			check_constraint (At (Just ast_n) (tyMonoFoldable :$ ty_o)) $ \Con ->
			k as ty_o $ TermLC $
			 \c -> toNullable (n c)

-- | The 'NonNull' 'Type'
tyNonNull :: Inj_Const cs NonNull => Type cs NonNull
tyNonNull = TyConst inj_const

sym_NonNull :: Proxy Sym_NonNull
sym_NonNull = Proxy

syNonNull :: IsString a => [Syntax a] -> Syntax a
syNonNull = Syntax "NonNull"