{-# 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 as G
import Language.Symantic.Lib.Function (a0, b1, c2)
import Language.Symantic.Lib.MonoFunctor (Element)

-- * Class 'Sym_List'
type instance Sym [] = 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 NameTyOf [] where
        nameTyOf _c = [] `Mod` "[]"
instance FixityOf []
instance ClassInstancesFor [] where
        proveConstraintFor _ (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 _ (tq@(TyConst _ _ q) :$ 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 (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
 , SymInj ss []
 ) => Gram_Term_AtomsFor src ss g [] where
        g_term_atomsFor =
         [ rule "teList_list" $
                between (symbol "[") (symbol "]") listG
         , rule "teList_empty" $
                G.source $
                (\src -> BinTree0 $ Token_Term $ TermAVT teList_empty `setSource` src)
                 <$ symbol "["
                 <* symbol "]"
         ]
                where
                listG :: CF g (AST_Term src ss)
                listG = rule "list" $
                        G.source $
                        (\a mb src ->
                                case mb of
                                 Just b  -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a) b
                                 Nothing ->
                                        BinTree2
                                         (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a)
                                         (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_empty))
                         <$> g_term
                         <*> option Nothing (Just <$ symbol "," <*> listG)
instance (Source src, SymInj ss []) => ModuleFor src ss [] where
        moduleFor = ["List"] `moduleWhere`
         [ "[]"      := teList_empty
         , "zipWith" := teList_zipWith
         , ":" `withInfixR` 5 := teList_cons
         ]

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

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

teList_cons :: Source src => SymInj 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 => SymInj 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