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

import Control.Applicative (Alternative(..))
import Control.Monad (Monad)
import Data.Eq (Eq)
import Data.Maybe (Maybe(..))
import Data.Ord (Ord)
import Data.Proxy
import Data.TreeMap.Strict.Zipper (Zipper)
import Data.Type.Equality ((:~:)(Refl))
import Text.Show (Show(..))
import qualified Data.TreeMap.Strict as TreeMap
import qualified Data.TreeMap.Strict.Zipper as Zipper
{-
import Data.Foldable (Foldable(..))
import Data.Function (($))
import Data.Functor (Functor(..))
import Data.Monoid (Monoid(..))
import Data.NonNull (NonNull)
import Data.Traversable (Traversable(..))
-}

import Language.Symantic.Grammar
import Language.Symantic
import Language.Symantic.Lib ()

-- * Class 'Sym_Zipper'
type instance Sym (Proxy Zipper) = 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         :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default zipper_descendant_or_self :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default zipper_child              :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default zipper_child_lookup       :: Sym_Zipper (UnT term) => Trans term => Ord k => Alternative f => term k -> term (Zipper k a) -> term (f (Zipper k a))
	default zipper_child_lookups      :: Sym_Zipper (UnT term) => Trans term => Ord k => Alternative f => Monad f => term (TreeMap.Path k) -> term (Zipper k a) -> term (f (Zipper k a))
	default zipper_child_first        :: Sym_Zipper (UnT term) => Trans term => Ord k => Alternative f => term (Zipper k a) -> term (f (Zipper k a))
	default zipper_child_last         :: Sym_Zipper (UnT term) => Trans term => Ord k => Alternative f => term (Zipper k a) -> term (f (Zipper k a))
	default zipper_ancestor           :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default zipper_ancestor_or_self   :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default zipper_preceding          :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default zipper_preceding_sibling  :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default zipper_following          :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default zipper_following_sibling  :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default zipper_parent             :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	zipper_descendant         = trans1 zipper_descendant
	zipper_descendant_or_self = trans1 zipper_descendant_or_self
	zipper_child              = trans1 zipper_child
	zipper_child_lookup       = trans2 zipper_child_lookup
	zipper_child_lookups      = trans2 zipper_child_lookups
	zipper_child_first        = trans1 zipper_child_first
	zipper_child_last         = trans1 zipper_child_last
	zipper_ancestor           = trans1 zipper_ancestor
	zipper_ancestor_or_self   = trans1 zipper_ancestor_or_self
	zipper_preceding          = trans1 zipper_preceding
	zipper_preceding_sibling  = trans1 zipper_preceding_sibling
	zipper_following          = trans1 zipper_preceding
	zipper_following_sibling  = trans1 zipper_preceding
	zipper_parent             = trans1 zipper_preceding

instance Sym_Zipper Eval where
	zipper_descendant         = eval1 Zipper.zipper_descendant
	zipper_descendant_or_self = eval1 Zipper.zipper_descendant_or_self
	zipper_child              = eval1 Zipper.zipper_child
	zipper_child_lookup       = eval2 Zipper.zipper_child_lookup
	zipper_child_lookups      = eval2 Zipper.zipper_child_lookups
	zipper_child_first        = eval1 Zipper.zipper_child_first
	zipper_child_last         = eval1 Zipper.zipper_child_last
	zipper_ancestor           = eval1 Zipper.zipper_ancestor
	zipper_ancestor_or_self   = eval1 Zipper.zipper_ancestor_or_self
	zipper_preceding          = eval1 Zipper.zipper_preceding
	zipper_preceding_sibling  = eval1 Zipper.zipper_preceding_sibling
	zipper_following          = eval1 Zipper.zipper_following
	zipper_following_sibling  = eval1 Zipper.zipper_following_sibling
	zipper_parent             = eval1 Zipper.zipper_parent
instance Sym_Zipper View where
	zipper_descendant         = view1 "TreeMap.Zipper.descendant"
	zipper_descendant_or_self = view1 "TreeMap.Zipper.descendant_or_self"
	zipper_child              = view1 "TreeMap.Zipper.child"
	zipper_child_lookup       = view2 "TreeMap.Zipper.child_lookup"
	zipper_child_lookups      = view2 "TreeMap.Zipper.child_lookups"
	zipper_child_first        = view1 "TreeMap.Zipper.child_first"
	zipper_child_last         = view1 "TreeMap.Zipper.child_last"
	zipper_ancestor           = view1 "TreeMap.Zipper.ancestor"
	zipper_ancestor_or_self   = view1 "TreeMap.Zipper.ancestor_or_self"
	zipper_preceding          = view1 "TreeMap.Zipper.preceding"
	zipper_preceding_sibling  = view1 "TreeMap.Zipper.preceding_sibling"
	zipper_following          = view1 "TreeMap.Zipper.following"
	zipper_following_sibling  = view1 "TreeMap.Zipper.following_sibling"
	zipper_parent             = view1 "TreeMap.Zipper.parent"
instance (Sym_Zipper r1, Sym_Zipper r2) => Sym_Zipper (Dup r1 r2) where
	zipper_descendant         = dup1 @Sym_Zipper zipper_descendant
	zipper_descendant_or_self = dup1 @Sym_Zipper zipper_descendant_or_self
	zipper_child              = dup1 @Sym_Zipper zipper_child
	zipper_child_lookup       = dup2 @Sym_Zipper zipper_child_lookup
	zipper_child_lookups      = dup2 @Sym_Zipper zipper_child_lookups
	zipper_child_first        = dup1 @Sym_Zipper zipper_child_first
	zipper_child_last         = dup1 @Sym_Zipper zipper_child_last
	zipper_ancestor           = dup1 @Sym_Zipper zipper_ancestor
	zipper_ancestor_or_self   = dup1 @Sym_Zipper zipper_ancestor_or_self
	zipper_preceding          = dup1 @Sym_Zipper zipper_preceding
	zipper_preceding_sibling  = dup1 @Sym_Zipper zipper_preceding_sibling
	zipper_following          = dup1 @Sym_Zipper zipper_following
	zipper_following_sibling  = dup1 @Sym_Zipper zipper_following_sibling
	zipper_parent             = dup1 @Sym_Zipper zipper_parent
instance (Sym_Zipper term, Sym_Lambda term) => Sym_Zipper (BetaT term)

instance FixityOf Zipper
instance ClassInstancesFor Zipper where
	proveConstraintFor _ (TyApp _ (TyConst _ _ _q) (TyApp _ c _k))
	 | Just HRefl <- proj_ConstKiTy @(K Zipper) @Zipper c
	 = case () of
		 {-_ | Just Refl <- proj_Const @Functor     q -> Just Dict
		   | Just Refl <- proj_Const @Foldable    q -> Just Dict
		   | Just Refl <- proj_Const @Traversable q -> Just Dict
		   -}
		 _ -> Nothing
	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c k) a))
	 | Just HRefl <- proj_ConstKiTy @(K Zipper) @Zipper c
	 = case () of
		 _ | Just Refl <- proj_Const @Eq q
		   , Just Dict <- proveConstraint (tq `tyApp` k)
		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
		   {-| Just Refl <- proj_Const @Ord q
		   , Just Dict <- proveConstraint (tq `tyApp` k)
		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
		   | Just Refl <- proj_Const @Monoid q
		   , Just Dict <- proveConstraint (tyOrd k) -> Just Dict
		   -}
		   | Just Refl <- proj_Const @Show q
		   , Just Dict <- proveConstraint (tq `tyApp` k)
		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Zipper

instance -- Gram_Term_AtomsFor
 ( Gram_Alt g
 , Gram_Rule g
 , Gram_Comment g
 , Gram_Source src g
 , Inj_Sym ss Zipper
 ) => Gram_Term_AtomsFor src ss g Zipper where
	{-
	gs_term_atomsFor _t =
	 [ rule "term_account" $
		lexeme $ withMeta $
		(\a meta -> ProTokTe $ 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])
	-}
instance (Source src, Inj_Sym ss Zipper) => ModuleFor src ss Zipper where
	moduleFor _s = ["TreeMap", "Zipper"] `moduleWhere`
	 [
	 ]