{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Expr.From where

import Data.Maybe (fromMaybe)
import Data.Monoid
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Type.Equality ((:~:)(Refl))
import GHC.Prim (Constraint)

import Language.Symantic.Type
import Language.Symantic.Expr.Root
import Language.Symantic.Expr.Alt
import Language.Symantic.Expr.Error
import Language.Symantic.Trans.Common
import Language.Symantic.Repr

-- * Class 'Expr_From'
-- | Parse given @ast@ into
-- a 'Type_Root_of_Expr' and
-- a 'Forall_Repr_with_Context',
-- or return an 'Error_of_Expr'.
class Expr_From ast (ex:: *) where
	expr_from :: ExprFrom ast ex hs ret
instance -- Expr_From
 ( Expr_From ast (ex (Expr_Root ex))
 , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
 ) => Expr_From ast (Expr_Root ex) where
	expr_from _ex ctx ast k =
		expr_from (Proxy::Proxy (ex (Expr_Root ex)))
		 ctx ast $ \ty (Forall_Repr_with_Context repr) ->
		k ty (Forall_Repr_with_Context repr)
instance -- Expr_From
 ( Expr_From ast (curr root)
 , Expr_From ast (next root)
 , Root_of_Expr (curr root) ~ root
 , Root_of_Expr (next root) ~ root
 , Error_Expr_Unlift (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
                                 (Type_Root_of_Expr root) ast)
                     (Error_of_Expr ast root)
 ) => Expr_From ast (Expr_Alt curr next root) where
	expr_from _ex ctx ast k =
		case expr_from (Proxy::Proxy (curr root)) ctx ast $
		 \ty (Forall_Repr_with_Context repr) ->
			Right $ k ty (Forall_Repr_with_Context repr) of
		 Right ret -> ret
		 Left err ->
			case error_expr_unlift err of
			 Just (Error_Expr_Unsupported_here _
			  :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
			                (Type_Root_of_Expr root) ast) ->
				expr_from (Proxy::Proxy (next root)) ctx ast $
				 \ty (Forall_Repr_with_Context repr) ->
				k ty (Forall_Repr_with_Context repr)
			 _ -> Left err

-- ** Type 'ExprFrom'
-- | Convenient type synonym defining a parser.
type ExprFrom ast ex hs ret
 = Proxy ex
 -- ^ Select the 'Expr_From' instance.
 -> ast
 -- ^ The input data to parse.
 -> Lambda_Context (Lambda_Var (Type_Root_of_Expr ex)) hs
 -- ^ The bound variables in scope and their types:
 -- held in the heterogeneous list @hs@,
 -- from the closest including lambda abstraction to the farest.
 -> ( forall h
    .  Type_Root_of_Expr ex h
    -> Forall_Repr_with_Context ex hs h
    -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
 -- ^ The accumulating continuation.
 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret

-- ** Type 'Lambda_Context'
-- | GADT for a typing context,
-- accumulating an @item@ at each lambda;
-- used to accumulate object-types (in 'Expr_From')
-- or host-terms (in 'Repr_Host')
-- associated with the 'Lambda_Var's in scope.
data Lambda_Context :: (* -> *) -> [*] -> * where
	Lambda_Context_Empty :: Lambda_Context item '[]
	Lambda_Context_Next  :: item h
	                     -> Lambda_Context item hs
	                     -> Lambda_Context item (h ': hs)
infixr 5 `Lambda_Context_Next`

-- ** Type 'Lambda_Var'
-- | Join a name and a type.
--
-- This data type is used to handle lambda variables by name
-- (instead of DeBruijn indices for instance).
data Lambda_Var ty h
 =   Lambda_Var Lambda_Var_Name (ty h)
type Lambda_Var_Name = Text

-- ** Type 'Forall_Repr_with_Context'
-- | A data type embedding a universal quantification
-- over an interpreter @repr@
-- and qualified by the symantics of an expression.
--
-- Moreover the expression is abstracted by a 'Lambda_Context'
-- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
-- for lambda abstractions.
--
-- This data type is used to keep a parsed expression polymorphic enough
-- to stay interpretable by different interpreters.
--
-- NOTE: 'Sym_of_Expr'@ ex repr@
-- is needed to be able to use symantic methods of the parsed expression
-- into a 'Forall_Repr_with_Context'@ ex@.
--
-- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
-- is needed to be able to use an expression
-- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
-- into a 'Forall_Repr_with_Context'@ ex@,
-- which happens when a symantic method includes a polymorphic type
-- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
--
-- NOTE: 'Sym_Lambda_Lam repr@
-- is needed to be able to parse partially applied functions
-- (when their type is knowable).
data Forall_Repr_with_Context ex hs h
 =   Forall_Repr_with_Context
 (   forall repr. ( Sym_of_Expr ex repr
                  , Sym_of_Expr (Root_of_Expr ex) repr
                  , Sym_Lambda_Lam repr
                  ) => Lambda_Context repr hs -> repr h )

-- ** Type 'Forall_Repr'
-- | 'Forall_Repr_with_Context' applied on a 'Lambda_Context'.
data Forall_Repr ex h
 =   Forall_Repr
 { unForall_Repr :: forall repr
                 .  ( Sym_of_Expr ex repr
                    , Sym_of_Expr (Root_of_Expr ex) repr
                    , Sym_Lambda_Lam repr )
                 => repr h }

-- * Class 'Sym_Lambda_Lam'
class Sym_Lambda_Lam repr where
	-- | /Lambda abstraction/.
	lam :: (repr arg -> repr res) -> repr ((->) arg res)
	default lam :: Trans t repr
	 => (t repr arg -> t repr res) -> t repr ((->) arg res)
	lam f = trans_lift $ lam $ trans_apply . f . trans_lift
instance Sym_Lambda_Lam Repr_Host where
	lam f = Repr_Host (unRepr_Host . f . Repr_Host)
instance Sym_Lambda_Lam Repr_Text where
	lam f =
		Repr_Text $ \p v ->
			let p' = Precedence 1 in
			let x = "x" <> Text.pack (show v) in
			paren p p' $ "\\" <> x <> " -> "
			 <> unRepr_Text (f (Repr_Text $ \_p _v -> x)) p' (succ v)
instance (Sym_Lambda_Lam r1, Sym_Lambda_Lam r2) => Sym_Lambda_Lam (Repr_Dup r1 r2) where
	lam f = repr_dup_1 (lam f) `Repr_Dup` repr_dup_2 (lam f)

-- ** Type family 'Sym_of_Expr'
-- | The symantic of an expression.
type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
type instance Sym_of_Expr (Expr_Root ex) repr
 =            Sym_of_Expr (ex (Expr_Root ex)) repr
type instance Sym_of_Expr (Expr_Alt curr next root) repr
 = ( Sym_of_Expr (curr root) repr
   , Sym_of_Expr (next root) repr
   )

-- * Checks

-- | Parsing utility to check that the type resulting
-- from the application of a given type family to a given type
-- is within the type stack,
-- or raise 'Error_Expr_Type_mismatch'.
check_type0_family
 :: forall ast ex tf root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type0_Family tf ty
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy tf -> Proxy ex -> ast -> ty h
 -> (ty (Host_of_Type0_Family tf h) -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type0_family tf ex ast ty k =
	case type0_family tf ty of
	 Just t -> k t
	 Nothing -> Left $ error_expr ex $
		Error_Expr_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast

-- | Parsing utility to check that two types are equal,
-- or raise 'Error_Expr_Type_mismatch'.
check_type0_eq
 :: forall ast ex root ty x y ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type0_Eq ty
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy ex -> ast -> ty x -> ty y
 -> (x :~: y -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type0_eq ex ast x y k =
	case x `type0_eq` y of
	 Just Refl -> k Refl
	 Nothing -> Left $ error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type0 x)
		 (Exists_Type0 y)

-- | Parsing utility to check that two 'Type1' are equal,
-- or raise 'Error_Expr_Type_mismatch'.
check_type1_eq
 :: forall ast ex root ty h1 h2 a1 a2 ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type1_Eq ty
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> ast -> ty (h1 a1) -> ty (h2 a2)
 -> (h1 :~: h2 -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type1_eq ex ast h1 h2 k =
	case h1 `type1_eq` h2 of
	 Just Refl -> k Refl
	 Nothing -> Left $ error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type0 h1)
		 (Exists_Type0 h2)

-- | Parsing utility to check that a 'Type0' or higher
-- is an instance of a given 'Constraint',
-- or raise 'Error_Expr_Constraint_missing'.
check_type0_constraint
 :: forall ast ex c root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type0_Constraint c ty
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> Proxy c -> ast -> ty h
 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type0_constraint ex c ast ty k =
	case type0_constraint c ty of
	 Just Dict -> k Dict
	 Nothing -> Left $ error_expr ex $
		Error_Expr_Constraint_missing ast
		 {-(Exists_Dict c)-}
		 -- FIXME: not easy to report the constraint
		 -- and still support 'Eq' and 'Show' deriving.
		 (Exists_Type0 ty)

-- | Parsing utility to check that a 'Type1' or higher
-- is an instance of a given 'Constraint',
-- or raise 'Error_Expr_Constraint_missing'.
check_type1_constraint
 :: forall ast ex c root ty h a ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type1_Constraint c ty
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy ex -> Proxy c -> ast -> ty (h a)
 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type1_constraint ex c ast ty k =
	case type1_constraint c ty of
	 Just Dict -> k Dict
	 Nothing -> Left $ error_expr ex $
		Error_Expr_Constraint_missing ast
		 (Exists_Type0 ty)

-- | Parsing utility to check that the given type is at least a 'Type1'
-- or raise 'Error_Expr_Type_mismatch'.
check_type1
 :: forall ast ex root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy ex -> ast -> ty h
 -> (forall (t1:: *).
     ( Type1 t1 ty h
     , Type1_Lift t1 ty (Type_Var0 :|: Type_Var1 :|: Type_of_Expr root)
     ) -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type1 ex ast ty k =
	(`fromMaybe` type1_unlift (unType_Root ty) (Just . k)) $
	Left $
		error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type0 (type_var1 SZero (type_var0 SZero)
		 :: ty (Var1 Var0)))
		 (Exists_Type0 ty)

-- * Parsers

-- | Like 'expr_from' but for a root expression.
root_expr_from
 :: forall ast root.
 ( Expr_From ast root
 , Root_of_Expr root ~ root
 ) => Proxy root -> ast
 -> Either (Error_of_Expr ast root)
           (Exists_Type0_and_Repr (Type_Root_of_Expr root)
                                  (Forall_Repr root))
root_expr_from _ex ast =
	expr_from (Proxy::Proxy root) ast
	 Lambda_Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
		Right $ Exists_Type0_and_Repr ty $
			Forall_Repr $ repr Lambda_Context_Empty

-- | Parse a literal.
lit_from
 :: forall ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , Read lit
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast (Root_of_Expr ex))
 ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
 -> ty lit -> Text
 -> ExprFrom ast ex hs ret
lit_from lit ty_lit toread ex ast _ctx k =
	case read_safe toread of
	 Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
	 Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i

-- | Parse a unary class operator.
class_op1_from
 :: forall root ty cl ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , Type0_Eq ty
 , Expr_From ast root
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Type0_Constraint cl ty
 ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit)
 -> Proxy cl -> ast
 -> ExprFrom ast ex hs ret
class_op1_from op cl ast_x ex _ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
	check_type0_constraint ex cl ast_x ty_x $ \Dict ->
	k ty_x $ Forall_Repr_with_Context (op . x)

-- | Parse a binary class operator.
class_op2_from
 :: forall root ty cl ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , Type0_Eq ty
 , Expr_From ast root
 , Type0_Constraint cl ty
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit -> repr lit)
 -> Proxy cl -> ast -> ast
 -> ExprFrom ast ex hs ret
class_op2_from op cl ast_x ast_y ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
	expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
	check_type0_constraint ex cl ast_x ty_x $ \Dict ->
	check_type0_constraint ex cl ast_y ty_y $ \Dict ->
	check_type0_eq ex ast ty_x ty_y $ \Refl ->
	k ty_x $ Forall_Repr_with_Context $
	 \c -> x c `op` y c

-- | Parse a binary class operator, partially applied.
class_op2_from1
 :: forall root ty cl ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , Type0_Eq ty
 , Type0_Constraint cl ty
 , Type0_Lift Type_Fun (Type_of_Expr root)
 , Expr_From ast root
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit -> repr lit)
 -> Proxy cl -> ast
 -> ExprFrom ast ex hs ret
class_op2_from1 op cl ast_x ex _ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
	check_type0_constraint ex cl ast_x ty_x $ \Dict ->
	k (type_fun ty_x ty_x) $ Forall_Repr_with_Context $
	 \c -> lam $ \y -> x c `op` y

-- | Parse a unary operator.
op1_from
 :: forall root ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , Type0_Eq ty
 , Expr_From ast root
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
 -> ty lit -> ast
 -> ExprFrom ast ex hs ret
op1_from op ty_lit ast_x ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
	check_type0_eq ex ast ty_lit ty_x $ \Refl ->
	k ty_x $ Forall_Repr_with_Context (op . x)

-- | Parse a unary operator, partially applied.
op1_from0
 :: forall root ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , Type0_Eq ty
 , Type0_Lift Type_Fun (Type_of_Expr root)
 , Expr_From ast root
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
 -> ty lit
 -> ExprFrom ast ex hs ret
op1_from0 op ty_lit _ex _ast _ctx k =
	k (type_fun ty_lit ty_lit) $ Forall_Repr_with_Context $
	 \_c -> lam op

-- | Parse a binary operator.
op2_from
 :: forall root ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , Type0_Eq ty
 , Expr_From ast root
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
 -> ty lit -> ast -> ast
 -> ExprFrom ast ex hs ret
op2_from op ty_lit ast_x ast_y ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
	expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
	check_type0_eq ex ast ty_lit ty_x $ \Refl ->
	check_type0_eq ex ast ty_lit ty_y $ \Refl ->
	k ty_x $ Forall_Repr_with_Context $
	 \c -> x c `op` y c

-- | Parse a binary operator, partially applied.
op2_from1
 :: forall root ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , Type0_Eq ty
 , Type0_Lift Type_Fun (Type_of_Expr root)
 , Expr_From ast root
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
 -> ty lit -> ast
 -> ExprFrom ast ex hs ret
op2_from1 op ty_lit ast_x ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
	check_type0_eq ex ast ty_lit ty_x $ \Refl ->
		k (type_fun ty_x ty_x) $ Forall_Repr_with_Context $
		 \c -> lam $ \y -> x c `op` y

-- | Parse a binary operator, partially applied.
op2_from0
 :: forall root ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , Type0_Eq ty
 , Type0_Lift Type_Fun (Type_of_Expr root)
 , Expr_From ast root
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
 -> ty lit
 -> ExprFrom ast ex hs ret
op2_from0 op ty_lit _ex _ast _ctx k =
	k (type_fun ty_lit $ type_fun ty_lit ty_lit) $ Forall_Repr_with_Context $
	 \_c -> lam $ \x -> lam $ \y -> x `op` y