{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Hcompta.Expr.Lit where

-- import Control.Applicative (Applicative(..))
-- import Control.Monad (Monad(..))
-- import Control.Monad.Trans.State.Strict as ST
-- import Data.Bool
-- import Data.Either (Either(..))
-- import Data.Eq (Eq(..))
-- import Data.Function (($), (.))
-- import Data.Functor (Functor(..))
-- import Data.Maybe (Maybe(..))
-- import Data.Monoid ((<>))
-- import Data.Proxy (Proxy(..))
-- import Data.String (IsString(..))
-- import Data.Text (Text)
-- import qualified Data.Text as Text
import Data.Text.Buildable (Buildable(..))
-- import Data.Type.Equality ((:~:)(Refl))
-- import GHC.Exts (IsList(..))
-- import Prelude (undefined)
-- import Text.Read (Read, reads)
import Text.Show (Show(..))

-- import Hcompta.Lib.Control.Monad
-- import qualified Hcompta.Lib.Control.Monad.Classes as MC
-- import qualified Hcompta.Lib.Data.Text.Buildable as Build

import Hcompta.Expr.Dup
-- import Hcompta.Expr.Fun

-- * Class 'Expr_Lit'

-- | /Tagless-final symantics/ to inject a meta-level term
-- into and object-level expression.
class Expr_Lit repr where
	lit :: (Buildable a, Show a) => a -> repr a

instance -- Expr_Lit Dup
 ( Expr_Lit r1
 , Expr_Lit r2
 ) => Expr_Lit (Dup r1 r2) where
	lit x = lit x `Dup` lit x

{-
-- * Type 'Type_Lit'

-- | GADT for boolean type:
--
-- * singleton (bijective mapping between Haskell type @h@ and the GADT's terms),
-- * and extensible (through @next@).
data Type_Lit lit (next:: * -> *) h where
	Type_Lit      :: Type_Lit lit next lit
	Type_Lit_Next :: next h -> Type_Lit lit next h
type Type_Fun_Lit lit repr next = Type_Fun repr (Type_Lit lit next)
type Type_Fun_Lit_End lit repr = Type_Fun_Lit lit repr Type_Lit_End

instance -- Type_Eq
 Type_Eq next =>
 Type_Eq (Type_Lit lit next) where
	type_eq Type_Lit
	        Type_Lit = Just Refl
	type_eq (Type_Lit_Next x)
	        (Type_Lit_Next y) = x `type_eq` y
	type_eq _ _ = Nothing
instance -- Type_from Tree
 ( Type_from Tree next
 , Buildable (Type_Lit_Name lit)
 ) => Type_from Tree (Type_Lit lit next) where
	type_from (Tree raw_lit []) k
	 | raw_lit == Build.text (Type_Lit_Name::Type_Lit_Name lit)
	 = k Type_Lit
	type_from raw k = type_from raw $ k . Type_Lit_Next
instance -- From_Type Text
 ( From_Type Text next
 , Buildable (Type_Lit_Name lit)
 ) => From_Type Text (Type_Lit lit next) where
	from_type Type_Lit = Build.text (Type_Lit_Name::Type_Lit_Name lit)
	from_type (Type_Lit_Next t) = from_type t
instance -- Expr_from Tree
 ( Expr_Lit repr
 , Type_from Tree next
 , Expr_from Tree repr next (Type_Fun_Lit lit repr next)
 , Read lit
 , Show lit
 , Buildable lit
 , Buildable (Type_Lit_Name lit)
 ) => Expr_from Tree repr (Type_Lit lit next) (Type_Fun_Lit lit repr next) where
	expr_from _pty _pvar _ctx (Tree lit_name [Tree raw_lit []]) k
	 | lit_name == Build.text (Type_Lit_Name::Type_Lit_Name lit) = do
		l <- repr_lit_read raw_lit
		k (Type_Fun_Next Type_Lit) $ \_c -> lit l
	expr_from _pty pvar ctx raw k =
		expr_from (Proxy::Proxy next) pvar ctx raw k

repr_lit_read :: Read a => Text -> Either Error_Type a
repr_lit_read t =
	let s = Text.unpack t in
	case reads s of
	 [(a, "")] -> Right a
	 _         -> Left $ "Read error: " <> s

instance Monad m => Expr_Lit (ST.StateT s m) where
	lit = return
instance Monad m => Expr_Lit (MC.WriterT w m) where
	lit = return

-- * Type 'Type_Lit_Name'

-- | Data type to get a name from a Haskell type-level literal type.
data Type_Lit_Name lit = Type_Lit_Name
instance Buildable (Type_Lit_Name Bool) where
	build _ = "Bool"

-- * Type 'Type_Lit_End'

-- | Data type to finalize a type at 'Type_Fun_Lit'.
data Type_Lit_End h where
	Type_Lit_End :: Type_Lit_End ()

instance -- Type_Eq
 Type_Eq Type_Lit_End where
	type_eq Type_Lit_End
	        Type_Lit_End = Just Refl
instance -- Type_from Tree
 Type_from Tree Type_Lit_End where
	type_from _ k = k Type_Lit_End
instance -- Expr_from Tree
 Buildable (Type_Lit_Name lit)
 => Expr_from Tree repr Type_Lit_End (Type_Fun_Lit lit repr Type_Lit_End) where
	expr_from _pty _pvar _ctx raw _k =
		Left $ "Error: invalid Type_Lit: "
		 <> Build.string (Type_Lit_Name::Type_Lit_Name lit) <> ": "
		 <> show raw
-}

{-
class Literal from to where
	literal :: from -> to
instance Applicative repr => Literal a (repr a) where
	literal = pure
instance (Applicative repr, IsString a) => Literal String (repr a) where
	literal = pure . fromString
instance (Applicative repr, IsString a) => Literal [String] (repr [a]) where
	literal = pure . (fromString <$>)
instance Applicative repr => Literal [a] (repr [a]) where
	literal = pure
instance Monad repr => Literal [repr a] (repr [a]) where
	literal = sequence
instance Literal a a where
	literal a = a
-}

{-
-- * Class 'List'
class Monad repr => List repr where
	list :: [repr a] -> repr [a]
	list = sequence
instance Monad m => List (ST.StateT s m)
instance Monad m => List (WriterT w m)

instance (Monad m, Monad (repr m)) => List (repr (m:: * -> *)) where
	list = sequence
-}
-- instance IsList ([a])

{-
-- Orphan instances for overloading
instance (IsList a, List (repr m)) => IsList (repr (m:: * -> *) [a]) where
	type Item (repr m [a]) = repr m a
	fromList = list
	toList = undefined
-}


{- NOTE: conflicts with specific instance in Data.DList
instance (IsList a, List repr) => IsList (repr [a]) where
	type Item (repr [a]) = repr a
	fromList = list
	toList = undefined
-}
{-
instance (Monad repr, IsString a) => IsString (repr a) where
	fromString = return . fromString
-}