{-# 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 #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
-- | Symantic for 'NonNull'.
module Language.Symantic.Compiling.NonNull where

import Control.Monad (liftM, liftM2)
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.Sequences (IsSequence, SemiSequence)
import Data.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (head, init, last, tail)

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Bool (tyBool)
import Language.Symantic.Compiling.Maybe (tyMaybe)
import Language.Symantic.Compiling.Tuple2 (tyTuple2)
import Language.Symantic.Compiling.MonoFunctor
import Language.Symantic.Compiling.MonoFoldable
import Language.Symantic.Compiling.Sequences (tyIsSequence, tySemiSequence)
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
	ncons :: SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
	nuncons :: IsSequence s => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
	head :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
	last :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
	tail :: IsSequence s => term (NonNull s) -> term s
	init :: IsSequence s => term (NonNull s) -> term s
	nfilter :: IsSequence s => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
	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
	default ncons :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term (NonNull s)
	default nuncons :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term (MT.Element s, Maybe (NonNull s))
	default head :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
	default last :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
	default tail :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
	default init :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
	default nfilter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term (NonNull s) -> t term s
	fromNullable = trans_map1 fromNullable
	toNullable   = trans_map1 toNullable
	ncons        = trans_map2 ncons
	nuncons      = trans_map1 nuncons
	head         = trans_map1 head
	last         = trans_map1 last
	tail         = trans_map1 tail
	init         = trans_map1 init
	nfilter      = trans_map2 nfilter

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 (->)
 , Proxy (,)
 , Proxy Eq
 , Proxy Maybe
 , Proxy Ord
 , Proxy MT.MonoFoldable
 , Proxy MT.MonoFunctor
 , Proxy IsSequence
 , Proxy SemiSequence
 ]

instance Sym_NonNull HostI where
	fromNullable = liftM  NonNull.fromNullable
	toNullable   = liftM  NonNull.toNullable
	ncons        = liftM2 NonNull.ncons
	nuncons      = liftM  NonNull.nuncons
	head         = liftM  NonNull.head
	last         = liftM  NonNull.last
	tail         = liftM  NonNull.tail
	init         = liftM  NonNull.init
	nfilter      = liftM2 NonNull.nfilter
instance Sym_NonNull TextI where
	fromNullable = textI_app1 "fromNullable"
	toNullable   = textI_app1 "toNullable"
	ncons        = textI_app2 "ncons"
	nuncons      = textI_app1 "nuncons"
	head         = textI_app1 "head"
	last         = textI_app1 "last"
	tail         = textI_app1 "tail"
	init         = textI_app1 "init"
	nfilter      = textI_app2 "nfilter"
instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (DupI r1 r2) where
	fromNullable = dupI1 sym_NonNull fromNullable
	toNullable   = dupI1 sym_NonNull toNullable
	ncons        = dupI2 sym_NonNull ncons
	nuncons      = dupI1 sym_NonNull nuncons
	head         = dupI1 sym_NonNull head
	last         = dupI1 sym_NonNull last
	tail         = dupI1 sym_NonNull tail
	init         = dupI1 sym_NonNull init
	nfilter      = dupI2 sym_NonNull nfilter

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
		   | Just Refl <- proj_const q (Proxy::Proxy SemiSequence)
		   , 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) (->)
 , Inj_Const (Consts_of_Ifaces is) (,)
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Inj_Const (Consts_of_Ifaces is) Maybe
 , Inj_Const (Consts_of_Ifaces is) MonoFoldable
 , Inj_Const (Consts_of_Ifaces is) IsSequence
 , Inj_Const (Consts_of_Ifaces is) SemiSequence
 , Proj_Con  (Consts_of_Ifaces is)
 , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 , 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
		 "ncons"        -> ncons_from
		 "nuncons"      -> nuncons_from
		 "head"         -> n2e_from head
		 "last"         -> n2e_from last
		 "tail"         -> n2s_from tail
		 "init"         -> n2s_from init
		 "nfilter"      -> nfilter_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)
		ncons_from =
		 -- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s
			from_ast2 ast $ \ast_e ast_s as ->
			term_from ast_e ctx $ \ty_e (TermLC e) ->
			term_from ast_s ctx $ \ty_s (TermLC s) ->
			check_constraint (At (Just ast_s) (tySemiSequence :$ ty_s)) $ \Con ->
			check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type (At Nothing ty_s_e) (At (Just ast_e) ty_e) $ \Refl ->
			k as (tyNonNull :$ ty_s) $ TermLC $
			 \c -> ncons (e c) (s c)
		nuncons_from =
		 -- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s))
			from_ast1 ast $ \ast_n as ->
			term_from ast_n ctx $ \ty_n (TermLC n) ->
			check_type1 tyNonNull ast_n ty_n $ \Refl ty_s ->
			check_constraint (At (Just ast_n) (tyIsSequence :$ ty_s)) $ \Con ->
			check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type (At Nothing ty_s_e) (At (Just ast_n) ty_s_e) $ \Refl ->
			k as (tyTuple2 :$ ty_s_e :$ (tyMaybe :$ (tyNonNull :$ ty_s))) $ TermLC $
			 \c -> nuncons (n c)
		n2e_from
		 (f::forall term o.
			 (Sym_NonNull term, MonoFoldable o)
			 => term (NonNull o) -> term (MT.Element o)) =
		 -- head :: MonoFoldable o => NonNull o -> MT.Element o
		 -- last :: MonoFoldable o => NonNull o -> MT.Element 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 ->
			check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			k as ty_o_e $ TermLC $
			 \c -> f (n c)
		n2s_from
		 (f::forall term s.
			 (Sym_NonNull term, IsSequence s)
			 => term (NonNull s) -> term s) =
		 -- tail :: IsSequence s => NonNull s -> s
		 -- init :: IsSequence s => NonNull s -> s
			from_ast1 ast $ \ast_n as ->
			term_from ast_n ctx $ \ty_n (TermLC n) ->
			check_type1 tyNonNull ast_n ty_n $ \Refl ty_s ->
			check_constraint (At (Just ast_n) (tyIsSequence :$ ty_s)) $ \Con ->
			k as ty_s $ TermLC $
			 \c -> f (n c)
		nfilter_from =
		 -- filter :: IsSequence s => (MT.Element s -> Bool) -> NonNull s -> s
			from_ast2 ast $ \ast_e2Bool ast_n as ->
			term_from ast_e2Bool ctx $ \ty_e2Bool (TermLC e2Bool) ->
			term_from ast_n      ctx $ \ty_n      (TermLC s) ->
			check_type2 tyFun ast_e2Bool ty_e2Bool $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
			check_type (At Nothing tyBool) (At (Just ast_e2Bool) ty_e2Bool_Bool) $ \Refl ->
			check_type1 tyNonNull ast_n ty_n $ \Refl ty_s ->
			check_constraint (At (Just ast_n) (tyIsSequence :$ ty_s)) $ \Con ->
			check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type (At Nothing ty_s_e) (At (Just ast_e2Bool) ty_e2Bool_e) $ \Refl ->
			k as ty_s $ TermLC $
			 \c -> nfilter (e2Bool c) (s 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"