{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Zipper'.
module Hcompta.LCC.Sym.Zipper where

import Control.Applicative (Alternative(..))
import Control.Monad (Monad, liftM, liftM2)
import Data.Eq (Eq)
import Data.Function (($))
import Data.NonNull (NonNull)
import Data.Maybe (Maybe(..))
import Data.Monoid (Monoid(..))
import Data.Ord (Ord)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Text.Show (Show(..))
import qualified Prelude ()
import qualified Data.TreeMap.Strict.Zipper as Zipper
import qualified Data.TreeMap.Strict as TreeMap
import Data.TreeMap.Strict.Zipper (Zipper)

import Language.Symantic
-- import Language.Symantic.Lib.Lambda
import qualified Language.Symantic.Lib as Sym

-- * Class 'Sym_Zipper'
class Sym_Zipper term where
	zipper_descendant         :: Ord k => term (Zipper k a) -> term [Zipper k a]
	zipper_descendant_or_self :: Ord k => term (Zipper k a) -> term [Zipper k a]
	zipper_child              :: Ord k => term (Zipper k a) -> term [Zipper k a]
	zipper_child_lookup       :: (Ord k, Alternative f) => term k -> term (Zipper k a) -> term (f (Zipper k a))
	zipper_child_lookups      :: (Ord k, Alternative f, Monad f) => term (TreeMap.Path k) -> term (Zipper k a) -> term (f (Zipper k a))
	zipper_child_first        :: (Ord k, Alternative f) => term (Zipper k a) -> term (f (Zipper k a))
	zipper_child_last         :: (Ord k, Alternative f) => term (Zipper k a) -> term (f (Zipper k a))
	zipper_ancestor           :: Ord k => term (Zipper k a) -> term [Zipper k a]
	zipper_ancestor_or_self   :: Ord k => term (Zipper k a) -> term [Zipper k a]
	zipper_preceding          :: Ord k => term (Zipper k a) -> term [Zipper k a]
	zipper_preceding_sibling  :: Ord k => term (Zipper k a) -> term [Zipper k a]
	zipper_following          :: Ord k => term (Zipper k a) -> term [Zipper k a]
	zipper_following_sibling  :: Ord k => term (Zipper k a) -> term [Zipper k a]
	zipper_parent             :: Ord k => term (Zipper k a) -> term [Zipper k a]
	default zipper_descendant         :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
	default zipper_descendant_or_self :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
	default zipper_child              :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
	default zipper_child_lookup       :: (Trans t term, Ord k, Alternative f) => t term k -> t term (Zipper k a) -> t term (f (Zipper k a))
	default zipper_child_lookups      :: (Trans t term, Ord k, Alternative f, Monad f) => t term (TreeMap.Path k) -> t term (Zipper k a) -> t term (f (Zipper k a))
	default zipper_child_first        :: (Trans t term, Ord k, Alternative f) => t term (Zipper k a) -> t term (f (Zipper k a))
	default zipper_child_last         :: (Trans t term, Ord k, Alternative f) => t term (Zipper k a) -> t term (f (Zipper k a))
	default zipper_ancestor           :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
	default zipper_ancestor_or_self   :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
	default zipper_preceding          :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
	default zipper_preceding_sibling  :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
	default zipper_following          :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
	default zipper_following_sibling  :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
	default zipper_parent             :: (Trans t term, Ord k) => t term (Zipper k a) -> t term [Zipper k a]
	zipper_descendant         = trans_map1 zipper_descendant
	zipper_descendant_or_self = trans_map1 zipper_descendant_or_self
	zipper_child              = trans_map1 zipper_child
	zipper_child_lookup       = trans_map2 zipper_child_lookup
	zipper_child_lookups      = trans_map2 zipper_child_lookups
	zipper_child_first        = trans_map1 zipper_child_first
	zipper_child_last         = trans_map1 zipper_child_last
	zipper_ancestor           = trans_map1 zipper_ancestor
	zipper_ancestor_or_self   = trans_map1 zipper_ancestor_or_self
	zipper_preceding          = trans_map1 zipper_preceding
	zipper_preceding_sibling  = trans_map1 zipper_preceding_sibling
	zipper_following          = trans_map1 zipper_preceding
	zipper_following_sibling  = trans_map1 zipper_preceding
	zipper_parent             = trans_map1 zipper_preceding

type instance Sym_of_Iface (Proxy Zipper) = Sym_Zipper
type instance TyConsts_of_Iface (Proxy Zipper) = Proxy Zipper ': TyConsts_imported_by (Proxy Zipper)
type instance TyConsts_imported_by (Proxy Zipper) =
 [ Proxy Eq
 , Proxy Show
 , Proxy []
 ]

instance Sym_Zipper HostI where
	zipper_descendant         = liftM  Zipper.zipper_descendant
	zipper_descendant_or_self = liftM  Zipper.zipper_descendant_or_self
	zipper_child              = liftM  Zipper.zipper_child
	zipper_child_lookup       = liftM2 Zipper.zipper_child_lookup
	zipper_child_lookups      = liftM2 Zipper.zipper_child_lookups
	zipper_child_first        = liftM  Zipper.zipper_child_first
	zipper_child_last         = liftM  Zipper.zipper_child_last
	zipper_ancestor           = liftM  Zipper.zipper_ancestor
	zipper_ancestor_or_self   = liftM  Zipper.zipper_ancestor_or_self
	zipper_preceding          = liftM  Zipper.zipper_preceding
	zipper_preceding_sibling  = liftM  Zipper.zipper_preceding_sibling
	zipper_following          = liftM  Zipper.zipper_following
	zipper_following_sibling  = liftM  Zipper.zipper_following_sibling
	zipper_parent             = liftM  Zipper.zipper_parent
instance Sym_Zipper TextI where
	zipper_descendant         = textI1 "zipper_descendant"
	zipper_descendant_or_self = textI1 "zipper_descendant_or_self"
	zipper_child              = textI1 "zipper_child"
	zipper_child_lookup       = textI2 "zipper_child_lookup"
	zipper_child_lookups      = textI2 "zipper_child_lookups"
	zipper_child_first        = textI1 "zipper_child_first"
	zipper_child_last         = textI1 "zipper_child_last"
	zipper_ancestor           = textI1 "zipper_ancestor"
	zipper_ancestor_or_self   = textI1 "zipper_ancestor_or_self"
	zipper_preceding          = textI1 "zipper_preceding"
	zipper_preceding_sibling  = textI1 "zipper_preceding_sibling"
	zipper_following          = textI1 "zipper_following"
	zipper_following_sibling  = textI1 "zipper_following_sibling"
	zipper_parent             = textI1 "zipper_parent"
instance (Sym_Zipper r1, Sym_Zipper r2) => Sym_Zipper (DupI r1 r2) where
	zipper_descendant         = dupI1 @Sym_Zipper zipper_descendant
	zipper_descendant_or_self = dupI1 @Sym_Zipper zipper_descendant_or_self
	zipper_child              = dupI1 @Sym_Zipper zipper_child
	zipper_child_lookup       = dupI2 @Sym_Zipper zipper_child_lookup
	zipper_child_lookups      = dupI2 @Sym_Zipper zipper_child_lookups
	zipper_child_first        = dupI1 @Sym_Zipper zipper_child_first
	zipper_child_last         = dupI1 @Sym_Zipper zipper_child_last
	zipper_ancestor           = dupI1 @Sym_Zipper zipper_ancestor
	zipper_ancestor_or_self   = dupI1 @Sym_Zipper zipper_ancestor_or_self
	zipper_preceding          = dupI1 @Sym_Zipper zipper_preceding
	zipper_preceding_sibling  = dupI1 @Sym_Zipper zipper_preceding_sibling
	zipper_following          = dupI1 @Sym_Zipper zipper_following
	zipper_following_sibling  = dupI1 @Sym_Zipper zipper_following_sibling
	zipper_parent             = dupI1 @Sym_Zipper zipper_parent

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Zipper
 ) => Read_TyNameR TyName cs (Proxy Zipper ': rs) where
	read_TyNameR _cs (TyName "Zipper") k = k (ty @Zipper)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Zipper ': cs) where
	show_TyConst TyConstZ{} = "Zipper"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyFamC cs Sym.TyFam_MonoElement Zipper

instance -- Proj_TyConC
 ( Proj_TyConst cs Zipper
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Zipper))
 , Proj_TyCon cs
 , Inj_TyConst cs Ord
 ) => Proj_TyConC cs (Proxy Zipper) where
	proj_TyConC _ (TyConst _q :$ (TyConst c :$ _k))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Zipper)
	 = case () of
		   {-
		 _ | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Foldable)    -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
			 -}
		 _ -> Nothing
	proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ k :$ a))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Zipper)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Eq)
		   , Just TyCon  <- proj_TyCon (t :$ k)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		   {-
		   | Just Refl <- proj_TyConst q (Proxy @Ord)
		   , Just TyCon  <- proj_TyCon (t :$ k)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monoid)
		   , Just TyCon  <- proj_TyCon (ty @Ord :$ k) -> Just TyCon
		   -}
		   | Just Refl <- proj_TyConst q (Proxy @Show)
		   , Just TyCon  <- proj_TyCon (t :$ k)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy Zipper)
 = Token_Term_Zipper_descendant         (EToken meta ts)
 | Token_Term_Zipper_descendant_or_self (EToken meta ts)
 | Token_Term_Zipper_child              (EToken meta ts)
 | Token_Term_Zipper_child_lookup       (EToken meta '[Proxy Token_Type]) (EToken meta ts) (EToken meta ts)
 | Token_Term_Zipper_child_lookups      (EToken meta '[Proxy Token_Type]) (EToken meta ts) (EToken meta ts)
 | Token_Term_Zipper_child_first        (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 | Token_Term_Zipper_child_last         (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 | Token_Term_Zipper_ancestor           (EToken meta ts)
 | Token_Term_Zipper_ancestor_or_self   (EToken meta ts)
 | Token_Term_Zipper_preceding          (EToken meta ts)
 | Token_Term_Zipper_preceding_sibling  (EToken meta ts)
 | Token_Term_Zipper_following          (EToken meta ts)
 | Token_Term_Zipper_following_sibling  (EToken meta ts)
 | Token_Term_Zipper_parent             (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Zipper))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Zipper))

instance -- CompileI
 ( Inj_TyConst cs Zipper
 , Inj_TyConst cs []
 , Inj_TyConst cs Ord
 , Inj_TyConst cs Alternative
 , Inj_TyConst cs Monad
 , Inj_TyConst cs NonNull
 , Proj_TyCon cs
 , Read_TyName TyName cs
 , Compile cs is
 ) => CompileI cs is (Proxy Zipper) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Zipper_descendant         tok_z -> comp tok_z zipper_descendant
		 Token_Term_Zipper_descendant_or_self tok_z -> comp tok_z zipper_descendant_or_self
		 Token_Term_Zipper_child              tok_z -> comp tok_z zipper_child
		 Token_Term_Zipper_child_lookup  tok_ty_f tok_x tok_z -> comp_lookup  tok_ty_f tok_x tok_z zipper_child_lookup
		 Token_Term_Zipper_child_lookups tok_ty_f tok_x tok_z -> comp_lookups tok_ty_f tok_x tok_z zipper_child_lookups
		 Token_Term_Zipper_child_first tok_ty_f tok_z -> comp_child tok_ty_f tok_z zipper_child_first
		 Token_Term_Zipper_child_last  tok_ty_f tok_z -> comp_child tok_ty_f tok_z zipper_child_last
		 Token_Term_Zipper_ancestor           tok_z -> comp tok_z zipper_ancestor
		 Token_Term_Zipper_ancestor_or_self   tok_z -> comp tok_z zipper_ancestor_or_self
		 Token_Term_Zipper_preceding          tok_z -> comp tok_z zipper_preceding
		 Token_Term_Zipper_preceding_sibling  tok_z -> comp tok_z zipper_preceding_sibling
		 Token_Term_Zipper_following          tok_z -> comp tok_z zipper_following
		 Token_Term_Zipper_following_sibling  tok_z -> comp tok_z zipper_following_sibling
		 Token_Term_Zipper_parent             tok_z -> comp tok_z zipper_parent
		where
		comp tok_z
		 (op::forall term k a. (Sym_Zipper term, Ord k)
		    => term (Zipper k a) -> term [Zipper k a]) =
			compileO tok_z ctx $ \ty_z (TermO z) ->
			check_TyEq2 (ty @Zipper) (At (Just tok_z) ty_z) $ \Refl ty_k _ty_a ->
			check_TyCon (At (Just tok_z) (ty @Ord :$ ty_k)) $ \TyCon ->
			k (ty @[] :$ ty_z) $ TermO $
			 \c -> op (z c)
		comp_child tok_ty_f tok_z
		 (op::forall term f k a. (Sym_Zipper term, Ord k, Alternative f)
		    => term (Zipper k a) -> term (f (Zipper k a))) =
			compile_Type tok_ty_f $ \(ty_f::Type cs f) ->
			check_Kind
			 (At Nothing (SKiType `SKiArrow` SKiType))
			 (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
			check_TyCon (At (Just tok_ty_f) (ty @Alternative :$ ty_f)) $ \TyCon ->
			compileO tok_z ctx $ \ty_z (TermO z) ->
			check_TyEq2 (ty @Zipper) (At (Just tok_z) ty_z) $ \Refl ty_k _ty_a ->
			check_TyCon (At (Just tok_z) (ty @Ord :$ ty_k)) $ \TyCon ->
			k (ty_f :$ ty_z) $ TermO $
			 \c -> op (z c)
		comp_lookup tok_ty_f tok_x tok_z
		 (op::forall term f k a. (Sym_Zipper term, Ord k, Alternative f)
		    => term k -> term (Zipper k a) -> term (f (Zipper k a))) =
			compile_Type tok_ty_f $ \(ty_f::Type cs f) ->
			check_Kind
			 (At Nothing (SKiType `SKiArrow` SKiType))
			 (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
			check_TyCon (At (Just tok_ty_f) (ty @Alternative :$ ty_f)) $ \TyCon ->
			compileO tok_x ctx $ \ty_x (TermO x) ->
			compileO tok_z ctx $ \ty_z (TermO z) ->
			check_TyEq2 (ty @Zipper) (At (Just tok_z) ty_z) $ \Refl ty_k _ty_a ->
			check_TyCon (At (Just tok_z) (ty @Ord :$ ty_k)) $ \TyCon ->
			check_TyEq (At (Just tok_x) ty_x) (At (Just tok_z) ty_k) $ \Refl ->
			k (ty_f :$ ty_z) $ TermO $
			 \c -> op (x c) (z c)
		comp_lookups tok_ty_f tok_p tok_z
		 (op::forall term f k a. (Sym_Zipper term, Ord k, Alternative f, Monad f)
		    => term (TreeMap.Path k) -> term (Zipper k a) -> term (f (Zipper k a))) =
			compile_Type tok_ty_f $ \(ty_f::Type cs f) ->
			check_Kind
			 (At Nothing (SKiType `SKiArrow` SKiType))
			 (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
			check_TyCon (At (Just tok_ty_f) (ty @Alternative :$ ty_f)) $ \TyCon ->
			check_TyCon (At (Just tok_ty_f) (ty @Monad :$ ty_f)) $ \TyCon ->
			compileO tok_p ctx $ \ty_p (TermO p) ->
			compileO tok_z ctx $ \ty_z (TermO z) ->
			check_TyEq2 (ty @Zipper) (At (Just tok_z) ty_z) $ \Refl ty_k _ty_a ->
			check_TyCon (At (Just tok_z) (ty @Ord :$ ty_k)) $ \TyCon ->
			check_TyEq
			 (At (Just tok_z) $ ty @NonNull :$ (ty @[] :$ ty_k))
			 (At (Just tok_p) ty_p) $ \Refl ->
			k (ty_f :$ ty_z) $ TermO $
			 \c -> op (p c) (z c)
instance -- TokenizeT
 Inj_Token meta ts Zipper =>
 TokenizeT meta ts (Proxy Zipper) where
	tokenizeT _t = mempty
	 {- tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "-" (infixL 6) Token_Term_Subable_add
		 ]
	 -}
instance -- Gram_Term_AtomsT
 ( Alt g
 , Gram_Rule g
 , Gram_Lexer g
 , Gram_Meta meta g
 , Inj_Token meta ts Zipper
 ) => Gram_Term_AtomsT meta ts (Proxy Zipper) g where
	{-
	gs_term_atomsT _t =
	 [ rule "term_account" $
		lexeme $ metaG $
		(\a meta -> ProTok $ inj_EToken meta $ Token_Term_Zipper a)
		 <$> g_account
	 ]
		where
		g_account :: CF g Zipper
		g_account =
			Zipper . NonNull.impureNonNull
			 <$> some (id <$ char '/' <*> g_account_section)
		g_account_section :: CF g Zipper_Section
		g_account_section =
			Name . Text.pack
			 <$> some (choice $ unicat <$> [Unicat_Letter])
	-}