{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Compiling.Term where

import Data.Proxy (Proxy(..))
import Data.Text (Text)
import qualified Data.Function as Fun
import Data.Monoid ((<>))
import qualified Data.Text as Text
import Data.Type.Equality
import GHC.Exts (Constraint)
import Prelude hiding (not)

import Language.Symantic.Lib.Data.Type.List
import Language.Symantic.Typing
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Type 'Term'
-- | 'Term_of_LamCtx' applied on a 'LamCtx_Type'.
data Term is h
 =   Term
 (forall term. ( Sym_of_Ifaces is term
               , Sym_Lambda term
               ) => term (UnProxy h))

-- ** Type 'Term_of_LamCtx'
-- | A data type embedding a universal quantification
-- over an interpreter @term@
-- and qualified by the symantics of a term.
--
-- Moreover the term is abstracted by a 'LamCtx_Term'
-- built top-down at parsing time
-- to build a /Higher-Order Abstract Syntax/ (HOAS)
-- for /lambda abstractions/ ('lam').
--
-- This data type is used to keep a parsed term polymorphic enough
-- to stay interpretable by different interpreters.
--
-- * @(@'Sym_of_Ifaces'@ is term)@
-- is needed to be able to use a term
-- out of a @(@'Term_of_LamCtx'@ (@'Root_of_Expr'@ is))@
-- into a @(@'Term_of_LamCtx'@ is)@,
-- which happens when a symantic method includes a polymorphic type
-- and thus calls: 'term_from'@ (Proxy::Proxy (@'Root_of_Expr'@ is))@.
--
-- * @'@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
-- are needed to be able to write the instance:
-- @(@'Term_fromR'@ is ls (i ': rs) ast)@.
--
-- * @(@'Sym_Lambda'@ term)@
-- is needed to be able to parse partially applied functions
-- (when their type is knowable).
data Term_of_LamCtx ctx h is ls rs
 =   Term_of_LamCtx
 (forall term. ( Sym_of_Ifaces is term
               , Sym_of_Ifaces ls term
               , Sym_of_Ifaces rs term
               , Sym_Lambda term
               ) => LamCtx_Term term ctx -> term (UnProxy h))

-- ** Type 'ETerm'
-- | Existential 'Term', with its 'Type'.
data ETerm is
 = forall h. ETerm
   (Type (Consts_of_Ifaces is) 'KiTerm h)
   (Term is h)

-- | Like 'term_from' but for a term with empty /lambda context/.
root_term_from
 :: Term_from is ast
 => ast -> Either (Error_Term is ast) (ETerm is)
root_term_from ast =
	term_from ast LamCtx_TypeZ $ \ty (Term_of_LamCtx te) ->
	Right $ ETerm ty $ Term $ te LamCtx_TermZ

-- * Type 'Term_from'
-- | Convenient type synonym wrapping 'Term_fromR'
-- to initiate its recursion.
class Term_from is ast where
	term_from :: Term_fromT ast ctx ret is '[] is
instance
 ( AST ast
 , Eq (Lexem ast)
 , Term_fromR is '[] is ast
 ) => Term_from is ast where
	term_from ast ctx k =
		case replace_var (ast_lexem ast) ctx k of
		 Left Error_Term_unsupported -> term_fromR ast ctx k
		 x -> x
		where
		replace_var :: forall lc ret.
		      Lexem ast
		   -> LamCtx_Type is (Lexem ast) lc
		   -> ( forall h.
		         Type (Consts_of_Ifaces is) 'KiTerm h
		      -> Term_of_LamCtx lc h is '[] is
		      -> Either (Error_Term is ast) ret )
		   -> Either (Error_Term is ast) ret
		replace_var name lc k' =
			case lc of
			 LamCtx_TypeZ -> Left $ Error_Term_unsupported
			 LamCtx_TypeS n ty _ | n == name ->
				k' ty $ Term_of_LamCtx $ \(te `LamCtx_TermS` _) -> te
			 LamCtx_TypeS _n _ty lc' ->
				replace_var name lc' $ \ty (Term_of_LamCtx te::Term_of_LamCtx lc' h is '[] is) ->
				k' ty $ Term_of_LamCtx $ \(_ `LamCtx_TermS` c) -> te c

-- ** Type 'Term_fromT'
-- | Convenient type synonym defining a term parser.
type Term_fromT ast ctx ret is ls rs
 = ast
 -> LamCtx_Type is (Lexem ast) ctx
 -- ^ The bound variables in scope and their types:
 -- built top-down in the heterogeneous list @ctx@,
 -- from the closest including /lambda abstraction/ to the farest.
 -> ( forall h.
       Type (Consts_of_Ifaces is) 'KiTerm h
    -> Term_of_LamCtx ctx h is ls rs
    -> Either (Error_Term is ast) ret )
 -- ^ The accumulating continuation called bottom-up.
 -> Either (Error_Term is ast) ret

-- ** Class 'Term_fromR'
-- | Intermediate type class to construct an instance of 'Term_from'
-- from many instances of 'Term_fromI', one for each item of @is@.
--
-- * @is@: starting  list of /term constants/.
-- * @ls@: done      list of /term constants/.
-- * @rs@: remaining list of /term constants/.
class AST ast => Term_fromR (is::[*]) (ls::[*]) (rs::[*]) ast where
	term_fromR :: Term_fromT ast ctx ret is ls rs
	term_fromR ast _ctx _k =
		Left $ Error_Term_unknown $
		At (Just ast) $ ast_lexem ast

-- | Test whether @i@ handles the work of 'Term_from' or not,
-- or recurse on @rs@, preserving the starting list of /term constants/,
-- and keeping a list of those done to construct 'Term_of_LamCtx'.
instance
 ( Term_fromI is i ast
 , Term_fromR is (i ': ls) rs ast
 ) => Term_fromR is ls (i ': rs) ast where
	term_fromR ast ctx k =
		case term_fromI ast ctx $ \ty (Term_of_LamCtx te
		 ::Term_of_LamCtx ctx h is ls (i ': rs)) ->
			k ty (Term_of_LamCtx te) of
		 Left Error_Term_unsupported ->
			term_fromR ast ctx $ \ty (Term_of_LamCtx te
			 ::Term_of_LamCtx ctx h is (i ': ls) rs) ->
				k ty (Term_of_LamCtx te
				 ::Term_of_LamCtx ctx h is ls (i ': rs))
		 x -> x
-- | End the recursion.
instance AST ast => Term_fromR is ls '[] ast

-- * Type family 'Sym_of_Ifaces'
type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
	Sym_of_Ifaces '[] term = ()
	Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)

-- ** Type family 'Sym_of_Iface'
type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda

-- ** Class 'Term_fromI'
-- | Handle the work of 'Term_from' for a given /instance/ @i@,
-- that is: maybe it handles the given /instance/,
-- and if so, maybe the 'Constraint' holds.
class AST ast => Term_fromI (is::[*]) (i:: *) ast where
	term_fromI :: Term_fromT ast ctx ret is ls (i ': rs)
	term_fromI _ast _ctx _k =
		Left $ Error_Term_unsupported
instance -- (->)
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Proj_Const (Consts_of_Ifaces is) (Proxy (->))
 , Const_from (Lexem ast) (Consts_of_Ifaces is)
 , Term_from is ast
 ) => Term_fromI is (Proxy (->)) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "\\" ->
			from_ast3 ast $ \ast_name ast_ty_arg ast_body ->
				either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
				type_from ast_ty_arg $ \ty_arg -> Right $
				check_kind ast SKiTerm (At (Just ast) ty_arg) $ \Refl ->
				term_from ast_body
				 (LamCtx_TypeS (ast_lexem ast_name) ty_arg ctx) $
				 \ty_res (Term_of_LamCtx res) ->
				k (ty_arg ~> ty_res) $ Term_of_LamCtx $
				 \c -> lam $ \arg ->
					res (arg `LamCtx_TermS` c)
		 " " ->
			from_ast2 ast $ \ast_lam ast_arg_actual ->
				term_from ast_lam ctx $ \ty_lam (Term_of_LamCtx lam_) ->
				term_from ast_arg_actual ctx $ \ty_arg_actual (Term_of_LamCtx arg_actual) ->
				case ty_lam of
				 TyConst co_fun :$ ty_arg :$ ty_res
				  | Just Refl <- proj_const co_fun (Proxy::Proxy (->)) ->
					check_type
					 (At (Just ast_lam) ty_arg)
					 (At (Just ast_arg_actual) ty_arg_actual) $ \Refl ->
					k ty_res $ Term_of_LamCtx $
					 \c -> lam_ c .$ arg_actual c
				 _ -> Left $ Error_Term_not_applicable $
					At (Just ast) $ EType ty_lam
		 "let" ->
			from_ast3 ast $ \ast_name ast_var ast_body ->
				term_from ast_var ctx $ \ty_var (Term_of_LamCtx var) ->
				term_from ast_body (LamCtx_TypeS (ast_lexem ast_name) ty_var ctx) $
				 \ty_res (Term_of_LamCtx res) ->
				k ty_res $ Term_of_LamCtx $
				 \c -> let_ (var c) $ \arg -> res (arg `LamCtx_TermS` c)
		 _ -> Left $ Error_Term_unsupported
instance -- Applicative
 AST ast =>
 Term_fromI is (Proxy Applicative) ast

check_type
 :: AST ast
 => At ast (Type (Consts_of_Ifaces is) ki_x x)
 -> At ast (Type (Consts_of_Ifaces is) ki_y y)
 -> ((x :~: y) -> Either (Error_Term is ast) ret)
 -> Either (Error_Term is ast) ret
check_type (At at_x x) (At at_y y) k =
	case eq_type x y of
	 Just Refl -> k Refl
	 Nothing -> Left $ Error_Term_Type_mismatch
		 (At at_x $ EType x)
		 (At at_y $ EType y)

check_kind
 :: AST ast
 => ast -> SKind ki
 -> At ast (Type (Consts_of_Ifaces is) ki_x x)
 -> ((ki :~: ki_x) -> Either (Error_Term is ast) ret)
 -> Either (Error_Term is ast) ret
check_kind ast ki (At at_ty ty) k =
	let ki_ty = kind_of ty in
	case testEquality ki ki_ty of
	 Just Refl -> k Refl
	 Nothing -> Left $ Error_Term_Typing $
		At (Just ast) $
		Error_Type_Kind_mismatch
		 (At Nothing $ EKind SKiTerm)
		 (At at_ty $ EKind ki_ty)

check_constraint
 :: (AST ast, Proj_Con (Consts_of_Ifaces is))
 => At ast (Type (Consts_of_Ifaces is) 'KiCon q)
 -> (Con (UnProxy q) -> Either (Error_Term is ast) ret)
 -> Either (Error_Term is ast) ret
check_constraint (At at_q q) k =
	case proj_con q of
	 Just Con -> k Con
	 Nothing -> Left $ Error_Term_Constraint_not_deductible $
		At at_q $ KType q

-- * Type 'Error_Term'
data Error_Term (is::[*]) ast
 =   Error_Term_unknown (At ast (Lexem ast))
 |   Error_Term_unsupported
 |   Error_Term_Syntax (Error_Syntax ast)
 |   Error_Term_Constraint_not_deductible (At ast (KType (Consts_of_Ifaces is) 'KiCon))
 |   Error_Term_Typing (At ast (Error_Type (Consts_of_Ifaces is) ast))
 |   Error_Term_Type_mismatch (At ast (EType (Consts_of_Ifaces is)))
                              (At ast (EType (Consts_of_Ifaces is)))
 |   Error_Term_not_applicable (At ast (EType (Consts_of_Ifaces is)))
deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Term is ast)
deriving instance (Show ast, Show (Lexem ast), Show_Const (Consts_of_Ifaces is)) => Show (Error_Term is ast)

instance Lift_Error_Syntax (Error_Term is) where
	lift_error_syntax = Error_Term_Syntax

-- * Type 'Consts_of_Ifaces'
type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)

-- ** Type family 'Consts_of_IfaceR'
type family Consts_of_IfaceR (is::[*]) where
	Consts_of_IfaceR '[] = '[]
	Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is

-- ** Type family 'Consts_of_Iface'
type family   Consts_of_Iface (i:: *) :: [*]
type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
type instance Consts_of_Iface (Proxy Bool) = Proxy Bool ': Consts_imported_by Bool
type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
type instance Consts_of_Iface (Proxy Eq)   = Proxy Eq   ': Consts_imported_by Eq
type instance Consts_of_Iface (Proxy Ord)  = Proxy Ord  ': Consts_imported_by Ord

-- * Type 'LamCtx_Type'
-- | GADT for a typing context,
-- accumulating an @item@ at each lambda;
-- used to accumulate object-types (in 'Expr_From')
-- or host-terms (in 'HostI')
-- associated with the 'LamVar's in scope.
data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
	LamCtx_TypeZ :: LamCtx_Type is name '[]
	LamCtx_TypeS :: name
	             -> Type (Consts_of_Ifaces is) 'KiTerm h
	             -> LamCtx_Type is name hs
	             -> LamCtx_Type is name (h ': hs)
infixr 5 `LamCtx_TypeS`

-- ** Type 'LamVarName'
type LamVarName = Text

-- * Type 'LamCtx_Term'
data LamCtx_Term (term:: * -> *) (ctx::[*]) where
	LamCtx_TermZ :: LamCtx_Term term '[]
	LamCtx_TermS :: term (UnProxy h)
	             -> LamCtx_Term term hs
	             -> LamCtx_Term term (h ': hs)
infixr 5 `LamCtx_TermS`

-- * Class 'Sym_Lambda'
class Sym_Lambda term where
	-- | /Lambda abstraction/.
	lam :: (term arg -> term res) -> term ((->) arg res)
	default lam :: Trans t term
	 => (t term arg -> t term res)
	 -> t term ((->) arg res)
	lam f = trans_lift $ lam $ trans_apply . f . trans_lift
	
	-- | /Lambda application/.
	(.$) :: term ((->) arg res) -> term arg -> term res
	default (.$) :: Trans t term
	 => t term ((->) arg res) -> t term arg -> t term res
	(.$) f x = trans_lift (trans_apply f .$ trans_apply x)
	
	-- | Convenient 'lam' and '.$' wrapper.
	let_ :: term var -> (term var -> term res) -> term res
	let_ x y = lam y .$ x
	
	id :: term a -> term a
	id a = lam Fun.id .$ a
	
	const :: term a -> term b -> term a
	const a b = lam (lam . Fun.const) .$ a .$ b
	
	-- | /Lambda composition/.
	(#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
	(#) f g = lam $ \a -> f .$ (g .$ a)
	
	flip :: term (a -> b -> c) -> term (b -> a -> c)
	flip f = lam $ \b -> lam $ \a -> f .$ a .$ b

infixl 0 .$
infixr 9 #

instance Sym_Lambda HostI where
	lam f = HostI (unHostI . f . HostI)
	(.$)  = (<*>)
instance Sym_Lambda TextI where
	lam f = TextI $ \p v ->
		let p' = Precedence 1 in
		let x = "x" <> Text.pack (show v) in
		paren p p' $ "\\" <> x <> " -> "
		 <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
	-- (.$) = textI_infix "$" (Precedence 0)
	(.$) (TextI a1) (TextI a2) =
		TextI $ \p v ->
			let p' = precedence_App in
			paren p p' $ a1 p' v <> " " <> a2 p' v
	let_ e in_ =
		TextI $ \p v ->
			let p' = Precedence 2 in
			let x = "x" <> Text.pack (show v) in
			paren p p' $ "let" <> " " <> x <> " = "
			 <> unTextI e (Precedence 0) (succ v) <> " in "
			 <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
	(#)   = textI_infix "." (Precedence 9)
	id    = textI_app1 "id"
	const = textI_app2 "const"
	flip  = textI_app1 "flip"
instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
	lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
		where lam_f = lam f
	(.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)


{-
class IProxy (ty::ki) where
	proxy :: Proxy ty
	proxy = (Proxy::Proxy ty)
instance IProxy ty

-}

{-
-- * 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_Term_Type_mismatch'.
check_type0_family
 :: forall ast is tf root ty h ret.
 ( root ~ Root_of_Expr is
 , ty ~ Type_Root_of_Expr is
 , Type0_Family tf ty
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy tf -> Proxy is -> 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 is ast ty k =
	case type0_family tf ty of
	 Just t -> k t
	 Nothing -> Left $ error_expr is $
		Error_Term_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast

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

-- | Parsing utility to check that two 'Type1' are equal,
-- or raise 'Error_Term_Type_mismatch'.
check_type1_eq
 :: forall ast is root ty h1 h2 a1 a2 ret.
 ( root ~ Root_of_Expr is
 , ty ~ Type_Root_of_Expr is
 , Type1_Eq ty
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy is -> 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 is ast h1 h2 k =
	case h1 `type1_eq` h2 of
	 Just Refl -> k Refl
	 Nothing -> Left $ error_expr is $
		Error_Term_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_Term_Constraint_missing'.
check_type0_constraint
 :: forall ast is c root ty h ret.
 ( root ~ Root_of_Expr is
 , ty ~ Type_Root_of_Expr is
 , Type0_Constraint c ty
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy is -> 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 is c ast ty k =
	case type0_constraint c ty of
	 Just Dict -> k Dict
	 Nothing -> Left $ error_expr is $
		Error_Term_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_Term_Constraint_missing'.
check_type1_constraint
 :: forall ast is c root ty h a ret.
 ( root ~ Root_of_Expr is
 , ty ~ Type_Root_of_Expr is
 , Type1_Constraint c ty
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy is -> 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 is c ast ty k =
	case type1_constraint c ty of
	 Just Dict -> k Dict
	 Nothing -> Left $ error_expr is $
		Error_Term_Constraint_missing ast
		 (Exists_Type0 ty)

-- | Parsing utility to check that the given type is at least a 'Type1'
-- or raise 'Error_Term_Type_mismatch'.
check_type1
 :: forall ast is root ty h ret.
 ( root ~ Root_of_Expr is
 , ty ~ Type_Root_of_Expr is
 , Type1_Unlift (Type_of_Expr root)
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy is -> 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 is ast ty k =
	(`fromMaybe` type1_unlift (unType_Root ty) (Just . k)) $
	Left $ error_expr is $
	Error_Term_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)
                                  (Term root))
root_expr_from _ex ast =
	expr_from (Proxy::Proxy root) ast
	 LamCtxZ $ \ty (Term_of_LamCtx term) ->
	Right $ Exists_Type0_and_Repr ty $
		Term $ term LamCtxZ

-- | Parse a literal.
lit_from
 :: forall ty lit is ast hs ret.
 ( ty ~ Type_Root_of_Expr is
 , Read lit
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast (Root_of_Expr is))
 ) => (forall term. Sym_of_Iface is term => lit -> term lit)
 -> ty lit -> Text
 -> Term_fromT ast is hs ret
lit_from lit ty_lit toread is ast _ctx k =
	case read_safe toread of
	 Left err -> Left $ error_expr is $ Error_Term_Read err ast
	 Right (i::lit) -> k ty_lit $ Term_of_LamCtx $ const $ lit i

-- | Parse a unary class operator.
class_op1_from
 :: forall root ty cl is ast hs ret.
 ( ty ~ Type_Root_of_Expr is
 , root ~ Root_of_Expr is
 , Type0_Eq ty
 , Expr_From ast root
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Type0_Constraint cl ty
 ) => (forall lit term. (cl lit, Sym_of_Iface is term) => term lit -> term lit)
 -> Proxy cl -> ast
 -> Term_fromT ast is hs ret
class_op1_from op cl ast_x is _ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
	check_type0_constraint is cl ast_x ty_x $ \Dict ->
	k ty_x $ Term_of_LamCtx (op . x)

-- | Parse a binary class operator.
class_op2_from
 :: forall root ty cl is ast hs ret.
 ( ty ~ Type_Root_of_Expr is
 , root ~ Root_of_Expr is
 , Type0_Eq ty
 , Expr_From ast root
 , Type0_Constraint cl ty
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall lit term. (cl lit, Sym_of_Iface is term) => term lit -> term lit -> term lit)
 -> Proxy cl -> ast -> ast
 -> Term_fromT ast is hs ret
class_op2_from op cl ast_x ast_y is ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
	expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
	check_type0_constraint is cl ast_x ty_x $ \Dict ->
	check_type0_constraint is cl ast_y ty_y $ \Dict ->
	check_type0_eq is ast ty_x ty_y $ \Refl ->
	k ty_x $ Term_of_LamCtx $
	 \c -> x c `op` y c

-- | Parse a binary class operator, partially applied.
class_op2_from1
 :: forall root ty cl is ast hs ret.
 ( ty ~ Type_Root_of_Expr is
 , root ~ Root_of_Expr is
 , Type0_Eq ty
 , Type0_Constraint cl ty
 , Type0_Lift Type_Fun (Type_of_Expr root)
 , Expr_From ast root
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall lit term. (cl lit, Sym_of_Iface is term) => term lit -> term lit -> term lit)
 -> Proxy cl -> ast
 -> Term_fromT ast is hs ret
class_op2_from1 op cl ast_x is _ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
	check_type0_constraint is cl ast_x ty_x $ \Dict ->
	k (type_fun ty_x ty_x) $ Term_of_LamCtx $
	 \c -> lam $ \y -> x c `op` y

-- | Parse a unary operator.
op1_from
 :: forall root ty lit is ast hs ret.
 ( ty ~ Type_Root_of_Expr is
 , root ~ Root_of_Expr is
 , Type0_Eq ty
 , Expr_From ast root
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall term. Sym_of_Iface is term => term lit -> term lit)
 -> ty lit -> ast
 -> Term_fromT ast is hs ret
op1_from op ty_lit ast_x is ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
	check_type0_eq is ast ty_lit ty_x $ \Refl ->
	k ty_x $ Term_of_LamCtx (op . x)

-- | Parse a unary operator, partially applied.
op1_from0
 :: forall root ty lit is ast hs ret.
 ( ty ~ Type_Root_of_Expr is
 , root ~ Root_of_Expr is
 , Type0_Eq ty
 , Type0_Lift Type_Fun (Type_of_Expr root)
 , Expr_From ast root
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall term. Sym_of_Iface is term => term lit -> term lit)
 -> ty lit
 -> Term_fromT ast is hs ret
op1_from0 op ty_lit _ex _ast _ctx k =
	k (type_fun ty_lit ty_lit) $ Term_of_LamCtx $
	 \_c -> lam op

-- | Parse a binary operator.
op2_from
 :: forall root ty lit is ast hs ret.
 ( ty ~ Type_Root_of_Expr is
 , root ~ Root_of_Expr is
 , Type0_Eq ty
 , Expr_From ast root
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall term. Sym_of_Iface is term => term lit -> term lit -> term lit)
 -> ty lit -> ast -> ast
 -> Term_fromT ast is hs ret
op2_from op ty_lit ast_x ast_y is ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
	expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
	check_type0_eq is ast ty_lit ty_x $ \Refl ->
	check_type0_eq is ast ty_lit ty_y $ \Refl ->
	k ty_x $ Term_of_LamCtx $
	 \c -> x c `op` y c

-- | Parse a binary operator, partially applied.
op2_from1
 :: forall root ty lit is ast hs ret.
 ( ty ~ Type_Root_of_Expr is
 , root ~ Root_of_Expr is
 , Type0_Eq ty
 , Type0_Lift Type_Fun (Type_of_Expr root)
 , Expr_From ast root
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall term. Sym_of_Iface is term => term lit -> term lit -> term lit)
 -> ty lit -> ast
 -> Term_fromT ast is hs ret
op2_from1 op ty_lit ast_x is ast ctx k =
	expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
	check_type0_eq is ast ty_lit ty_x $ \Refl ->
		k (type_fun ty_x ty_x) $ Term_of_LamCtx $
		 \c -> lam $ \y -> x c `op` y

-- | Parse a binary operator, partially applied.
op2_from0
 :: forall root ty lit is ast hs ret.
 ( ty ~ Type_Root_of_Expr is
 , root ~ Root_of_Expr is
 , Type0_Eq ty
 , Type0_Lift Type_Fun (Type_of_Expr root)
 , Expr_From ast root
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall term. Sym_of_Iface is term => term lit -> term lit -> term lit)
 -> ty lit
 -> Term_fromT ast is hs ret
op2_from0 op ty_lit _ex _ast _ctx k =
	k (type_fun ty_lit $ type_fun ty_lit ty_lit) $ Term_of_LamCtx $
	 \_c -> lam $ \x -> lam $ \y -> x `op` y
-}