{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for '[]'.
module Language.Symantic.Lib.List where

import Data.Semigroup ((<>))
import Prelude hiding (zipWith)
import qualified Data.Functor as Functor
import qualified Data.List as List
import qualified Data.MonoTraversable as MT
import qualified Data.Sequences as Seqs
import qualified Data.Text as Text
import qualified Data.Traversable as Traversable

import Language.Symantic
import Language.Symantic.Grammar
import Language.Symantic.Lib.Function (a0, b1, c2)
import Language.Symantic.Lib.MonoFunctor (Element)

-- * Class 'Sym_List'
type instance Sym (Proxy []) = Sym_List
class Sym_List term where
	list_empty :: term [a]
	list_cons  :: term a -> term [a] -> term [a]; infixr 5 `list_cons`
	list       :: [term a] -> term [a]
	zipWith    :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
	
	default list_empty :: Sym_List (UnT term) => Trans term => term [a]
	default list_cons  :: Sym_List (UnT term) => Trans term => term a -> term [a] -> term [a]
	default list       :: Sym_List (UnT term) => Trans term => [term a] -> term [a]
	default zipWith    :: Sym_List (UnT term) => Trans term => term (a -> b -> c) -> term [a] -> term [b] -> term [c]
	
	list_empty = trans list_empty
	list_cons  = trans2 list_cons
	list l     = trans (list (unTrans Functor.<$> l))
	zipWith    = trans3 zipWith

-- Interpreting
instance Sym_List Eval where
	list_empty = return []
	list_cons  = eval2 (:)
	list       = Traversable.sequence
	zipWith    = eval3 List.zipWith
instance Sym_List View where
	list_empty = View $ \_p _v -> "[]"
	list_cons = viewInfix ":" (infixR 5)
	list l = View $ \_po v ->
		"[" <> Text.intercalate ", " ((\(View a) -> a op v) Functor.<$> l) <> "]"
		where op = (infixN0, SideL)
	zipWith = view3 "zipWith"
instance (Sym_List r1, Sym_List r2) => Sym_List (Dup r1 r2) where
	list_empty = dup0 @Sym_List list_empty
	list_cons  = dup2 @Sym_List list_cons
	list l =
		let (l1, l2) =
			foldr (\(x1 `Dup` x2) (xs1, xs2) ->
				(x1:xs1, x2:xs2)) ([], []) l in
		list l1 `Dup` list l2
	zipWith = dup3 @Sym_List zipWith

-- Transforming
instance (Sym_List term, Sym_Lambda term) => Sym_List (BetaT term)

-- Typing
instance FixityOf [] where
instance ClassInstancesFor [] where
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
	 | Just HRefl <- proj_ConstKiTy @_ @[] z
	 = case () of
		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
		   | Just Refl <- proj_Const @Foldable    q -> Just Dict
		   | Just Refl <- proj_Const @Functor     q -> Just Dict
		   | Just Refl <- proj_Const @Monad       q -> Just Dict
		   | Just Refl <- proj_Const @Traversable q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ z a))
	 | Just HRefl <- proj_ConstKiTy @_ @[] z
	 = case () of
		 _ | Just Refl <- proj_Const @Eq q
		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
		   | Just Refl <- proj_Const @Monoid q -> Just Dict
		   | Just Refl <- proj_Const @Show q
		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
		   | Just Refl <- proj_Const @Ord q
		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
		   | Just Refl <- proj_Const @MT.MonoFoldable   q -> Just Dict
		   | Just Refl <- proj_Const @MT.MonoFunctor    q -> Just Dict
		   | Just Refl <- proj_Const @Seqs.IsSequence   q -> Just Dict
		   | Just Refl <- proj_Const @Seqs.SemiSequence q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor [] where
	expandFamFor _c _len f ((TyApp _ z a) `TypesS` TypesZ)
	 | Just HRefl <- proj_ConstKi   @_ @Element f
	 , Just HRefl <- proj_ConstKiTy @_ @[] z
	 = Just a
	expandFamFor _c _len _fam _as = Nothing

-- Compiling
instance
 ( Gram_App g
 , Gram_Rule g
 , Gram_Comment g
 , Gram_Term src ss g
 , Inj_Sym ss []
 ) => Gram_Term_AtomsFor src ss g [] where
	g_term_atomsFor _t =
	 [ rule "teList_list" $
		between (symbol "[") (symbol "]") listG
	 , rule "teList_empty" $
		withMeta $
		(\src -> BinTree0 $ Token_Term $ TermVT_CF teList_empty `setSource` src)
		 <$ symbol "["
		 <* symbol "]"
	 ]
		where
		listG :: CF g (AST_Term src ss)
		listG = rule "list" $
			withMeta $
			(\a mb src ->
				case mb of
				 Just b_  -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_cons) a) b_
				 Nothing ->
					BinTree2
					 (BinTree2 (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_cons) a)
					 (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_empty))
			 <$> g_term
			 <*> option Nothing (Just <$ symbol "," <*> listG)
instance (Source src, Inj_Sym ss []) => Module src ss [] where
	module_ _s = [] `moduleWhere`
	 [ "[]"      := teList_empty
	 , "zipWith" := teList_zipWith
	 , ":" `withInfixR` 5 := teList_cons
	 ]

-- ** 'Type's
tyList :: Source src => Inj_Len vs => Type src vs a -> Type src vs [a]
tyList = (tyConst @(K []) @[] `tyApp`)

-- ** 'Term's
teList_empty ::
 Source src => Inj_Sym ss [] =>
 Term src ss ts '[Proxy a] [a]
teList_empty = Term noConstraint (tyList a0) $ teSym @[] $ list_empty

teList_cons ::
 Source src => Inj_Sym ss [] =>
 Term src ss ts '[Proxy a] (a -> [a] -> [a])
teList_cons =
	Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $
	teSym @[] $ lam2 list_cons

teList_zipWith ::
 Source src => Inj_Sym ss [] =>
 Term src ss ts '[Proxy a, Proxy b, Proxy c]
                 ((a -> b -> c) -> [a] -> [b] -> [c])
teList_zipWith =
	Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $
	teSym @[] $ lam3 zipWith