Language/Symantic/AST/Test.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE Rank2Types #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE UndecidableInstances #-}
  10 -- | Abstract Syntax Tree.
  11 module AST.Test where
  12
  13 import Test.Tasty
  14 -- import Test.Tasty.HUnit
  15
  16 import qualified Data.List as List
  17 import Data.Proxy (Proxy(..))
  18 import Data.Text (Text)
  19 import qualified Data.Text as Text
  20
  21 import Language.Symantic.Lib.Data.Bool
  22 import Language.Symantic.Type
  23 import Language.Symantic.Expr as Expr
  24
  25 tests :: TestTree
  26 tests = testGroup "AST" $
  27  [
  28  ]
  29
  30 -- * Type 'AST'
  31 data AST
  32  =   AST Text [AST]
  33  deriving (Eq)
  34 -- | Custom 'Show' instance a little bit more readable
  35 -- than the automatically derived one.
  36 instance Show AST where
  37         showsPrec p ast@(AST f args) =
  38                 let n = Text.unpack f in
  39                 case ast of
  40                  AST _ [] -> showString n
  41                  AST "->" [a] ->
  42                                 showParen (p >= prec_arrow) $
  43                                 showString ("("++n++") ") .
  44                                 showsPrec prec_arrow a
  45                  AST "->" [a, b] ->
  46                                 showParen (p >= prec_arrow) $
  47                                 showsPrec prec_arrow a .
  48                                 showString (" "++n++" ") .
  49                                 showsPrec prec_arrow b
  50                  _ ->
  51                         showString n .
  52                         showString "(" .
  53                         showString (List.intercalate ", " $ show Prelude.<$> args) .
  54                         showString ")"
  55                 where prec_arrow = 1
  56
  57 -- ** Parsing utilities
  58 from_ast0
  59  :: forall ty ast ex hs ret.
  60  ( ty ~ Type_Root_of_Expr ex
  61  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  62                    (Error_of_Expr ast (Root_of_Expr ex))
  63  ) => [ast]
  64  -> Expr_From ast ex hs ret
  65  -> Expr_From ast ex hs ret
  66 from_ast0 asts k' ex ast ctx k =
  67         case asts of
  68          [] -> k' ex ast ctx k
  69          _ -> Left $ error_expr ex $
  70                 Error_Expr_Wrong_number_of_arguments ast 0
  71
  72 from_ast1
  73  :: forall ty ast ex hs ret.
  74  ( ty ~ Type_Root_of_Expr ex
  75  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  76                    (Error_of_Expr ast (Root_of_Expr ex))
  77  ) => [ast] -> (ast -> Expr_From ast ex hs ret)
  78  -> Expr_From ast ex hs ret
  79 from_ast1 asts k' ex ast ctx k =
  80         case asts of
  81          [ast_0] -> k' ast_0 ex ast ctx k
  82          _ -> Left $ error_expr ex $
  83                 Error_Expr_Wrong_number_of_arguments ast 1
  84
  85 from_ast2
  86  :: forall ty ast ex hs ret.
  87  ( ty ~ Type_Root_of_Expr ex
  88  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  89                    (Error_of_Expr ast (Root_of_Expr ex))
  90  ) => [ast] -> (ast -> ast -> Expr_From ast ex hs ret)
  91  -> Expr_From ast ex hs ret
  92 from_ast2 asts k' ex ast ctx k =
  93         case asts of
  94          [ast_0, ast_1] -> k' ast_0 ast_1 ex ast ctx k
  95          _ -> Left $ error_expr ex $
  96                 Error_Expr_Wrong_number_of_arguments ast 2
  97
  98 from_ast3
  99  :: forall ty ast ex hs ret.
 100  ( ty ~ Type_Root_of_Expr ex
 101  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 102                    (Error_of_Expr ast (Root_of_Expr ex))
 103  ) => [ast] -> (ast -> ast -> ast -> Expr_From ast ex hs ret)
 104  -> Expr_From ast ex hs ret
 105 from_ast3 asts k' ex ast ctx k =
 106         case asts of
 107          [ast_0, ast_1, ast_2] -> k' ast_0 ast_1 ast_2 ex ast ctx k
 108          _ -> Left $ error_expr ex $
 109                 Error_Expr_Wrong_number_of_arguments ast 3
 110
 111 lit_from_AST
 112  :: forall root ty lit ex ast hs ret.
 113  ( ty ~ Type_Root_of_Expr ex
 114  , root ~ Root_of_Expr ex
 115  , ast ~ AST
 116  , Read lit
 117  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 118                    (Error_of_Expr ast root)
 119  ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
 120  -> ty lit -> [ast]
 121  -> Expr_From ast ex hs ret
 122 lit_from_AST op ty_lit asts ex ast ctx k =
 123         case asts of
 124          [AST lit []] -> lit_from op ty_lit lit ex ast ctx k
 125          _ -> Left $ error_expr ex $
 126                 Error_Expr_Wrong_number_of_arguments ast 1
 127
 128 op1_from_AST
 129  :: forall root ty lit ex ast hs ret.
 130  ( ty ~ Type_Root_of_Expr ex
 131  , root ~ Root_of_Expr ex
 132  , ast ~ AST
 133  , Eq_Type (Type_Root_of_Expr root)
 134  , Expr_from ast root
 135  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 136                    (Error_of_Expr ast root)
 137  , Root_of_Expr root ~ root
 138  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
 139  -> ty lit -> [ast]
 140  -> Expr_From ast ex hs ret
 141 op1_from_AST op ty_lit asts ex ast ctx k =
 142         case asts of
 143          [ast_x] -> op1_from op ty_lit ast_x ex ast ctx k
 144          _ -> Left $ error_expr ex $
 145                 Error_Expr_Wrong_number_of_arguments ast 1
 146
 147 op2_from_AST
 148  :: forall root ty lit ex ast hs ret.
 149  ( ty ~ Type_Root_of_Expr ex
 150  , root ~ Root_of_Expr ex
 151  , ast ~ AST
 152  , Eq_Type (Type_Root_of_Expr root)
 153  , Expr_from ast root
 154  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 155                    (Error_of_Expr ast root)
 156  , Root_of_Expr root ~ root
 157  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
 158  -> ty lit -> [ast]
 159  -> Expr_From ast ex hs ret
 160 op2_from_AST op ty_lit asts ex ast ctx k =
 161         case asts of
 162          [ast_x, ast_y] -> op2_from op ty_lit ast_x ast_y ex ast ctx k
 163          _ -> Left $ error_expr ex $
 164                 Error_Expr_Wrong_number_of_arguments ast 2
 165
 166 instance -- Type_from AST Type_Var0
 167  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 168  , Implicit_HBool (Is_Last_Type (Type_Var0 root) root)
 169  ) => Type_from AST (Type_Var0 root) where
 170         type_from ty ast _k =
 171                 Left $ error_type_unsupported ty ast
 172          -- NOTE: no support so far.
 173 instance -- Type_from AST Type_Var1
 174  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 175  , Implicit_HBool (Is_Last_Type (Type_Var1 root) root)
 176  ) => Type_from AST (Type_Var1 root) where
 177         type_from ty ast _k =
 178                 Left $ error_type_unsupported ty ast
 179          -- NOTE: no support so far.
 180 instance -- Type_from AST Type_Unit
 181  ( Lift_Type_Root Type_Unit root
 182  , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 183  , Implicit_HBool (Is_Last_Type (Type_Unit root) root)
 184  ) => Type_from AST (Type_Unit root) where
 185         type_from ty ast k =
 186                 case ast of
 187                  AST "()" asts ->
 188                         case asts of
 189                          [] -> k type_unit
 190                          _ -> Left $ lift_error_type $
 191                                 Error_Type_Wrong_number_of_arguments ast 0
 192                  _ -> Left $ error_type_unsupported ty ast
 193 instance -- Type_from AST Type_Bool
 194  ( Lift_Type_Root Type_Bool root
 195  , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 196  , Implicit_HBool (Is_Last_Type (Type_Bool root) root)
 197  ) => Type_from AST (Type_Bool root) where
 198         type_from ty ast k =
 199                 case ast of
 200                  AST "Bool" asts ->
 201                         case asts of
 202                          [] -> k type_bool
 203                          _ -> Left $ lift_error_type $
 204                                 Error_Type_Wrong_number_of_arguments ast 0
 205                  _ -> Left $ error_type_unsupported ty ast
 206 instance -- Type_from AST Type_Int
 207  ( Lift_Type_Root Type_Int root
 208  , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 209  , Implicit_HBool (Is_Last_Type (Type_Int root) root)
 210  ) => Type_from AST (Type_Int root) where
 211         type_from ty ast k =
 212                 case ast of
 213                  AST "Int" asts ->
 214                         case asts of
 215                          [] -> k type_int
 216                          _ -> Left $ lift_error_type $
 217                                 Error_Type_Wrong_number_of_arguments ast 0
 218                  _ -> Left $ error_type_unsupported ty ast
 219 instance -- Type_from AST Type_Ordering
 220  ( Lift_Type_Root Type_Ordering root
 221  , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 222  , Implicit_HBool (Is_Last_Type (Type_Ordering root) root)
 223  ) => Type_from AST (Type_Ordering root) where
 224         type_from ty ast k =
 225                 case ast of
 226                  AST "Ordering" asts ->
 227                         case asts of
 228                          [] -> k type_ordering
 229                          _ -> Left $ lift_error_type $
 230                                 Error_Type_Wrong_number_of_arguments ast 0
 231                  _ -> Left $ error_type_unsupported ty ast
 232 instance -- Type_from AST Type_Fun
 233  ( Eq_Type root
 234  , Type_from AST root
 235  , Lift_Type_Root (Type_Fun lam) root
 236  , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 237  , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 238  , Root_of_Type root ~ root
 239  , Implicit_HBool (Is_Last_Type (Type_Fun lam root) root)
 240  ) => Type_from AST (Type_Fun lam root) where
 241         type_from ty ast k =
 242                 case ast of
 243                  AST "->" asts ->
 244                         case asts of
 245                          [ast_arg, ast_res] -> type_fun_from ty ast_arg ast_res k
 246                          _ -> Left $ lift_error_type $
 247                                 Error_Type_Wrong_number_of_arguments ast 2
 248                  _ -> Left $ error_type_unsupported ty ast
 249 instance -- Type_from AST Type_Maybe
 250  ( Eq_Type root
 251  , Type_from AST root
 252  , Lift_Type_Root Type_Maybe root
 253  , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 254  , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 255  , Root_of_Type root ~ root
 256  , Implicit_HBool (Is_Last_Type (Type_Maybe root) root)
 257  ) => Type_from AST (Type_Maybe root) where
 258         type_from ty ast k =
 259                 case ast of
 260                  AST "Maybe" asts ->
 261                         case asts of
 262                          [ast_a] ->
 263                                 type_from (Proxy::Proxy root) ast_a $ \ty_a ->
 264                                         k (type_maybe ty_a)
 265                          _ -> Left $ lift_error_type $
 266                                 Error_Type_Wrong_number_of_arguments ast 1
 267                  _ -> Left $ error_type_unsupported ty ast
 268 instance -- Type_from AST Type_List
 269  ( Eq_Type root
 270  , Type_from AST root
 271  , Lift_Type_Root Type_List root
 272  , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 273  , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 274  , Root_of_Type root ~ root
 275  , Implicit_HBool (Is_Last_Type (Type_List root) root)
 276  ) => Type_from AST (Type_List root) where
 277         type_from ty ast k =
 278                 case ast of
 279                  AST "[]" asts ->
 280                         case asts of
 281                          [ast_a] ->
 282                                 type_from (Proxy::Proxy root) ast_a $ \ty_a ->
 283                                         k (type_list ty_a)
 284                          _ -> Left $ lift_error_type $
 285                                 Error_Type_Wrong_number_of_arguments ast 1
 286                  _ -> Left $ error_type_unsupported ty ast
 287
 288 instance -- Type1_from AST Type_Bool
 289  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 290  , Implicit_HBool (Is_Last_Type (Type_Bool root) root)
 291  ) => Type1_from AST (Type_Bool root)
 292 instance -- Type1_from AST Type_Int
 293  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 294  , Implicit_HBool (Is_Last_Type (Type_Int root) root)
 295  ) => Type1_from AST (Type_Int root)
 296 instance -- Type1_from AST Type_Unit
 297  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 298  , Implicit_HBool (Is_Last_Type (Type_Unit root) root)
 299  ) => Type1_from AST (Type_Unit root)
 300 instance -- Type1_from AST Type_Ordering
 301  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 302  , Implicit_HBool (Is_Last_Type (Type_Ordering root) root)
 303  ) => Type1_from AST (Type_Ordering root)
 304 instance -- Type1_from AST Type_Var0
 305  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 306  , Implicit_HBool (Is_Last_Type (Type_Var0 root) root)
 307  ) => Type1_from AST (Type_Var0 root)
 308 instance -- Type1_from AST Type_Var1
 309  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 310  , Implicit_HBool (Is_Last_Type (Type_Var1 root) root)
 311  ) => Type1_from AST (Type_Var1 root)
 312 instance -- Type1_from AST Type_Maybe
 313  ( Type_from AST root
 314  , Lift_Type_Root Type_Maybe root
 315  , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 316  , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 317  , Root_of_Type root ~ root
 318  , Implicit_HBool (Is_Last_Type (Type_Maybe root) root)
 319  ) => Type1_from AST (Type_Maybe root) where
 320         type1_from ty ast k =
 321                 case ast of
 322                  AST "Maybe" asts ->
 323                         case asts of
 324                          [] -> k (Proxy::Proxy Maybe) type_maybe
 325                          _ -> Left $ lift_error_type $
 326                                 Error_Type_Wrong_number_of_arguments ast 0
 327                  _ -> Left $ error_type_unsupported ty ast
 328 instance -- Type1_from AST Type_List
 329  ( Eq_Type root
 330  , Type_from AST root
 331  , Lift_Type_Root Type_List root
 332  , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 333  , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 334  , Root_of_Type root ~ root
 335  , Implicit_HBool (Is_Last_Type (Type_List root) root)
 336  ) => Type1_from AST (Type_List root) where
 337         type1_from ty ast k =
 338                 case ast of
 339                  AST "[]" asts ->
 340                         case asts of
 341                          [] -> k (Proxy::Proxy []) type_list
 342                          _ -> Left $ lift_error_type $
 343                                 Error_Type_Wrong_number_of_arguments ast 0
 344                  _ -> Left $ error_type_unsupported ty ast
 345 instance -- Type1_from AST Type_Fun
 346  ( Eq_Type root
 347  , Type_from AST root
 348  , Lift_Type_Root (Type_Fun lam) root
 349  , Lift_Error_Type   (Error_Type AST) (Error_of_Type AST root)
 350  , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
 351  , Root_of_Type root ~ root
 352  , Implicit_HBool (Is_Last_Type (Type_Fun lam root) root)
 353  ) => Type1_from AST (Type_Fun lam root) where
 354         type1_from ty ast k =
 355                 case ast of
 356                  AST "->" asts ->
 357                         case asts of
 358                          [ast_arg] ->
 359                                 type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
 360                                 k (Proxy::Proxy (Lambda lam h_arg)) $
 361                                         type_fun ty_arg
 362                          _ -> Left $ lift_error_type $
 363                                 Error_Type_Wrong_number_of_arguments ast 1
 364                  _ -> Left $ error_type_unsupported ty ast
 365
 366 instance -- Expr_from AST Expr_Bool
 367  ( Eq_Type (Type_Root_of_Expr root)
 368  , Type_from AST (Type_Root_of_Expr root)
 369  , Expr_from AST root
 370  , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
 371  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 372  , Unlift_Type Type_Bool (Type_of_Expr root)
 373  , Root_of_Expr root ~ root
 374  , Implicit_HBool (Is_Last_Expr (Expr_Bool root) root)
 375  ) => Expr_from AST (Expr_Bool root) where
 376         expr_from ex ast =
 377                 case ast of
 378                  AST "bool" asts -> lit_from_AST bool      type_bool asts ex ast
 379                  AST "not"  asts -> op1_from_AST Expr.not  type_bool asts ex ast
 380                  AST "&&"   asts -> op2_from_AST (Expr.&&) type_bool asts ex ast
 381                  AST "||"   asts -> op2_from_AST (Expr.||) type_bool asts ex ast
 382                  AST "xor"  asts -> op2_from_AST Expr.xor  type_bool asts ex ast
 383                  _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
 384 instance -- Expr_from AST Expr_If
 385  ( Eq_Type (Type_Root_of_Expr root)
 386  , Type_from AST (Type_Root_of_Expr root)
 387  , Expr_from AST root
 388  , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
 389  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 390  , Root_of_Expr root ~ root
 391  , Implicit_HBool (Is_Last_Expr (Expr_If root) root)
 392  ) => Expr_from AST (Expr_If root) where
 393         expr_from ex ast ctx k =
 394                 case ast of
 395                  AST "if" asts -> from_ast3 asts if_from ex ast ctx k
 396                  _ -> Left $ error_expr_unsupported ex ast
 397 instance -- Expr_from AST Expr_When
 398  ( Eq_Type (Type_Root_of_Expr root)
 399  , Type_from AST (Type_Root_of_Expr root)
 400  , Expr_from AST root
 401  , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
 402  , Lift_Type_Root Type_Unit (Type_Root_of_Expr root)
 403  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 404  , Root_of_Expr root ~ root
 405  , Implicit_HBool (Is_Last_Expr (Expr_When root) root)
 406  ) => Expr_from AST (Expr_When root) where
 407         expr_from ex ast ctx k =
 408                 case ast of
 409                  AST "when" asts -> from_ast2 asts when_from ex ast ctx k
 410                  _ -> Left $ error_expr_unsupported ex ast
 411 instance -- Expr_from AST Expr_Int
 412  ( Eq_Type (Type_Root_of_Expr root)
 413  , Type_from AST (Type_Root_of_Expr root)
 414  , Expr_from AST root
 415  , Lift_Type_Root Type_Int (Type_Root_of_Expr root)
 416  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 417  , Unlift_Type Type_Int (Type_of_Expr root)
 418  , Root_of_Expr root ~ root
 419  , Implicit_HBool (Is_Last_Expr (Expr_Int root) root)
 420  ) => Expr_from AST (Expr_Int root) where
 421         expr_from ex ast =
 422                 case ast of
 423                  AST "int"    asts -> lit_from_AST int         type_int asts ex ast
 424                  AST "abs"    asts -> op1_from_AST Expr.abs    type_int asts ex ast
 425                  AST "negate" asts -> op1_from_AST Expr.negate type_int asts ex ast
 426                  AST "+"      asts -> op2_from_AST (Expr.+)    type_int asts ex ast
 427                  AST "-"      asts -> op2_from_AST (Expr.-)    type_int asts ex ast
 428                  AST "*"      asts -> op2_from_AST (Expr.*)    type_int asts ex ast
 429                  AST "mod"    asts -> op2_from_AST Expr.mod    type_int asts ex ast
 430                  _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
 431 instance -- Expr_from AST Expr_Lambda
 432  ( Eq_Type (Type_Root_of_Expr root)
 433  , Type_from AST (Type_Root_of_Expr root)
 434  , Expr_from AST root
 435  , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
 436  , Lift_Error_Expr (Error_Expr_Lambda AST)       (Error_of_Expr AST root)
 437  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 438  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 439  , Root_of_Expr root ~ root
 440  , Implicit_HBool (Is_Last_Expr (Expr_Lambda_App lam root) root)
 441  ) => Expr_from AST (Expr_Lambda_App lam root) where
 442         expr_from ex ast ctx k =
 443                 case ast of
 444                  AST "var" asts ->
 445                         case asts of
 446                          [AST name []] -> var_from name ex ast ctx k
 447                          _ -> Left $ error_expr ex $
 448                                 Error_Expr_Wrong_number_of_arguments ast 1
 449                  AST "app" asts -> from_ast2 asts app_from ex ast ctx k
 450                  _ -> Left $ error_expr_unsupported ex ast
 451 instance -- Expr_from AST Expr_Lambda_Inline
 452  ( Eq_Type (Type_Root_of_Expr root)
 453  , Type_from AST (Type_Root_of_Expr root)
 454  , Expr_from AST root
 455  , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
 456  , Lift_Error_Expr (Error_Expr_Lambda AST)       (Error_of_Expr AST root)
 457  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 458  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 459  , Root_of_Expr root ~ root
 460  , Implicit_HBool (Is_Last_Expr (Expr_Lambda_Inline lam root) root)
 461  ) => Expr_from AST (Expr_Lambda_Inline lam root) where
 462         expr_from ex ast ctx k =
 463                 case ast of
 464                  AST "inline"     asts -> go_lam asts inline
 465                  AST "let_inline" asts -> go_let asts let_inline
 466                  _ -> Left $ error_expr_unsupported ex ast
 467                 where
 468                 go_lam asts
 469                  (lam::forall repr arg res. Sym_Lambda_Inline lam repr
 470                      => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
 471                         case asts of
 472                          [AST name [], ast_ty_arg, ast_body] ->
 473                                 lam_from (Proxy::Proxy lam) lam name ast_ty_arg ast_body ex ast ctx k
 474                          _ -> Left $ error_expr ex $
 475                                 Error_Expr_Wrong_number_of_arguments ast 3
 476                 go_let asts
 477                  (let_::forall repr var res. Sym_Lambda_Inline lam repr
 478                      => repr var -> (repr var -> repr res) -> repr res) =
 479                         case asts of
 480                          [AST name [], ast_var, ast_body] ->
 481                                 let_from let_ name ast_var ast_body ex ast ctx k
 482                          _ -> Left $ error_expr ex $
 483                                 Error_Expr_Wrong_number_of_arguments ast 3
 484 instance -- Expr_from AST Expr_Lambda_Val
 485  ( Eq_Type (Type_Root_of_Expr root)
 486  , Type_from AST (Type_Root_of_Expr root)
 487  , Expr_from AST root
 488  , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
 489  , Lift_Error_Expr (Error_Expr_Lambda AST)       (Error_of_Expr AST root)
 490  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 491  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 492  , Root_of_Expr root ~ root
 493  , Implicit_HBool (Is_Last_Expr (Expr_Lambda_Val lam root) root)
 494  ) => Expr_from AST (Expr_Lambda_Val lam root) where
 495         expr_from ex ast ctx k =
 496                 case ast of
 497                  AST "val"     asts -> go_lam asts val
 498                  AST "let_val" asts -> go_let asts let_val
 499                  _ -> Left $ error_expr_unsupported ex ast
 500                 where
 501                 go_lam asts
 502                  (lam::forall repr arg res. Sym_Lambda_Val lam repr
 503                      => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
 504                         case asts of
 505                          [AST name [], ast_ty_arg, ast_body] ->
 506                                 lam_from (Proxy::Proxy lam) lam name ast_ty_arg ast_body ex ast ctx k
 507                          _ -> Left $ error_expr ex $
 508                                 Error_Expr_Wrong_number_of_arguments ast 3
 509                 go_let asts
 510                  (let_::forall repr var res. Sym_Lambda_Val lam repr
 511                      => repr var -> (repr var -> repr res) -> repr res) =
 512                         case asts of
 513                          [AST name [], ast_var, ast_body] ->
 514                                 let_from let_ name ast_var ast_body ex ast ctx k
 515                          _ -> Left $ error_expr ex $
 516                                 Error_Expr_Wrong_number_of_arguments ast 3
 517 instance -- Expr_from AST Expr_Lambda_Lazy
 518  ( Eq_Type (Type_Root_of_Expr root)
 519  , Type_from AST (Type_Root_of_Expr root)
 520  , Expr_from AST root
 521  , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
 522  , Lift_Error_Expr (Error_Expr_Lambda AST)       (Error_of_Expr AST root)
 523  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 524  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 525  , Root_of_Expr root ~ root
 526  , Implicit_HBool (Is_Last_Expr (Expr_Lambda_Lazy lam root) root)
 527  ) => Expr_from AST (Expr_Lambda_Lazy lam root) where
 528         expr_from ex ast ctx k =
 529                 case ast of
 530                  AST "lazy"     asts -> go_lam asts lazy
 531                  AST "let_lazy" asts -> go_let asts let_lazy
 532                  _ -> Left $ error_expr_unsupported ex ast
 533                 where
 534                 go_lam asts
 535                  (lam::forall repr arg res. Sym_Lambda_Lazy lam repr
 536                      => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
 537                         case asts of
 538                          [AST name [], ast_ty_arg, ast_body] ->
 539                                 lam_from (Proxy::Proxy lam) lam name ast_ty_arg ast_body ex ast ctx k
 540                          _ -> Left $ error_expr ex $
 541                                 Error_Expr_Wrong_number_of_arguments ast 3
 542                 go_let asts
 543                  (let_::forall repr var res. Sym_Lambda_Lazy lam repr
 544                      => repr var -> (repr var -> repr res) -> repr res) =
 545                         case asts of
 546                          [AST name [], ast_var, ast_body] ->
 547                                 let_from let_ name ast_var ast_body ex ast ctx k
 548                          _ -> Left $ error_expr ex $
 549                                 Error_Expr_Wrong_number_of_arguments ast 3
 550 instance -- Expr_from AST Expr_Maybe
 551  ( Eq_Type (Type_Root_of_Expr root)
 552  , Type_from AST (Type_Root_of_Expr root)
 553  , Expr_from AST root
 554  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 555  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 556  , Lift_Type   Type_Maybe     (Type_of_Expr root)
 557  , Unlift_Type Type_Maybe     (Type_of_Expr root)
 558  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 559  , Root_of_Expr root ~ root
 560  , Implicit_HBool (Is_Last_Expr (Expr_Maybe lam root) root)
 561  ) => Expr_from AST (Expr_Maybe lam root) where
 562         expr_from ex ast ctx k =
 563                 case ast of
 564                  AST "maybe"   asts -> from_ast3 asts maybe_from   ex ast ctx k
 565                  AST "nothing" asts -> from_ast1 asts nothing_from ex ast ctx k
 566                  AST "just"    asts -> from_ast1 asts just_from    ex ast ctx k
 567                  _ -> Left $ error_expr_unsupported ex ast
 568 instance -- Expr_from AST Expr_Eq
 569  ( Eq_Type (Type_Root_of_Expr root)
 570  , Type_from AST (Type_Root_of_Expr root)
 571  , Lift_Type Type_Bool (Type_of_Expr root)
 572  , Constraint_Type Eq (Type_Root_of_Expr root)
 573  , Expr_from AST root
 574  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 575  , Root_of_Expr root ~ root
 576  , Implicit_HBool (Is_Last_Expr (Expr_Eq root) root)
 577  ) => Expr_from AST (Expr_Eq root) where
 578         expr_from ex ast ctx k =
 579                 case ast of
 580                  AST "==" asts -> from_ast2 asts eq_from ex ast ctx k
 581                  _ -> Left $ error_expr_unsupported ex ast
 582 instance -- Expr_from AST Expr_Ord
 583  ( Eq_Type (Type_Root_of_Expr root)
 584  , Type_from AST (Type_Root_of_Expr root)
 585  , Lift_Type Type_Ordering (Type_of_Expr root)
 586  , Constraint_Type Ord (Type_Root_of_Expr root)
 587  , Expr_from AST root
 588  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 589  , Root_of_Expr root ~ root
 590  , Implicit_HBool (Is_Last_Expr (Expr_Ord root) root)
 591  ) => Expr_from AST (Expr_Ord root) where
 592         expr_from ex ast ctx k =
 593                 case ast of
 594                  AST "compare" asts -> from_ast2 asts compare_from ex ast ctx k
 595                  _ -> Left $ error_expr_unsupported ex ast
 596 instance -- Expr_from AST Expr_List
 597  ( Eq_Type (Type_Root_of_Expr root)
 598  , Type_from AST (Type_Root_of_Expr root)
 599  , Expr_from AST root
 600  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 601  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 602  , Lift_Type   Type_List      (Type_of_Expr root)
 603  , Unlift_Type Type_List      (Type_of_Expr root)
 604  , Lift_Type   Type_Bool      (Type_of_Expr root)
 605  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 606  , Root_of_Expr root ~ root
 607  , Implicit_HBool (Is_Last_Expr (Expr_List lam root) root)
 608  ) => Expr_from AST (Expr_List lam root) where
 609         expr_from ex ast ctx k =
 610                 case ast of
 611                  AST "[]"          asts -> from_ast1 asts list_empty_from  ex ast ctx k
 612                  AST ":"           asts -> from_ast2 asts list_cons_from   ex ast ctx k
 613                  AST "list_filter" asts -> from_ast2 asts list_filter_from ex ast ctx k
 614                  AST "list"        asts ->
 615                         case asts of
 616                          ast_ty_a:asts' -> list_from ast_ty_a asts' ex ast ctx k
 617                          _ -> Left $ error_expr ex $
 618                                 Error_Expr_Wrong_number_of_arguments ast 1
 619                  _ -> Left $ error_expr_unsupported ex ast
 620 instance -- Expr_from AST Expr_Map
 621  ( Eq_Type (Type_Root_of_Expr root)
 622  , Type_from AST (Type_Root_of_Expr root)
 623  , Expr_from AST root
 624  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 625  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 626  , Lift_Type   Type_Map       (Type_of_Expr root)
 627  , Unlift_Type Type_Map       (Type_of_Expr root)
 628  , Lift_Type   Type_List      (Type_of_Expr root)
 629  , Unlift_Type Type_List      (Type_of_Expr root)
 630  , Lift_Type   Type_Tuple2    (Type_of_Expr root)
 631  , Unlift_Type Type_Tuple2    (Type_of_Expr root)
 632  , Constraint_Type Ord (Type_Root_of_Expr root)
 633  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 634  , Root_of_Expr root ~ root
 635  , Implicit_HBool (Is_Last_Expr (Expr_Map lam root) root)
 636  ) => Expr_from AST (Expr_Map lam root) where
 637         expr_from ex ast ctx k =
 638                 case ast of
 639                  AST "map_from_list" asts -> from_ast1 asts map_from_list_from ex ast ctx k
 640                  AST "map_map" asts -> from_ast2 asts map_map_from ex ast ctx k
 641                  _ -> Left $ error_expr_unsupported ex ast
 642 instance -- Expr_from AST Expr_Functor
 643  ( Eq_Type (Type_Root_of_Expr root)
 644  , Type_from AST (Type_Root_of_Expr root)
 645  , Expr_from AST root
 646  , String_from_Type (Type_Root_of_Expr root)
 647  -- , Lift_Type   Type_Var1      (Type_of_Expr root)
 648  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 649  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 650  , Unlift_Type1 (Type_of_Expr root)
 651  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 652  , Constraint_Type1 Functor (Type_Root_of_Expr root)
 653  , Root_of_Expr root ~ root
 654  , Implicit_HBool (Is_Last_Expr (Expr_Functor lam root) root)
 655  ) => Expr_from AST (Expr_Functor lam root) where
 656         expr_from ex ast ctx k =
 657                 case ast of
 658                  AST "fmap" asts -> from_ast2 asts fmap_from ex ast ctx k
 659                  AST "<$>"  asts -> from_ast2 asts fmap_from ex ast ctx k
 660                  _ -> Left $ error_expr_unsupported ex ast
 661 instance -- Expr_from AST Expr_Applicative
 662  ( Eq_Type (Type_Root_of_Expr root)
 663  , Type1_from AST (Type_Root_of_Expr root)
 664  , Expr_from AST root
 665  , String_from_Type (Type_Root_of_Expr root)
 666  -- , Lift_Type   Type_Var1      (Type_of_Expr root)
 667  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 668  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 669  , Eq_Type1 (Type_Root_of_Expr root)
 670  , Unlift_Type1 (Type_of_Expr root)
 671  , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
 672  , Constraint_Type1 Applicative (Type_Root_of_Expr root)
 673  , Root_of_Expr root ~ root
 674  , Implicit_HBool (Is_Last_Expr (Expr_Applicative lam root) root)
 675  ) => Expr_from AST (Expr_Applicative lam root) where
 676         expr_from ex ast ctx k =
 677                 case ast of
 678                  AST "pure" asts -> from_ast2 asts pure_from     ex ast ctx k
 679                  AST "<*>"  asts -> from_ast2 asts ltstargt_from ex ast ctx k
 680                  _ -> Left $ error_expr_unsupported ex ast