{-# 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.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 Zipper = Sym_Zipper
class Sym_Zipper term where
	axis_descendant         :: Ord k => term (Zipper k a) -> term [Zipper k a]
	axis_descendant_or_self :: Ord k => term (Zipper k a) -> term [Zipper k a]
	axis_child              :: Ord k => term (Zipper k a) -> term [Zipper k a]
	axis_child_lookup       :: Ord k => Alternative f => term k -> term (Zipper k a) -> term (f (Zipper k a))
	axis_child_lookups      :: Ord k => Alternative f => Monad f => term (TreeMap.Path k) -> term (Zipper k a) -> term (f (Zipper k a))
	axis_child_first        :: Ord k => Alternative f => term (Zipper k a) -> term (f (Zipper k a))
	axis_child_last         :: Ord k => Alternative f => term (Zipper k a) -> term (f (Zipper k a))
	axis_ancestor           :: Ord k => term (Zipper k a) -> term [Zipper k a]
	axis_ancestor_or_self   :: Ord k => term (Zipper k a) -> term [Zipper k a]
	axis_preceding          :: Ord k => term (Zipper k a) -> term [Zipper k a]
	axis_preceding_sibling  :: Ord k => term (Zipper k a) -> term [Zipper k a]
	axis_following          :: Ord k => term (Zipper k a) -> term [Zipper k a]
	axis_following_sibling  :: Ord k => term (Zipper k a) -> term [Zipper k a]
	axis_parent             :: Ord k => term (Zipper k a) -> term [Zipper k a]
	default axis_descendant         :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default axis_descendant_or_self :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default axis_child              :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default axis_child_lookup       :: Sym_Zipper (UnT term) => Trans term => Ord k => Alternative f => term k -> term (Zipper k a) -> term (f (Zipper k a))
	default axis_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 axis_child_first        :: Sym_Zipper (UnT term) => Trans term => Ord k => Alternative f => term (Zipper k a) -> term (f (Zipper k a))
	default axis_child_last         :: Sym_Zipper (UnT term) => Trans term => Ord k => Alternative f => term (Zipper k a) -> term (f (Zipper k a))
	default axis_ancestor           :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default axis_ancestor_or_self   :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default axis_preceding          :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default axis_preceding_sibling  :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default axis_following          :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default axis_following_sibling  :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	default axis_parent             :: Sym_Zipper (UnT term) => Trans term => Ord k => term (Zipper k a) -> term [Zipper k a]
	axis_descendant         = trans1 axis_descendant
	axis_descendant_or_self = trans1 axis_descendant_or_self
	axis_child              = trans1 axis_child
	axis_child_lookup       = trans2 axis_child_lookup
	axis_child_lookups      = trans2 axis_child_lookups
	axis_child_first        = trans1 axis_child_first
	axis_child_last         = trans1 axis_child_last
	axis_ancestor           = trans1 axis_ancestor
	axis_ancestor_or_self   = trans1 axis_ancestor_or_self
	axis_preceding          = trans1 axis_preceding
	axis_preceding_sibling  = trans1 axis_preceding_sibling
	axis_following          = trans1 axis_preceding
	axis_following_sibling  = trans1 axis_preceding
	axis_parent             = trans1 axis_preceding

instance Sym_Zipper Eval where
	axis_descendant         = eval1 Zipper.axis_descendant
	axis_descendant_or_self = eval1 Zipper.axis_descendant_or_self
	axis_child              = eval1 Zipper.axis_child
	axis_child_lookup       = eval2 Zipper.axis_child_lookup
	axis_child_lookups      = eval2 Zipper.axis_child_lookups
	axis_child_first        = eval1 Zipper.axis_child_first
	axis_child_last         = eval1 Zipper.axis_child_last
	axis_ancestor           = eval1 Zipper.axis_ancestor
	axis_ancestor_or_self   = eval1 Zipper.axis_ancestor_or_self
	axis_preceding          = eval1 Zipper.axis_preceding
	axis_preceding_sibling  = eval1 Zipper.axis_preceding_sibling
	axis_following          = eval1 Zipper.axis_following
	axis_following_sibling  = eval1 Zipper.axis_following_sibling
	axis_parent             = eval1 Zipper.axis_parent
instance Sym_Zipper View where
	axis_descendant         = view1 "TreeMap.Zipper.descendant"
	axis_descendant_or_self = view1 "TreeMap.Zipper.descendant_or_self"
	axis_child              = view1 "TreeMap.Zipper.child"
	axis_child_lookup       = view2 "TreeMap.Zipper.child_lookup"
	axis_child_lookups      = view2 "TreeMap.Zipper.child_lookups"
	axis_child_first        = view1 "TreeMap.Zipper.child_first"
	axis_child_last         = view1 "TreeMap.Zipper.child_last"
	axis_ancestor           = view1 "TreeMap.Zipper.ancestor"
	axis_ancestor_or_self   = view1 "TreeMap.Zipper.ancestor_or_self"
	axis_preceding          = view1 "TreeMap.Zipper.preceding"
	axis_preceding_sibling  = view1 "TreeMap.Zipper.preceding_sibling"
	axis_following          = view1 "TreeMap.Zipper.following"
	axis_following_sibling  = view1 "TreeMap.Zipper.following_sibling"
	axis_parent             = view1 "TreeMap.Zipper.parent"
instance (Sym_Zipper r1, Sym_Zipper r2) => Sym_Zipper (Dup r1 r2) where
	axis_descendant         = dup1 @Sym_Zipper axis_descendant
	axis_descendant_or_self = dup1 @Sym_Zipper axis_descendant_or_self
	axis_child              = dup1 @Sym_Zipper axis_child
	axis_child_lookup       = dup2 @Sym_Zipper axis_child_lookup
	axis_child_lookups      = dup2 @Sym_Zipper axis_child_lookups
	axis_child_first        = dup1 @Sym_Zipper axis_child_first
	axis_child_last         = dup1 @Sym_Zipper axis_child_last
	axis_ancestor           = dup1 @Sym_Zipper axis_ancestor
	axis_ancestor_or_self   = dup1 @Sym_Zipper axis_ancestor_or_self
	axis_preceding          = dup1 @Sym_Zipper axis_preceding
	axis_preceding_sibling  = dup1 @Sym_Zipper axis_preceding_sibling
	axis_following          = dup1 @Sym_Zipper axis_following
	axis_following_sibling  = dup1 @Sym_Zipper axis_following_sibling
	axis_parent             = dup1 @Sym_Zipper axis_parent
instance (Sym_Zipper term, Sym_Lambda term) => Sym_Zipper (BetaT term)

instance NameTyOf Zipper where
	nameTyOf _c = ["TreeMap", "Zipper"] `Mod` "Zipper"
instance FixityOf Zipper
instance ClassInstancesFor Zipper where
	proveConstraintFor _ (TyConst _ _ _q :$ 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 _ (tq@(TyConst _ _ q) :$ 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
 , SymInj 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, SymInj ss Zipper) => ModuleFor src ss Zipper where
	moduleFor = ["TreeMap", "Zipper"] `moduleWhere`
	 [
	 ]