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 import Prelude hiding (and, not, or)
  21
  22 import Language.Symantic.Type
  23 import Language.Symantic.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 <$> 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  , Error_Expr_Lift (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  , Error_Expr_Lift (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  , Error_Expr_Lift (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  , Error_Expr_Lift (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  , Error_Expr_Lift (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  , Type_Eq (Type_Root_of_Expr root)
 134  , Expr_from ast root
 135  , Error_Expr_Lift (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  , Type_Eq (Type_Root_of_Expr root)
 153  , Expr_from ast root
 154  , Error_Expr_Lift (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_Var
 167  ( Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
 168  , Implicit_HBool (Is_Last_Type (Type_Var root) root)
 169  ) => Type_from AST (Type_Var 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_Unit
 174  ( Type_Root_Lift Type_Unit root
 175  , Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
 176  , Implicit_HBool (Is_Last_Type (Type_Unit root) root)
 177  ) => Type_from AST (Type_Unit root) where
 178         type_from ty ast k =
 179                 case ast of
 180                  AST "()" asts ->
 181                         case asts of
 182                          [] -> k type_unit
 183                          _ -> Left $ error_type_lift $
 184                                 Error_Type_Wrong_number_of_arguments ast 0
 185                  _ -> Left $ error_type_unsupported ty ast
 186 instance -- Type_from AST Type_Bool
 187  ( Type_Root_Lift Type_Bool root
 188  , Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
 189  , Implicit_HBool (Is_Last_Type (Type_Bool root) root)
 190  ) => Type_from AST (Type_Bool root) where
 191         type_from ty ast k =
 192                 case ast of
 193                  AST "Bool" asts ->
 194                         case asts of
 195                          [] -> k type_bool
 196                          _ -> Left $ error_type_lift $
 197                                 Error_Type_Wrong_number_of_arguments ast 0
 198                  _ -> Left $ error_type_unsupported ty ast
 199 instance -- Type_from AST Type_Int
 200  ( Type_Root_Lift Type_Int root
 201  , Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
 202  , Implicit_HBool (Is_Last_Type (Type_Int root) root)
 203  ) => Type_from AST (Type_Int root) where
 204         type_from ty ast k =
 205                 case ast of
 206                  AST "Int" asts ->
 207                         case asts of
 208                          [] -> k type_int
 209                          _ -> Left $ error_type_lift $
 210                                 Error_Type_Wrong_number_of_arguments ast 0
 211                  _ -> Left $ error_type_unsupported ty ast
 212 instance -- Type_from AST Type_Fun
 213  ( Type_Eq root
 214  , Type_from AST root
 215  , Type_Root_Lift (Type_Fun lam) root
 216  , Error_Type_Lift   (Error_Type AST) (Error_of_Type AST root)
 217  , Error_Type_Unlift (Error_Type AST) (Error_of_Type AST root)
 218  , Root_of_Type root ~ root
 219  , Implicit_HBool (Is_Last_Type (Type_Fun lam root) root)
 220  ) => Type_from AST (Type_Fun lam root) where
 221         type_from ty ast k =
 222                 case ast of
 223                  AST "->" asts ->
 224                         case asts of
 225                          [ast_arg, ast_res] -> type_fun_from ty ast_arg ast_res k
 226                          _ -> Left $ error_type_lift $
 227                                 Error_Type_Wrong_number_of_arguments ast 2
 228                  _ -> Left $ error_type_unsupported ty ast
 229 instance -- Type_from AST Type_Maybe
 230  ( Type_Eq root
 231  , Type_from AST root
 232  , Type_Root_Lift Type_Maybe root
 233  , Error_Type_Lift   (Error_Type AST) (Error_of_Type AST root)
 234  , Error_Type_Unlift (Error_Type AST) (Error_of_Type AST root)
 235  , Root_of_Type root ~ root
 236  , Implicit_HBool (Is_Last_Type (Type_Maybe root) root)
 237  ) => Type_from AST (Type_Maybe root) where
 238         type_from ty ast k =
 239                 case ast of
 240                  AST "Maybe" asts ->
 241                         case asts of
 242                          [ast_a] ->
 243                                 type_from (Proxy::Proxy root) ast_a $ \(ty_a::root h_a) ->
 244                                         k (type_root_lift $ Type_Maybe ty_a
 245                                          :: root (Maybe h_a))
 246                          _ -> Left $ error_type_lift $
 247                                 Error_Type_Wrong_number_of_arguments ast 1
 248                  _ -> Left $ error_type_unsupported ty ast
 249 instance -- Expr_from AST Expr_Bool
 250  ( Type_from AST (Type_Root_of_Expr root)
 251  , Expr_from AST root
 252  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
 253  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 254                                (                   Type_Root_of_Expr root)
 255                                AST)
 256                    (Error_of_Expr AST root)
 257  , Type_Unlift Type_Bool (Type_of_Expr root)
 258  , Root_of_Expr root ~ root
 259  , Implicit_HBool (Is_Last_Expr (Expr_Bool root) root)
 260  ) => Expr_from AST (Expr_Bool root) where
 261         expr_from ex ast =
 262                 case ast of
 263                  AST "bool" asts -> lit_from_AST bool type_bool asts ex ast
 264                  AST "not"  asts -> op1_from_AST not  type_bool asts ex ast
 265                  AST "and"  asts -> op2_from_AST and  type_bool asts ex ast
 266                  AST "or"   asts -> op2_from_AST or   type_bool asts ex ast
 267                  AST "xor"  asts -> op2_from_AST xor  type_bool asts ex ast
 268                  _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
 269 instance -- Expr_from AST Expr_If
 270  ( Type_from AST (Type_Root_of_Expr root)
 271  , Expr_from AST root
 272  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
 273  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 274                                (                   Type_Root_of_Expr root)
 275                                AST)
 276                    (Error_of_Expr AST root)
 277  , Root_of_Expr root ~ root
 278  , Implicit_HBool (Is_Last_Expr (Expr_If root) root)
 279  ) => Expr_from AST (Expr_If root) where
 280         expr_from ex ast ctx k =
 281                 case ast of
 282                  AST "if" asts -> from_ast3 asts if_from ex ast ctx k
 283                  _ -> Left $ error_expr_unsupported ex ast
 284 instance -- Expr_from AST Expr_When
 285  ( Type_from AST (Type_Root_of_Expr root)
 286  , Expr_from AST root
 287  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
 288  , Type_Root_Lift Type_Unit (Type_Root_of_Expr root)
 289  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 290                                (                   Type_Root_of_Expr root)
 291                                AST)
 292                    (Error_of_Expr AST root)
 293  , Root_of_Expr root ~ root
 294  , Implicit_HBool (Is_Last_Expr (Expr_When root) root)
 295  ) => Expr_from AST (Expr_When root) where
 296         expr_from ex ast ctx k =
 297                 case ast of
 298                  AST "when" asts -> from_ast2 asts when_from ex ast ctx k
 299                  _ -> Left $ error_expr_unsupported ex ast
 300 instance -- Expr_from AST Expr_Int
 301  ( Type_from AST (Type_Root_of_Expr root)
 302  , Expr_from AST root
 303  , Type_Root_Lift Type_Int (Type_Root_of_Expr root)
 304  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 305                                (                   Type_Root_of_Expr root)
 306                                AST)
 307                    (Error_of_Expr AST root)
 308
 309  , Type_Unlift Type_Int (Type_of_Expr root)
 310  , Root_of_Expr root ~ root
 311  , Implicit_HBool (Is_Last_Expr (Expr_Int root) root)
 312  ) => Expr_from AST (Expr_Int root) where
 313         expr_from ex ast =
 314                 case ast of
 315                  AST "int" asts -> lit_from_AST int type_int asts ex ast
 316                  AST "neg" asts -> op1_from_AST neg type_int asts ex ast
 317                  AST "add" asts -> op2_from_AST add type_int asts ex ast
 318                  _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
 319 instance -- Expr_from AST Expr_Lambda
 320  ( Type_from AST (Type_Root_of_Expr root)
 321  , Expr_from AST root
 322  , Type_Root_Lift (Type_Fun lam) (Type_Root_of_Expr root)
 323  , Error_Expr_Lift (Error_Expr_Lambda AST)
 324                    (Error_of_Expr AST root)
 325  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 326                                (                   Type_Root_of_Expr root)
 327                                AST)
 328                    (Error_of_Expr AST root)
 329  , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 330                                  (                   Type_Root_of_Expr root)
 331                                  AST)
 332                    (Error_of_Expr AST root)
 333  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
 334  , Root_of_Expr root ~ root
 335  , Implicit_HBool (Is_Last_Expr (Expr_Lambda lam root) root)
 336  ) => Expr_from AST (Expr_Lambda lam root) where
 337         expr_from ex ast ctx k =
 338                 case ast of
 339                  AST "var" asts ->
 340                         case asts of
 341                          [AST name []] -> var_from name ex ast ctx k
 342                          _ -> Left $ error_expr ex $
 343                                 Error_Expr_Wrong_number_of_arguments ast 1
 344                  AST "app"        asts -> from_ast2 asts app_from ex ast ctx k
 345                  AST "inline"     asts -> go_lam asts inline
 346                  AST "val"        asts -> go_lam asts val
 347                  AST "lazy"       asts -> go_lam asts lazy
 348                  AST "let_inline" asts -> go_let asts let_inline
 349                  AST "let_val"    asts -> go_let asts let_val
 350                  AST "let_lazy"   asts -> go_let asts let_lazy
 351                  _ -> Left $ error_expr_unsupported ex ast
 352                 where
 353                 go_lam asts
 354                  (lam::forall repr arg res. Sym_Lambda lam repr
 355                      => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
 356                         case asts of
 357                          [AST name [], ast_ty_arg, ast_body] ->
 358                                 lam_from lam name ast_ty_arg ast_body ex ast ctx k
 359                          _ -> Left $ error_expr ex $
 360                                 Error_Expr_Wrong_number_of_arguments ast 3
 361                 go_let asts
 362                  (let_::forall repr var res. Sym_Lambda lam repr
 363                      => repr var -> (repr var -> repr res) -> repr res) =
 364                         case asts of
 365                          [AST name [], ast_var, ast_body] ->
 366                                 let_from let_ name ast_var ast_body ex ast ctx k
 367                          _ -> Left $ error_expr ex $
 368                                 Error_Expr_Wrong_number_of_arguments ast 3
 369 instance -- Expr_from AST Expr_Maybe
 370  ( Type_from AST (Type_Root_of_Expr root)
 371  , Expr_from AST root
 372  , Type_Lift   (Type_Fun lam) (Type_of_Expr root)
 373  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
 374  , Type_Lift   Type_Maybe     (Type_of_Expr root)
 375  , Type_Unlift Type_Maybe     (Type_of_Expr root)
 376  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 377                                (                   Type_Root_of_Expr root)
 378                                AST)
 379                    (Error_of_Expr AST root)
 380  , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 381                                  (                   Type_Root_of_Expr root)
 382                                  AST)
 383                    (Error_of_Expr AST root)
 384  , Root_of_Expr root ~ root
 385  , Implicit_HBool (Is_Last_Expr (Expr_Maybe lam root) root)
 386  ) => Expr_from AST (Expr_Maybe lam root) where
 387         expr_from ex ast ctx k =
 388                 case ast of
 389                  AST "maybe"   asts -> from_ast3 asts maybe_from ex ast ctx k
 390                  AST "nothing" asts -> from_ast1 asts nothing_from ex ast ctx k
 391                  AST "just"    asts -> from_ast1 asts just_from ex ast ctx k
 392                  _ -> Left $ error_expr_unsupported ex ast
 393 instance -- Expr_from AST Expr_Eq
 394  ( Type_from AST (Type_Root_of_Expr root)
 395  , Type_Lift Type_Bool (Type_of_Expr root)
 396  , Type_Constraint Eq (Type_Root_of_Expr root)
 397  , Expr_from AST root
 398  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 399                                (                   Type_Root_of_Expr root)
 400                                AST)
 401                    (Error_of_Expr AST root)
 402  , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 403                                  (                   Type_Root_of_Expr root)
 404                                  AST)
 405                    (Error_of_Expr AST root)
 406  , Root_of_Expr root ~ root
 407  , Implicit_HBool (Is_Last_Expr (Expr_Eq root) root)
 408  ) => Expr_from AST (Expr_Eq root) where
 409         expr_from ex ast ctx k =
 410                 case ast of
 411                  AST "eq" asts -> from_ast2 asts eq_from ex ast ctx k
 412                  _ -> Left $ error_expr_unsupported ex ast
 413 instance -- Expr_from AST Expr_Ord
 414  ( Type_from AST (Type_Root_of_Expr root)
 415  , Type_Lift Type_Ordering (Type_of_Expr root)
 416  , Type_Constraint Ord (Type_Root_of_Expr root)
 417  , Expr_from AST root
 418  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 419                                (                   Type_Root_of_Expr root)
 420                                AST)
 421                    (Error_of_Expr AST root)
 422  , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 423                                  (                   Type_Root_of_Expr root)
 424                                  AST)
 425                    (Error_of_Expr AST root)
 426  , Root_of_Expr root ~ root
 427  , Implicit_HBool (Is_Last_Expr (Expr_Ord root) root)
 428  ) => Expr_from AST (Expr_Ord root) where
 429         expr_from ex ast ctx k =
 430                 case ast of
 431                  AST "compare" asts -> from_ast2 asts compare_from ex ast ctx k
 432                  _ -> Left $ error_expr_unsupported ex ast
 433 instance -- Expr_from AST Expr_List
 434  ( Type_from AST (Type_Root_of_Expr root)
 435  , Expr_from AST root
 436  , Type_Lift   (Type_Fun lam) (Type_of_Expr root)
 437  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
 438  , Type_Lift   Type_List      (Type_of_Expr root)
 439  , Type_Unlift Type_List      (Type_of_Expr root)
 440  , Type_Lift   Type_Bool      (Type_of_Expr root)
 441  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 442                                (                   Type_Root_of_Expr root)
 443                                AST)
 444                    (Error_of_Expr AST root)
 445  , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 446                                  (                   Type_Root_of_Expr root)
 447                                  AST)
 448                    (Error_of_Expr AST root)
 449  , Root_of_Expr root ~ root
 450  , Implicit_HBool (Is_Last_Expr (Expr_List lam root) root)
 451  ) => Expr_from AST (Expr_List lam root) where
 452         expr_from ex ast ctx k =
 453                 case ast of
 454                  AST "[]"          asts -> from_ast1 asts list_empty_from ex ast ctx k
 455                  AST ":"           asts -> from_ast2 asts list_cons_from ex ast ctx k
 456                  AST "list_filter" asts -> from_ast2 asts list_filter_from ex ast ctx k
 457                  _ -> Left $ error_expr_unsupported ex ast
 458 instance -- Expr_from AST Expr_Map
 459  ( Type_from AST (Type_Root_of_Expr root)
 460  , Expr_from AST root
 461  , Type_Lift   (Type_Fun lam) (Type_of_Expr root)
 462  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
 463  , Type_Lift   Type_Map      (Type_of_Expr root)
 464  , Type_Unlift Type_Map      (Type_of_Expr root)
 465  , Type_Lift   Type_List     (Type_of_Expr root)
 466  , Type_Unlift Type_List     (Type_of_Expr root)
 467  , Type_Lift   Type_Tuple2   (Type_of_Expr root)
 468  , Type_Unlift Type_Tuple2   (Type_of_Expr root)
 469  , Type_Constraint Ord (Type_Root_of_Expr root)
 470  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 471                                (                   Type_Root_of_Expr root)
 472                                AST)
 473                    (Error_of_Expr AST root)
 474  , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
 475                                  (                   Type_Root_of_Expr root)
 476                                  AST)
 477                    (Error_of_Expr AST root)
 478  , Root_of_Expr root ~ root
 479  , Implicit_HBool (Is_Last_Expr (Expr_Map lam root) root)
 480  ) => Expr_from AST (Expr_Map lam root) where
 481         expr_from ex ast ctx k =
 482                 case ast of
 483                  AST "map_from_list" asts -> from_ast1 asts map_from_list_from ex ast ctx k
 484                  AST "map_map" asts -> from_ast2 asts map_map_from ex ast ctx k
 485                  _ -> Left $ error_expr_unsupported ex ast