{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
-- | Symantic for '[]'.
module Language.Symantic.Compiling.List where

import Control.Monad (liftM3)
import qualified Data.Foldable as Foldable
import qualified Data.Function as Fun
import qualified Data.Functor as Functor
import qualified Data.List as List
import Data.Monoid ((<>))
import Data.Proxy
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Traversable as Traversable
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (zipWith)

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_List'
class Sym_List term where
	list_empty :: term [a]
	zipWith    :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
	list       :: [term a] -> term [a]
	
	default list_empty :: Trans t term => t term [a]
	default zipWith    :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c]
	default list       :: Trans t term => [t term a] -> t term [a]
	
	list_empty = trans_lift list_empty
	zipWith    = trans_map3 zipWith
	list l     = trans_lift (list (trans_apply Functor.<$> l))

type instance Sym_of_Iface (Proxy []) = Sym_List
type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by []
type instance Consts_imported_by [] =
 [ Proxy Applicative
 , Proxy Bool
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 , Proxy Ord
 , Proxy Show
 , Proxy Traversable
 ]

instance Sym_List HostI where
	list_empty = return []
	list       = Traversable.sequence
	zipWith    = liftM3 List.zipWith
instance Sym_List TextI where
	list_empty = TextI $ \_p _v -> "[]"
	list l = TextI $ \_p v ->
		let p' = precedence_Toplevel in
		"[" <> Text.intercalate ", " ((\(TextI a) -> a p' v) Functor.<$> l) <> "]"
	zipWith = textI_app3 "zipWith"
instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
	list_empty = dupI0 (Proxy @Sym_List) list_empty
	list l =
		let (l1, l2) =
			Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
				(x1:xs1, x2:xs2)) ([], []) l in
		list l1 `DupI` list l2
	zipWith = dupI3 (Proxy @Sym_List) zipWith

instance Const_from Text cs => Const_from Text (Proxy [] ': cs) where
	const_from "[]" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy [] ': cs) where
	show_const ConstZ{} = "[]"
	show_const (ConstS c) = show_const c
instance Const_from String cs => Const_from String (Proxy String ': cs) where
	const_from "String" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy String ': cs) where
	show_const ConstZ{} = "String"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs []
 , Proj_Consts cs (Consts_imported_by [])
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy []) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy [])
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
		 _ -> Nothing
	proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy [])
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monoid) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Show)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy [])
 = Token_Term_List_empty   (EToken meta '[Proxy Token_Type])
 | Token_Term_List_list    (EToken meta '[Proxy Token_Type]) [EToken meta ts]
 | Token_Term_List_zipWith (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
instance -- Term_fromI
 ( Const_from Name_LamVar (Consts_of_Ifaces is)
 , Inj_Const (Consts_of_Ifaces is) []
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Term_from is
 ) => Term_fromI is (Proxy []) where
	term_fromI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy [])
	 -> Term_fromT meta ctx ret is ls (Proxy [] ': rs)
	term_fromI tok ctx k =
		case tok of
		 Token_Term_List_empty tok_ty_a ->
			-- [] :: [a]
			type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
			check_kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			k (ty @[] :$ ty_a) $ TermLC $
				Fun.const list_empty
		 Token_Term_List_list tok_ty_a tok_as ->
			type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
			check_kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			go (At (Just tok_ty_a) ty_a) [] tok_as
			where
			go :: At meta '[Proxy Token_Type] (Type (Consts_of_Ifaces is) ty_a)
			   -> [TermLC ctx ty_a is '[] is]
			   -> [EToken meta is]
			   -> Either (Error_Term meta is) ret
			go ty_a as [] =
				k (ty @[] :$ unAt ty_a) $ TermLC $
				 \c -> list $ (\(TermLC a) -> a c)
					 Functor.<$> List.reverse as
			go ty_a as (tok_x:tok_xs) =
				term_from tok_x ctx $ \ty_x x ->
				check_type_is ty_a (At (Just tok_x) ty_x) $ \Refl ->
				go ty_a (x:as) tok_xs
		 Token_Term_List_zipWith tok_a2b2c ->
			-- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
			term_from tok_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
			check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
			check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
			k ( ty @[] :$ ty_a2b2c_a
			 ~> ty @[] :$ ty_a2b2c_b2c_b
			 ~> ty @[] :$ ty_a2b2c_b2c_c ) $ TermLC $
			 \c -> lam $ lam . zipWith (a2b2c c)