{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Abstract Syntax Tree.
module AST.Test where

import Test.Tasty
-- import Test.Tasty.HUnit

import qualified Data.List as List
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import qualified Data.Text as Text

import Language.Symantic.Lib.Data.Bool
import Language.Symantic.Type
import Language.Symantic.Expr as Expr

tests :: TestTree
tests = testGroup "AST" $
 [
 ]

-- * Type 'AST'
data AST
 =   AST Text [AST]
 deriving (Eq)
-- | Custom 'Show' instance a little bit more readable
-- than the automatically derived one.
instance Show AST where
	showsPrec p ast@(AST f args) =
		let n = Text.unpack f in
		case ast of
		 AST _ [] -> showString n
		 AST "->" [a] ->
				showParen (p >= prec_arrow) $
				showString ("("++n++") ") .
				showsPrec prec_arrow a
		 AST "->" [a, b] ->
				showParen (p >= prec_arrow) $
				showsPrec prec_arrow a .
				showString (" "++n++" ") .
				showsPrec prec_arrow b
		 _ ->
			showString n .
			showString "(" .
			showString (List.intercalate ", " $ show Prelude.<$> args) .
			showString ")"
		where prec_arrow = 1

-- ** Parsing utilities
from_ast0
 :: forall ty ast ex hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast (Root_of_Expr ex))
 ) => [ast]
 -> Expr_From ast ex hs ret
 -> Expr_From ast ex hs ret
from_ast0 asts k' ex ast ctx k =
	case asts of
	 [] -> k' ex ast ctx k
	 _ -> Left $ error_expr ex $
		Error_Expr_Wrong_number_of_arguments ast 0

from_ast1
 :: forall ty ast ex hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast (Root_of_Expr ex))
 ) => [ast] -> (ast -> Expr_From ast ex hs ret)
 -> Expr_From ast ex hs ret
from_ast1 asts k' ex ast ctx k =
	case asts of
	 [ast_0] -> k' ast_0 ex ast ctx k
	 _ -> Left $ error_expr ex $
		Error_Expr_Wrong_number_of_arguments ast 1

from_ast2
 :: forall ty ast ex hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast (Root_of_Expr ex))
 ) => [ast] -> (ast -> ast -> Expr_From ast ex hs ret)
 -> Expr_From ast ex hs ret
from_ast2 asts k' ex ast ctx k =
	case asts of
	 [ast_0, ast_1] -> k' ast_0 ast_1 ex ast ctx k
	 _ -> Left $ error_expr ex $
		Error_Expr_Wrong_number_of_arguments ast 2

from_ast3
 :: forall ty ast ex hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast (Root_of_Expr ex))
 ) => [ast] -> (ast -> ast -> ast -> Expr_From ast ex hs ret)
 -> Expr_From ast ex hs ret
from_ast3 asts k' ex ast ctx k =
	case asts of
	 [ast_0, ast_1, ast_2] -> k' ast_0 ast_1 ast_2 ex ast ctx k
	 _ -> Left $ error_expr ex $
		Error_Expr_Wrong_number_of_arguments ast 3

lit_from_AST
 :: forall root ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , ast ~ AST
 , Read lit
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
 -> ty lit -> [ast]
 -> Expr_From ast ex hs ret
lit_from_AST op ty_lit asts ex ast ctx k =
	case asts of
	 [AST lit []] -> lit_from op ty_lit lit ex ast ctx k
	 _ -> Left $ error_expr ex $
		Error_Expr_Wrong_number_of_arguments ast 1

op1_from_AST
 :: forall root ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , ast ~ AST
 , Eq_Type (Type_Root_of_Expr root)
 , Expr_from ast root
 , Lift_Error_Expr (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]
 -> Expr_From ast ex hs ret
op1_from_AST op ty_lit asts ex ast ctx k =
	case asts of
	 [ast_x] -> op1_from op ty_lit ast_x ex ast ctx k
	 _ -> Left $ error_expr ex $
		Error_Expr_Wrong_number_of_arguments ast 1

op2_from_AST
 :: forall root ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , ast ~ AST
 , Eq_Type (Type_Root_of_Expr root)
 , Expr_from ast root
 , Lift_Error_Expr (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]
 -> Expr_From ast ex hs ret
op2_from_AST op ty_lit asts ex ast ctx k =
	case asts of
	 [ast_x, ast_y] -> op2_from op ty_lit ast_x ast_y ex ast ctx k
	 _ -> Left $ error_expr ex $
		Error_Expr_Wrong_number_of_arguments ast 2

instance -- Type_from AST Type_Var0
 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Var0 root) root)
 ) => Type_from AST (Type_Var0 root) where
	type_from ty ast _k =
		Left $ error_type_unsupported ty ast
	 -- NOTE: no support so far.
instance -- Type_from AST Type_Var1
 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Var1 root) root)
 ) => Type_from AST (Type_Var1 root) where
	type_from ty ast _k =
		Left $ error_type_unsupported ty ast
	 -- NOTE: no support so far.
instance -- Type_from AST Type_Unit
 ( Lift_Type_Root Type_Unit root
 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Unit root) root)
 ) => Type_from AST (Type_Unit root) where
	type_from ty ast k =
		case ast of
		 AST "()" asts ->
			case asts of
			 [] -> k type_unit
			 _ -> Left $ lift_error_type $
				Error_Type_Wrong_number_of_arguments ast 0
		 _ -> Left $ error_type_unsupported ty ast
instance -- Type_from AST Type_Bool
 ( Lift_Type_Root Type_Bool root
 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Bool root) root)
 ) => Type_from AST (Type_Bool root) where
	type_from ty ast k =
		case ast of
		 AST "Bool" asts ->
			case asts of
			 [] -> k type_bool
			 _ -> Left $ lift_error_type $
				Error_Type_Wrong_number_of_arguments ast 0
		 _ -> Left $ error_type_unsupported ty ast
instance -- Type_from AST Type_Int
 ( Lift_Type_Root Type_Int root
 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Int root) root)
 ) => Type_from AST (Type_Int root) where
	type_from ty ast k =
		case ast of
		 AST "Int" asts ->
			case asts of
			 [] -> k type_int
			 _ -> Left $ lift_error_type $
				Error_Type_Wrong_number_of_arguments ast 0
		 _ -> Left $ error_type_unsupported ty ast
instance -- Type_from AST Type_Ordering
 ( Lift_Type_Root Type_Ordering root
 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Ordering root) root)
 ) => Type_from AST (Type_Ordering root) where
	type_from ty ast k =
		case ast of
		 AST "Ordering" asts ->
			case asts of
			 [] -> k type_ordering
			 _ -> Left $ lift_error_type $
				Error_Type_Wrong_number_of_arguments ast 0
		 _ -> Left $ error_type_unsupported ty ast
instance -- Type_from AST Type_Fun
 ( Eq_Type root
 , Type_from AST root
 , Lift_Type_Root (Type_Fun lam) root
 , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , Root_of_Type root ~ root
 , IBool (Is_Last_Type (Type_Fun lam root) root)
 ) => Type_from AST (Type_Fun lam root) where
	type_from ty ast k =
		case ast of
		 AST "->" asts ->
			case asts of
			 [ast_arg, ast_res] -> type_fun_from ty ast_arg ast_res k
			 _ -> Left $ lift_error_type $
				Error_Type_Wrong_number_of_arguments ast 2
		 _ -> Left $ error_type_unsupported ty ast
instance -- Type_from AST Type_Maybe
 ( Eq_Type root
 , Type_from AST root
 , Lift_Type_Root Type_Maybe root
 , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , Root_of_Type root ~ root
 , IBool (Is_Last_Type (Type_Maybe root) root)
 ) => Type_from AST (Type_Maybe root) where
	type_from ty ast k =
		case ast of
		 AST "Maybe" asts ->
			case asts of
			 [ast_a] ->
				type_from (Proxy::Proxy root) ast_a $ \ty_a ->
					k (type_maybe ty_a)
			 _ -> Left $ lift_error_type $
				Error_Type_Wrong_number_of_arguments ast 1
		 _ -> Left $ error_type_unsupported ty ast
instance -- Type_from AST Type_List
 ( Eq_Type root
 , Type_from AST root
 , Lift_Type_Root Type_List root
 , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , Root_of_Type root ~ root
 , IBool (Is_Last_Type (Type_List root) root)
 ) => Type_from AST (Type_List root) where
	type_from ty ast k =
		case ast of
		 AST "[]" asts ->
			case asts of
			 [ast_a] ->
				type_from (Proxy::Proxy root) ast_a $ \ty_a ->
					k (type_list ty_a)
			 _ -> Left $ lift_error_type $
				Error_Type_Wrong_number_of_arguments ast 1
		 _ -> Left $ error_type_unsupported ty ast

instance -- Type1_from AST Type_Bool
 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Bool root) root)
 ) => Type1_from AST (Type_Bool root)
instance -- Type1_from AST Type_Int
 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Int root) root)
 ) => Type1_from AST (Type_Int root)
instance -- Type1_from AST Type_Unit
 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Unit root) root)
 ) => Type1_from AST (Type_Unit root)
instance -- Type1_from AST Type_Ordering
 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Ordering root) root)
 ) => Type1_from AST (Type_Ordering root)
instance -- Type1_from AST Type_Var0
 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Var0 root) root)
 ) => Type1_from AST (Type_Var0 root)
instance -- Type1_from AST Type_Var1
 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , IBool (Is_Last_Type (Type_Var1 root) root)
 ) => Type1_from AST (Type_Var1 root)
instance -- Type1_from AST Type_Maybe
 ( Type_from AST root
 , Lift_Type_Root Type_Maybe root
 , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , Root_of_Type root ~ root
 , IBool (Is_Last_Type (Type_Maybe root) root)
 ) => Type1_from AST (Type_Maybe root) where
	type1_from ty ast k =
		case ast of
		 AST "Maybe" asts ->
			case asts of
			 [] -> k (Proxy::Proxy Maybe) type_maybe
			 _ -> Left $ lift_error_type $
				Error_Type_Wrong_number_of_arguments ast 0
		 _ -> Left $ error_type_unsupported ty ast
instance -- Type1_from AST Type_List
 ( Eq_Type root
 , Type_from AST root
 , Lift_Type_Root Type_List root
 , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , Root_of_Type root ~ root
 , IBool (Is_Last_Type (Type_List root) root)
 ) => Type1_from AST (Type_List root) where
	type1_from ty ast k =
		case ast of
		 AST "[]" asts ->
			case asts of
			 [] -> k (Proxy::Proxy []) type_list
			 _ -> Left $ lift_error_type $
				Error_Type_Wrong_number_of_arguments ast 0
		 _ -> Left $ error_type_unsupported ty ast
instance -- Type1_from AST Type_Fun
 ( Eq_Type root
 , Type_from AST root
 , Lift_Type_Root (Type_Fun lam) root
 , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 , Root_of_Type root ~ root
 , IBool (Is_Last_Type (Type_Fun lam root) root)
 ) => Type1_from AST (Type_Fun lam root) where
	type1_from ty ast k =
		case ast of
		 AST "->" asts ->
			case asts of
			 [ast_arg] ->
				type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
				k (Proxy::Proxy (Lambda lam h_arg)) $
					type_fun ty_arg
			 _ -> Left $ lift_error_type $
				Error_Type_Wrong_number_of_arguments ast 1
		 _ -> Left $ error_type_unsupported ty ast

instance -- Expr_from AST Expr_Bool
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Unlift_Type Type_Bool (Type_of_Expr root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Bool root) root)
 ) => Expr_from AST (Expr_Bool root) where
	expr_from ex ast =
		case ast of
		 AST "bool" asts -> lit_from_AST bool      type_bool asts ex ast
		 AST "not"  asts -> op1_from_AST Expr.not  type_bool asts ex ast
		 AST "&&"   asts -> op2_from_AST (Expr.&&) type_bool asts ex ast
		 AST "||"   asts -> op2_from_AST (Expr.||) type_bool asts ex ast
		 AST "xor"  asts -> op2_from_AST Expr.xor  type_bool asts ex ast
		 _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_If
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_If root) root)
 ) => Expr_from AST (Expr_If root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "if" asts -> from_ast3 asts if_from ex ast ctx k
		 _ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_When
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
 , Lift_Type_Root Type_Unit (Type_Root_of_Expr root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_When root) root)
 ) => Expr_from AST (Expr_When root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "when" asts -> from_ast2 asts when_from ex ast ctx k
		 _ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Int
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type_Root Type_Int (Type_Root_of_Expr root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Unlift_Type Type_Int (Type_of_Expr root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Int root) root)
 ) => Expr_from AST (Expr_Int root) where
	expr_from ex ast =
		case ast of
		 AST "int"    asts -> lit_from_AST int         type_int asts ex ast
		 AST "abs"    asts -> op1_from_AST Expr.abs    type_int asts ex ast
		 AST "negate" asts -> op1_from_AST Expr.negate type_int asts ex ast
		 AST "+"      asts -> op2_from_AST (Expr.+)    type_int asts ex ast
		 AST "-"      asts -> op2_from_AST (Expr.-)    type_int asts ex ast
		 AST "*"      asts -> op2_from_AST (Expr.*)    type_int asts ex ast
		 AST "mod"    asts -> op2_from_AST Expr.mod    type_int asts ex ast
		 _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Lambda
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
 , Lift_Error_Expr (Error_Expr_Lambda AST)       (Error_of_Expr AST root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Lambda_App lam root) root)
 ) => Expr_from AST (Expr_Lambda_App lam root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "var" asts ->
			case asts of
			 [AST name []] -> var_from name ex ast ctx k
			 _ -> Left $ error_expr ex $
				Error_Expr_Wrong_number_of_arguments ast 1
		 AST "app" asts -> from_ast2 asts app_from ex ast ctx k
		 _ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Lambda_Inline
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
 , Lift_Error_Expr (Error_Expr_Lambda AST)       (Error_of_Expr AST root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Lambda_Inline lam root) root)
 ) => Expr_from AST (Expr_Lambda_Inline lam root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "inline"     asts -> go_lam asts inline
		 AST "let_inline" asts -> go_let asts let_inline
		 _ -> Left $ error_expr_unsupported ex ast
		where
		go_lam asts
		 (lam::forall repr arg res. Sym_Lambda_Inline lam repr
		     => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
			case asts of
			 [AST name [], ast_ty_arg, ast_body] ->
				lam_from (Proxy::Proxy lam) lam name ast_ty_arg ast_body ex ast ctx k
			 _ -> Left $ error_expr ex $
				Error_Expr_Wrong_number_of_arguments ast 3
		go_let asts
		 (let_::forall repr var res. Sym_Lambda_Inline lam repr
		     => repr var -> (repr var -> repr res) -> repr res) =
			case asts of
			 [AST name [], ast_var, ast_body] ->
				let_from let_ name ast_var ast_body ex ast ctx k
			 _ -> Left $ error_expr ex $
				Error_Expr_Wrong_number_of_arguments ast 3
instance -- Expr_from AST Expr_Lambda_Val
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
 , Lift_Error_Expr (Error_Expr_Lambda AST)       (Error_of_Expr AST root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Lambda_Val lam root) root)
 ) => Expr_from AST (Expr_Lambda_Val lam root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "val"     asts -> go_lam asts val
		 AST "let_val" asts -> go_let asts let_val
		 _ -> Left $ error_expr_unsupported ex ast
		where
		go_lam asts
		 (lam::forall repr arg res. Sym_Lambda_Val lam repr
		     => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
			case asts of
			 [AST name [], ast_ty_arg, ast_body] ->
				lam_from (Proxy::Proxy lam) lam name ast_ty_arg ast_body ex ast ctx k
			 _ -> Left $ error_expr ex $
				Error_Expr_Wrong_number_of_arguments ast 3
		go_let asts
		 (let_::forall repr var res. Sym_Lambda_Val lam repr
		     => repr var -> (repr var -> repr res) -> repr res) =
			case asts of
			 [AST name [], ast_var, ast_body] ->
				let_from let_ name ast_var ast_body ex ast ctx k
			 _ -> Left $ error_expr ex $
				Error_Expr_Wrong_number_of_arguments ast 3
instance -- Expr_from AST Expr_Lambda_Lazy
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
 , Lift_Error_Expr (Error_Expr_Lambda AST)       (Error_of_Expr AST root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Lambda_Lazy lam root) root)
 ) => Expr_from AST (Expr_Lambda_Lazy lam root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "lazy"     asts -> go_lam asts lazy
		 AST "let_lazy" asts -> go_let asts let_lazy
		 _ -> Left $ error_expr_unsupported ex ast
		where
		go_lam asts
		 (lam::forall repr arg res. Sym_Lambda_Lazy lam repr
		     => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
			case asts of
			 [AST name [], ast_ty_arg, ast_body] ->
				lam_from (Proxy::Proxy lam) lam name ast_ty_arg ast_body ex ast ctx k
			 _ -> Left $ error_expr ex $
				Error_Expr_Wrong_number_of_arguments ast 3
		go_let asts
		 (let_::forall repr var res. Sym_Lambda_Lazy lam repr
		     => repr var -> (repr var -> repr res) -> repr res) =
			case asts of
			 [AST name [], ast_var, ast_body] ->
				let_from let_ name ast_var ast_body ex ast ctx k
			 _ -> Left $ error_expr ex $
				Error_Expr_Wrong_number_of_arguments ast 3
instance -- Expr_from AST Expr_Maybe
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Lift_Type   Type_Maybe     (Type_of_Expr root)
 , Unlift_Type Type_Maybe     (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Maybe lam root) root)
 ) => Expr_from AST (Expr_Maybe lam root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "maybe"   asts -> from_ast3 asts maybe_from   ex ast ctx k
		 AST "nothing" asts -> from_ast1 asts nothing_from ex ast ctx k
		 AST "just"    asts -> from_ast1 asts just_from    ex ast ctx k
		 _ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Eq
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Lift_Type Type_Bool (Type_of_Expr root)
 , Constraint_Type Eq (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Eq root) root)
 ) => Expr_from AST (Expr_Eq root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "==" asts -> from_ast2 asts eq_from ex ast ctx k
		 _ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Ord
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Lift_Type Type_Ordering (Type_of_Expr root)
 , Constraint_Type Ord (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Ord root) root)
 ) => Expr_from AST (Expr_Ord root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "compare" asts -> from_ast2 asts compare_from ex ast ctx k
		 _ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_List
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Lift_Type   Type_List      (Type_of_Expr root)
 , Unlift_Type Type_List      (Type_of_Expr root)
 , Lift_Type   Type_Bool      (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_List lam root) root)
 ) => Expr_from AST (Expr_List lam root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "[]"          asts -> from_ast1 asts list_empty_from  ex ast ctx k
		 AST ":"           asts -> from_ast2 asts list_cons_from   ex ast ctx k
		 AST "list_filter" asts -> from_ast2 asts list_filter_from ex ast ctx k
		 AST "list"        asts ->
			case asts of
			 ast_ty_a:asts' -> list_from ast_ty_a asts' ex ast ctx k
			 _ -> Left $ error_expr ex $
				Error_Expr_Wrong_number_of_arguments ast 1
		 _ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Map
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Lift_Type   Type_Map       (Type_of_Expr root)
 , Unlift_Type Type_Map       (Type_of_Expr root)
 , Lift_Type   Type_List      (Type_of_Expr root)
 , Unlift_Type Type_List      (Type_of_Expr root)
 , Lift_Type   Type_Tuple2    (Type_of_Expr root)
 , Unlift_Type Type_Tuple2    (Type_of_Expr root)
 , Constraint_Type Ord (Type_Root_of_Expr root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Map lam root) root)
 ) => Expr_from AST (Expr_Map lam root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "map_from_list" asts -> from_ast1 asts map_from_list_from ex ast ctx k
		 AST "map_map" asts -> from_ast2 asts map_map_from ex ast ctx k
		 _ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Functor
 ( Eq_Type (Type_Root_of_Expr root)
 , Type_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Unlift_Type1 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Constraint_Type1 Functor (Type_Root_of_Expr root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Functor lam root) root)
 ) => Expr_from AST (Expr_Functor lam root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "fmap" asts -> from_ast2 asts fmap_from ex ast ctx k
		 AST "<$>"  asts -> from_ast2 asts fmap_from ex ast ctx k
		 _ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Applicative
 ( Eq_Type (Type_Root_of_Expr root)
 , Type1_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Eq_Type1 (Type_Root_of_Expr root)
 , Unlift_Type1 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Constraint_Type1 Applicative (Type_Root_of_Expr root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Applicative lam root) root)
 ) => Expr_from AST (Expr_Applicative lam root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "pure" asts -> from_ast2 asts pure_from     ex ast ctx k
		 AST "<*>"  asts -> from_ast2 asts ltstargt_from ex ast ctx k
		 _ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Traversable
 ( Eq_Type (Type_Root_of_Expr root)
 , Type1_from AST (Type_Root_of_Expr root)
 , Expr_from AST root
 , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Eq_Type1 (Type_Root_of_Expr root)
 , Unlift_Type1 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 , Constraint_Type1 Applicative (Type_Root_of_Expr root)
 , Constraint_Type1 Traversable (Type_Root_of_Expr root)
 , Root_of_Expr root ~ root
 , IBool (Is_Last_Expr (Expr_Traversable lam root) root)
 ) => Expr_from AST (Expr_Traversable lam root) where
	expr_from ex ast ctx k =
		case ast of
		 AST "traverse"  asts -> from_ast2 asts traverse_from ex ast ctx k
		 _ -> Left $ error_expr_unsupported ex ast