content: {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE LambdaCase #-}
  
  -- |
  -- Module      : Jikka.RestrictedPython.Evaluate
  -- Description : evaluates programs of the restricted Python. / 制限された Python のプログラムを評価します。
  -- Copyright   : (c) Kimiyuki Onaka, 2021
  -- License     : Apache License 2.0
  -- Maintainer  : kimiyuki95@gmail.com
  -- Stability   : experimental
  -- Portability : portable
  module Jikka.RestrictedPython.Evaluate
    ( run,
  
      -- * internal functions
      makeGlobal,
      runWithGlobal,
      evalExpr,
      evalStatement,
      evalStatements,
      execToplevelStatement,
    )
  where
  
  import Control.Arrow (first)
  import Control.Monad.Reader
  import Control.Monad.State.Strict
  import Data.Bits
  import Data.List (maximumBy, minimumBy, sortBy)
  import qualified Data.Map.Strict as M
  import qualified Data.Vector as V
  import Jikka.Common.Combinatorics
  import Jikka.Common.Error
  import Jikka.RestrictedPython.Format (formatAttribute, formatBuiltin, formatOperator)
  import Jikka.RestrictedPython.Language.Expr
  import Jikka.RestrictedPython.Language.Lint
  import Jikka.RestrictedPython.Language.Util
  import Jikka.RestrictedPython.Language.Value
  
  assign :: MonadState Local m => VarName -> Value -> m ()
  assign x v = modify' (Local . M.insert x v . unLocal)
  
  lookupLocal :: (MonadState Local m, MonadError Error m) => VarName' -> m Value
  lookupLocal x = do
    local <- get
    case M.lookup (value' x) (unLocal local) of
      Just v -> return v
      Nothing -> throwInternalErrorAt' (loc' x) $ "undefined variable: " ++ formatVarName (value' x)
  
  assignSubscriptedTarget :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Target' -> Expr' -> Value -> m ()
  assignSubscriptedTarget f index v = wrapAt' (loc' f) $ do
    let go f indices = wrapAt' (loc' f) $ case value' f of
          SubscriptTrg f index -> go f (index : indices)
          NameTrg x -> return (x, indices)
          TupleTrg _ -> throwInternalError "cannot subscript a tuple target"
    (x, indices) <- go f [index]
    f <- lookupLocal x
    indices <- mapM evalExpr indices
    let go f index = case (f, index) of
          (_, []) -> return v
          (ListVal f, IntVal index : indices) -> do
            when (index < 0 || fromIntegral (V.length f) <= index) $ do
              throwRuntimeError "list index out of range"
            v' <- go (f V.! fromInteger index) indices
            return $ ListVal (f V.// [(fromInteger index, v')])
          (_, _) -> throwInternalError "type error"
    f <- go f indices
    assign (value' x) f
  
  assignTarget :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Target' -> Value -> m ()
  assignTarget x0 v = wrapAt' (loc' x0) $ case value' x0 of
    SubscriptTrg f index -> do
      assignSubscriptedTarget f index v
    NameTrg x -> do
      assign (value' x) v
    TupleTrg xs -> do
      case v of
        TupleVal vs -> do
          when (length xs /= length vs) $ do
            throwInternalError "the lengths of tuple are different"
          forM_ (zip xs vs) $ \(x, v) -> do
            assignTarget x v
        _ -> throwInternalError "cannot unpack non-tuple value"
  
  evalTarget :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Target' -> m Value
  evalTarget x0 = wrapAt' (loc' x0) $ case value' x0 of
    SubscriptTrg f index -> do
      f <- evalTarget f
      index <- evalExpr index
      case (f, index) of
        (ListVal f, IntVal index) -> do
          when (index < 0 || fromIntegral (V.length f) <= index) $ do
            throwRuntimeError "list index out of range"
          return $ f V.! fromInteger index
        (_, _) -> throwInternalError "type error"
    NameTrg x -> lookupLocal x
    TupleTrg xs -> TupleVal <$> mapM evalTarget xs
  
  -- | `evalExpr` evaluates exprs of our restricted Python-like language.
  --
  -- === Rules for \(e_1 \operatorname{boolop} e_2\)
  --
  -- \[
  --     \cfrac{e_1 \mid \mu \Downarrow \mathbf{false}}{e_1 ~\mathbf{and}~ e_2 \mid \mu \Downarrow \mathbf{false}}
  -- \]
  -- \[
  --     \cfrac{e_1 \mid \mu \Downarrow \mathbf{true} \qquad e_2 \mid \mu \Downarrow v}{e_1 ~\mathbf{and}~ e_2 \mid \mu \Downarrow v}
  -- \]
  -- \[
  --     \vdots
  -- \]
  --
  -- === Rules for \(e_1 \operatorname{binop} e_2\)
  --
  -- \[
  --     \cfrac{e_1 \mid \mu \Downarrow v_1 \qquad e_2 \mid \mu \Downarrow v_2}{e_1 + e_2 \mid \mu \Downarrow (v_1 + v_2)}
  -- \]
  -- \[
  --     \vdots
  -- \]
  --
  -- === Rules for \(\operatorname{unaryop} e\)
  --
  -- === Rules for \(\lambda x _ \tau x _ \tau \dots x _ \tau. e\)
  --
  -- \[
  --     \lambda {x_0} _ {\tau _ 0} {x_1} _ {\tau _ 1} \dots {x _ {n - 1}} _ {\tau _ {n - 1}}. e \mid \mu \Downarrow \lambda _ {\mu} x_0 x_1 \dots x _ {n - 1}. e
  -- \]
  --
  -- === Rules for \(\mathbf{if}~ e ~\mathbf{then}~ e ~\mathbf{else}~ e\)
  --
  -- === Rules for \(\lbrack e ~\mathbf{for}~ y ~\mathbf{in}~ e ~(\mathbf{if}~ e)? \rbrack\)
  --
  -- === Rules for \(e \operatorname{cmpop} e\)
  --
  -- === Rules for \(e (e, e, \dots, e)\)
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow \lambda _ {\mu'} x_0 x_1 \dots x _ {n - 1}. e'
  --         \qquad e_0 \mid \mu \Downarrow v_0
  --         \qquad e_1 \mid \mu \Downarrow v_1
  --         \qquad \dots
  --         \qquad e _ {n - 1} \mid \mu \Downarrow v _ {n - 1}
  --         \qquad e' \mid (x_0 \mapsto v_0; x_1 \mapsto v_1; \dots; x _ {n - 1} \mapsto v _ {n - 1}; \mu') \Downarrow v
  --     }{
  --         e(e_0, e_1, \dots, e _ {n - 1}) \mid \mu \Downarrow v
  --     }
  -- \]
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow b
  --         \qquad e_0 \mid \mu \Downarrow v_0
  --         \qquad e_1 \mid \mu \Downarrow v_1
  --         \qquad \dots
  --         \qquad e _ {n - 1} \mid \mu \Downarrow v _ {n - 1}
  --     }{
  --         e(e_0, e_1, \dots, e _ {n - 1}) \mid \mu \Downarrow b(e_0, e_1, \dots, e _ {n - 1})
  --     }
  --     \qquad{(b ~\text{is a builtin function})}
  -- \]
  --
  -- === Rules for \(\operatorname{constant}\)
  --
  -- === Rules for \(e \lbrack e \rbrack\)
  --
  -- === Rules for \(x\)
  --
  -- \[
  --     x \mid \mu \Downarrow \mu(x)
  -- \]
  --
  -- === Rules for \(\lbrack e, e, \dots, e \rbrack _ \tau\)
  --
  -- === Rules for \(e \lbrack e? \colon e? \colon e? \rbrack\)
  evalExpr :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Expr' -> m Value
  evalExpr e0 = wrapAt' (loc' e0) $ case value' e0 of
    BoolOp e1 op e2 -> do
      v1 <- evalExpr e1
      case (v1, op) of
        (BoolVal False, And) -> return $ BoolVal False
        (BoolVal True, And) -> evalExpr e2
        (BoolVal False, Or) -> evalExpr e2
        (BoolVal True, Or) -> return $ BoolVal True
        (BoolVal False, Implies) -> return $ BoolVal True
        (BoolVal True, Implies) -> evalExpr e2
        (_, _) -> throwInternalError "type error"
    BinOp e1 op e2 -> do
      v1 <- evalExpr e1
      v2 <- evalExpr e2
      evalBinOp v1 op v2
    UnaryOp op e -> do
      v <- evalExpr e
      case (op, v) of
        (Invert, IntVal v) -> return $ IntVal (complement v)
        (Not, BoolVal v) -> return $ BoolVal (not v)
        (UAdd, IntVal v) -> return $ IntVal v
        (USub, IntVal v) -> return $ IntVal (- v)
        (_, _) -> throwInternalError "type error"
    Lambda args body -> do
      savedLocal <- get
      return $ ClosureVal savedLocal (map (first value') args) [Return body]
    IfExp e1 e2 e3 -> do
      v1 <- evalExpr e1
      case v1 of
        BoolVal True -> evalExpr e2
        BoolVal False -> evalExpr e3
        _ -> throwInternalError "type error"
    ListComp e (Comprehension x iter pred) -> do
      iter <- evalExpr iter
      case iter of
        ListVal iter -> do
          savedLocal <- get
          vs <- V.forM iter $ \it -> do
            assignTarget x it
            pred <- mapM evalExpr pred
            case pred of
              Just (BoolVal False) -> return Nothing
              _ -> Just <$> evalExpr e
          put savedLocal
          return $ ListVal (V.catMaybes vs)
        _ -> throwInternalError "type error"
    Compare e1 op e2 -> do
      v1 <- evalExpr e1
      v2 <- evalExpr e2
      case op of
        CmpOp' In _ -> do
          v2 <- toList v2
          return $ BoolVal (v1 `V.elem` v2)
        CmpOp' NotIn _ -> do
          v2 <- toList v2
          return $ BoolVal (v1 `V.elem` v2)
        CmpOp' op _ -> do
          ordering <- maybe (throwInternalError "something wrong") return (compareValues v1 v2)
          BoolVal <$> case op of
            Eq' -> return $ ordering == EQ
            NotEq -> return $ ordering /= EQ
            Lt -> return $ ordering == LT
            LtE -> return $ ordering /= GT
            Gt -> return $ ordering == GT
            GtE -> return $ ordering /= LT
            Is -> return $ ordering == EQ
            IsNot -> return $ ordering /= EQ
            _ -> throwInternalError "something wrong"
    Call f args -> evalCall f args
    Constant const ->
      return $ case const of
        ConstNone -> TupleVal []
        ConstInt v -> IntVal v
        ConstBool v -> BoolVal v
        ConstBuiltin v -> BuiltinVal v
    Attribute e a -> AttributeVal <$> evalExpr e <*> pure (value' a)
    Subscript e1 e2 -> do
      v1 <- evalExpr e1
      v2 <- evalExpr e2
      case (v1, v2) of
        (ListVal v1, IntVal v2) -> do
          when (v2 < 0 || fromIntegral (V.length v1) <= v2) $ do
            throwRuntimeError "list index out of range"
          return $ v1 V.! fromInteger v2
        _ -> throwInternalError "type error"
    Starred _ ->
      throwInternalError "cannot evaluate starred expr"
    Name x -> do
      local <- get
      case M.lookup (value' x) (unLocal local) of
        Just v -> return v
        Nothing -> do
          global <- ask
          case M.lookup (value' x) (unGlobal global) of
            Just v -> return v
            Nothing -> throwInternalError $ "undefined variable: " ++ formatVarName (value' x)
    List _ es -> ListVal . V.fromList <$> mapM evalExpr es
    Tuple es -> TupleVal <$> mapM evalExpr es
    SubscriptSlice e from to step -> do
      v <- evalExpr e
      from <- mapM evalExpr from
      to <- mapM evalExpr to
      step <- mapM evalExpr step
      case v of
        ListVal v ->
          ListVal <$> case (from, to, step) of
            (_, _, Just _) -> throwInternalError "slice with step is TODO"
            (Nothing, Nothing, Nothing) -> return v
            (Nothing, Just (IntVal to), Nothing) -> return $ V.take (fromInteger to) v
            (Just (IntVal from), Nothing, Nothing) -> return $ V.drop (fromInteger from) v
            (Just (IntVal from), Just (IntVal to), Nothing) -> return $ V.drop (fromInteger from) (V.take (fromInteger to) v)
            (_, _, _) -> throwInternalError "type error"
        _ -> throwInternalError "type error"
  
  evalCall :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Expr' -> [Expr'] -> m Value
  evalCall f args = wrapAt' (loc' f) $ do
    f <- evalExpr f
    args <- mapM evalExpr args
    evalCall' f args
  
  evalCall' :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Value -> [Value] -> m Value
  evalCall' f actualArgs = case f of
    AttributeVal v a -> do
      evalAttribute v a actualArgs
    BuiltinVal b -> do
      evalBuiltin b actualArgs
    ClosureVal local formalArgs body -> do
      when (length formalArgs /= length actualArgs) $ do
        throwInternalError "wrong number of arguments"
      savedLocal <- get
      put local
      mapM_ (uncurry assign) (zip (map fst formalArgs) actualArgs)
      v <- evalStatements body
      put savedLocal
      case v of
        Just v -> return v
        Nothing -> throwRuntimeError "it reaches the end of function without return"
    _ -> throwRuntimeError "type error"
  
  -- | `evalStatement` evaluates statements of our restricted Python-like language.
  -- When a statement is evaluated, it returns a value \(v\), doesn't return anything \(\mathbf{stop}\), or fails \(\mathbf{err}\).
  -- Also it updates the environment function \(\mu\) from variables to values.
  --
  -- === Rules for \(\mathbf{return}~ e\)
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow v
  --     }{
  --         \mathbf{return}~ e \mid \mu \Downarrow v \mid \mu
  --     }
  -- \]
  --
  -- === Rules for \(y \operatorname{binop} = e\)
  --
  -- \[
  --     \cfrac{
  --         y \operatorname{binop} e \mid \mu \Downarrow v
  --     }{
  --         y \operatorname{binop} = e \mid \mu \Downarrow \mathbf{stop} \mid (y \mapsto v; \mu)
  --     }
  -- \]
  --
  -- === Rules for \(y := e\)
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow v
  --      }{
  --          y \operatorname{binop} = e \mid \mu \Downarrow \mathbf{stop} \mid (y \mapsto v; \mu)
  --      }
  -- \]
  --
  -- === Rules for \(\mathbf{for}~ y ~\mathbf{in}~ e \colon\quad \mathrm{stmt}; \mathrm{stmt}; \dots; \mathrm{stmt}\)
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow \mathbf{nil}
  --     }{
  --         (\mathbf{for}~ y ~\mathbf{in}~ e \colon~ \vec{\mathrm{stmt}}) \mid \mu \Downarrow \mathbf{stop} \mid \mu
  --     }
  -- \]
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow \mathbf{cons}(v_1, v_2)
  --         \qquad \vec{\mathrm{stmt}} \mid (y \mapsto v_1; \mu) \Downarrow v \mid \mu'
  --     }{
  --         (\mathbf{for}~ y ~\mathbf{in}~ e \colon~ \vec{\mathrm{stmt}}) \mid \mu \Downarrow v \mid \mu'
  --     }
  -- \]
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow \mathbf{cons}(v_1, v_2)
  --         \qquad \vec{\mathrm{stmt}} \mid (y \mapsto v_1; \mu) \Downarrow \mathbf{stop} \mid \mu'
  --         \qquad (\mathbf{for}~ y ~\mathbf{in}~ v_2 \colon~ \vec{\mathrm{stmt}}) \mid \mu' \Downarrow a \mid \mu''
  --     }{
  --         (\mathbf{for}~ y ~\mathbf{in}~ e \colon~ \vec{\mathrm{stmt}}) \mid \mu \Downarrow a \mid \mu''
  --     }
  --     \qquad{(a \in \lbrace v, \mathbf{stop} \rbrace)}
  -- \]
  --
  -- It assumes the program is properly alpha-converted, i.e. `doesntHaveLeakOfLoopCounters`. So it leaks loop counters to out of loops.
  --
  -- === Rules for \(\mathbf{if}~ e \colon\quad \mathrm{stmt}; \mathrm{stmt}; \dots; \mathrm{stmt};\quad \mathbf{else}\colon\quad \mathrm{stmt}; \mathrm{stmt}; \dots; \mathrm{stmt}\)
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow \mathbf{true}
  --         \qquad \vec{\mathrm{stmt}} _ 1 \mid \mu \Downarrow a \mid \mu'
  --     }{
  --         (\mathbf{if}~ e \colon~ \vec{\mathrm{stmt}} _ 1 ~\mathbf{else}\colon~ \vec{\mathrm{stmt}} _ 2) \mid \mu \Downarrow a \mid \mu'
  --     }
  --     \qquad{(a \in \lbrace v, \mathbf{stop} \rbrace)}
  -- \]
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow \mathbf{false}
  --         \qquad \vec{\mathrm{stmt}} _ 2 \mid \mu \Downarrow a \mid \mu'
  --     }{
  --         (\mathbf{if}~ e \colon~ \vec{\mathrm{stmt}} _ 1 ~\mathbf{else}\colon~ \vec{\mathrm{stmt}} _ 2) \mid \mu \Downarrow a \mid \mu'
  --     }
  --     \qquad{(a \in \lbrace v, \mathbf{stop} \rbrace)}
  -- \]
  --
  -- === Rules for \(\mathbf{assert}~ e\)
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow \mathbf{true}
  --     }{
  --         \mathbf{assert}~ e \mid \mu \Downarrow \mathbf{stop}
  --     }
  -- \]
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow \mathbf{false}
  --     }{
  --         \mathbf{assert}~ e \mid \mu \Downarrow \mathbf{err}
  --     }
  -- \]
  --
  -- === Rules for \(e\)
  --
  -- \[
  --     \cfrac{
  --         e \mid \mu \Downarrow v
  --     }{
  --         x.\mathrm{append}(e) \mid \mu \Downarrow \mathbf{stop} \mid (x \mapsto \mathrm{snoc}(\mu(x), v); \mu)
  --     }
  -- \]
  evalStatement :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Statement -> m (Maybe Value)
  evalStatement = \case
    Return e -> do
      v <- evalExpr e
      return $ Just v
    AugAssign x op e -> do
      v1 <- evalTarget x
      v2 <- evalExpr e
      v <- evalBinOp v1 op v2
      assignTarget x v
      return Nothing
    AnnAssign x _ e -> do
      v <- evalExpr e
      assignTarget x v
      return Nothing
    For x iter body -> do
      iter <- evalExpr iter
      case iter of
        ListVal iter -> do
          let go [] = return Nothing
              go (it : iter) = do
                assignTarget x it
                v <- evalStatements body
                case v of
                  Just v -> return $ Just v
                  Nothing -> go iter
          go (V.toList iter)
        _ -> wrapAt' (loc' x) $ do
          throwInternalError "type error"
    If pred body1 body2 -> do
      pred <- evalExpr pred
      if pred /= BoolVal False
        then evalStatements body1
        else evalStatements body2
    Assert e -> wrapAt' (loc' e) $ do
      v <- evalExpr e
      when (v == BoolVal False) $ do
        throwRuntimeError "assertion failure"
      return Nothing
    Append loc _ x e -> case exprToTarget x of
      Nothing -> throwSemanticErrorAt' loc "wrong `append` method"
      Just x -> do
        v1 <- evalTarget x
        v2 <- evalExpr e
        v <- ListVal <$> (V.snoc <$> toList v1 <*> pure v2)
        assignTarget x v
        return Nothing
    Expr' e -> throwSemanticErrorAt' (loc' e) "wrong expr-statement"
  
  -- | `evalStatements` evaluates sequences of statements of our restricted Python-like language.
  --
  -- \[
  --     \cfrac{\mathrm{stmt} _ 0 \mid \mu \Downarrow v \mid \mu'}{\mathrm{stmt} _ 0; \mathrm{stmt} _ 1; \dots; \mathrm{stmt} _ {n-1} \mid \mu \Downarrow v \mid \mu'}
  -- \]
  --
  -- \[
  --     \cfrac{\mathrm{stmt} _ 0 \mid \mu \Downarrow \mathbf{stop} \mid \mu' \qquad \mathrm{stmt} _ 1; \dots; \mathrm{stmt} _ {n-1} \mid \mu' \Downarrow a \mid \mu''}{\mathrm{stmt} _ 0; \mathrm{stmt} _ 1; \dots; \mathrm{stmt} _ {n-1} \mid \mu \Downarrow a \mid \mu''}
  --     \qquad{(a \in \lbrace v, \mathbf{stop} \rbrace)}
  -- \]
  --
  -- \[
  --     \epsilon \mid \mu \Downarrow \mathbf{stop} \mid \mu
  -- \]
  evalStatements :: (MonadReader Global m, MonadState Local m, MonadError Error m) => [Statement] -> m (Maybe Value)
  evalStatements [] = return Nothing
  evalStatements (stmt : stmts) = do
    v <- evalStatement stmt
    case v of
      Just v -> return $ Just v
      Nothing -> evalStatements stmts
  
  execToplevelStatement :: (MonadState Global m, MonadError Error m) => ToplevelStatement -> m ()
  execToplevelStatement = \case
    ToplevelAnnAssign x _ e -> do
      global <- get
      v <- runWithGlobal global e
      put $ Global (M.insert (value' x) v (unGlobal global))
    ToplevelFunctionDef f args _ body -> do
      global <- get
      let v = ClosureVal (Local M.empty) (map (first value') args) body
      put $ Global (M.insert (value' f) v (unGlobal global))
    ToplevelAssert e -> do
      global <- get
      v <- runWithGlobal global e
      when (v /= BoolVal True) $ do
        throwRuntimeError "assertion failure"
  
  newtype Global = Global
    { unGlobal :: M.Map VarName Value
    }
    deriving (Eq, Ord, Show, Read)
  
  initialGlobal :: Global
  initialGlobal = Global M.empty
  
  lookupGlobal :: MonadError Error m => VarName' -> Global -> m Value
  lookupGlobal x global =
    case M.lookup (value' x) (unGlobal global) of
      Just y -> return y
      Nothing -> throwSymbolErrorAt' (loc' x) $ "undefined variable: " ++ formatVarName (value' x)
  
  runWithGlobal :: MonadError Error m => Global -> Expr' -> m Value
  runWithGlobal global e = do
    runReaderT (evalStateT (evalExpr e) (Local M.empty)) global
  
  runWithGlobal' :: MonadError Error m => Global -> Value -> [Value] -> m Value
  runWithGlobal' global solve args = do
    runReaderT (evalStateT (evalCall' solve args) (Local M.empty)) global
  
  -- | `makeGlobal` packs toplevel definitions into `Global`.
  -- This assumes `doesntHaveLeakOfLoopCounters`.
  makeGlobal :: MonadError Error m => Program -> m Global
  makeGlobal prog = do
    ensureDoesntHaveLeakOfLoopCounters prog
    execStateT (mapM_ execToplevelStatement prog) initialGlobal
  
  run :: MonadError Error m => Program -> [Value] -> m Value
  run prog args = wrapError' "Jikka.RestrictedPython.Evaluate" $ do
    global <- makeGlobal prog
    solve <- lookupGlobal (withoutLoc solveVarName) global
    runWithGlobal' global solve args
  
  evalBinOp :: MonadError Error m => Value -> Operator -> Value -> m Value
  evalBinOp v1 op v2 = wrapError' ("calculating " ++ formatOperator op ++ " operator") $ do
    v1 <- toInt v1
    v2 <- toInt v2
    v <- case (op, v2) of
      (Add, _) -> return $ v1 + v2
      (Sub, _) -> return $ v1 - v2
      (Mult, _) -> return $ v1 * v2
      (MatMult, _) -> throwInternalError "matmul operator ('@') is not supported"
      (Div, _) -> throwInternalError "floatdiv operator ('/') is not supported"
      (FloorDiv, 0) -> throwRuntimeError "division by zero"
      (FloorDiv, _) -> return $ v1 `div` v2
      (FloorMod, 0) -> throwRuntimeError "division by zero"
      (FloorMod, _) -> return $ v1 `mod` v2
      (CeilDiv, 0) -> throwRuntimeError "division by zero"
      (CeilDiv, _) -> return $ (v1 + v2 - 1) `div` v2
      (CeilMod, 0) -> throwRuntimeError "division by zero"
      (CeilMod, _) -> return $ (v1 + v2 - 1) `mod` v2
      (Pow, _) -> return $ v1 ^ v2
      (BitLShift, _) -> return $ shiftL v1 (fromInteger v2)
      (BitRShift, _) -> return $ shiftR v1 (fromInteger v2)
      (BitOr, _) -> return $ v1 .|. v2
      (BitXor, _) -> return $ v1 `xor` v2
      (BitAnd, _) -> return $ v1 .&. v2
      (Max, _) -> return $ max v1 v2
      (Min, _) -> return $ min v1 v2
    return $ IntVal v
  
  evalBuiltin :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Builtin -> [Value] -> m Value
  evalBuiltin b args = wrapError' ("calling " ++ formatBuiltin b) $ do
    let go1' t1 ret f = case args of
          [v1] -> ret <$> (f =<< t1 v1)
          _ -> throwInternalError $ "expected 1 argument, got " ++ show (length args)
    let go1 t1 ret f = go1' t1 ret (return . f)
    let go2' t1 t2 ret f = case args of
          [v1, v2] -> ret <$> join (f <$> t1 v1 <*> t2 v2)
          _ -> throwInternalError $ "expected 2 arguments, got " ++ show (length args)
    let go2 t1 t2 ret f = go2' t1 t2 ret ((return .) . f)
    let go3 t1 t2 t3 ret f = case args of
          [v1, v2, v3] -> ret <$> (f <$> t1 v1 <*> t2 v2 <*> t3 v3)
          _ -> throwInternalError $ "expected 3 arguments, got " ++ show (length args)
    let goN' t ret f = ret <$> (f =<< mapM t args)
    let goN t ret f = goN' t ret (return . f)
    let zipN acc [] = reverse acc
        zipN acc xss | any null xss = reverse acc
        zipN acc xss = zipN (map head xss : acc) (map tail xss)
    case b of
      BuiltinAbs -> go1 toInt IntVal abs
      BuiltinPow -> go2 toInt toInt IntVal (^)
      BuiltinModPow -> go3 toInt toInt toInt IntVal $ \x k m -> (x ^ k) `mod` m
      BuiltinAll -> go1 toBoolList BoolVal minimum
      BuiltinAny -> go1 toBoolList BoolVal maximum
      BuiltinDivMod -> go2' toInt toInt TupleVal $ \a b -> case b of
        0 -> throwRuntimeError "division by zero"
        _ -> return [IntVal (a `div` b), IntVal (a `mod` b)]
      BuiltinSorted _ -> go1 toList ListVal (V.fromList . sortBy compareValues' . V.toList)
      BuiltinEnumerate _ -> go1 toList ListVal (V.fromList . zipWith (\i x -> TupleVal [IntVal i, x]) [0 ..] . V.toList)
      BuiltinBool _ -> go1' pure BoolVal $ \case
        IntVal n -> return $ n /= 0
        BoolVal p -> return p
        ListVal xs -> return $ not (V.null xs)
        TupleVal xs -> return $ not (null xs)
        _ -> throwInternalError "type error"
      BuiltinInt _ -> go1' return IntVal $ \case
        IntVal n -> return n
        BoolVal p -> return $ if p then 1 else 0
        _ -> throwInternalError "type error"
      BuiltinTuple _ -> goN pure TupleVal id
      BuiltinSum -> go1 toIntList IntVal sum
      BuiltinZip _ -> goN toList ListVal (V.fromList . map TupleVal . zipN [] . map V.toList)
      BuiltinFilter _ -> go2' pure toList ListVal $ \f xs -> do
        let go x = do
              pred <- evalCall' f [x]
              case pred of
                BoolVal True -> return $ Just x
                BoolVal False -> return Nothing
                _ -> throwInternalError "type error"
        V.mapMaybeM go xs
      BuiltinLen _ -> go1 toList IntVal (fromIntegral . V.length)
      BuiltinList _ -> go1 toList ListVal id
      BuiltinRange1 -> go1 toInt ListVal $ \to -> V.fromList (map IntVal [0 .. to - 1])
      BuiltinRange2 -> go2 toInt toInt ListVal $ \from to -> V.fromList (map IntVal [from .. to - 1])
      BuiltinRange3 -> go3 toInt toInt toInt ListVal $ \from to step -> V.fromList (map IntVal [from, from + step .. to - 1])
      BuiltinMap _ _ -> goN' pure ListVal $ \case
        [] -> throwInternalError "type error"
        f : args -> do
          args <- mapM toList args
          V.fromList <$> mapM (evalCall' f) (zipN [] (map V.toList args))
      BuiltinReversed _ -> go1 toList ListVal V.reverse
      BuiltinMin1 _ -> go1 toList id (minimumBy compareValues')
      BuiltinMin _ _ -> goN pure id (minimumBy compareValues')
      BuiltinMax1 _ -> go1 toList id (maximumBy compareValues')
      BuiltinMax _ _ -> goN pure id (maximumBy compareValues')
      BuiltinArgMax _ -> go1 toList IntVal $ \xs -> snd (maximumBy (\(x, i) (y, j) -> compareValues' x y <> compare i j) (zip (V.toList xs) [0 ..]))
      BuiltinArgMin _ -> go1 toList IntVal $ \xs -> snd (minimumBy (\(x, i) (y, j) -> compareValues' x y <> compare i j) (zip (V.toList xs) [0 ..]))
      BuiltinCeilDiv -> go2' toInt toInt IntVal $ \a b -> if b == 0 then throwRuntimeError "division by zero" else return $ (a + b - 1) `div` b
      BuiltinCeilMod -> go2' toInt toInt IntVal $ \a b -> if b == 0 then throwRuntimeError "division by zero" else return $ (a + b - 1) `mod` b
      BuiltinFloorDiv -> go2' toInt toInt IntVal $ \a b -> if b == 0 then throwRuntimeError "division by zero" else return $ a `div` b
      BuiltinFloorMod -> go2' toInt toInt IntVal $ \a b -> if b == 0 then throwRuntimeError "division by zero" else return $ a `mod` b
      BuiltinGcd -> go2 toInt toInt IntVal gcd
      BuiltinLcm -> go2 toInt toInt IntVal lcm
      BuiltinModInv -> go2' toInt toInt IntVal $ \_ _ -> throwInternalError "Jikka.RestrictedPython.Evaluate.evalBuiltin: TODO"
      BuiltinProduct -> go1 toIntList IntVal product
      BuiltinFact -> go1' toInt IntVal $ \n -> if 0 <= n then return $ fact n else throwRuntimeError "invalid argument"
      BuiltinChoose -> go2' toInt toInt IntVal $ \n r -> if 0 <= r && r <= n then return $ choose n r else throwRuntimeError "invalid argument"
      BuiltinPermute -> go2' toInt toInt IntVal $ \n r -> if 0 <= r && r <= n then return $ permute n r else throwRuntimeError "invalid argument"
      BuiltinMultiChoose -> go2' toInt toInt IntVal $ \n r -> if 0 <= r && r <= n then return $ multichoose n r else throwRuntimeError "invalid argument"
      BuiltinInput -> throwSemanticError "cannot use `input' out of main function"
      BuiltinPrint _ -> throwSemanticError "cannot use `print' out of main function"
  
  evalAttribute :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Value -> Attribute -> [Value] -> m Value
  evalAttribute v0 a args = wrapError' ("calling " ++ formatAttribute a) $ do
    let go0' t0 ret f = case args of
          [] -> ret <$> (f =<< t0 v0)
          _ -> throwInternalError $ "expected 0 arguments, got " ++ show (length args)
    let go0 t0 ret f = go0' t0 ret (return . f)
    let go1' t0 t1 ret f = case args of
          [v1] -> ret <$> join (f <$> t0 v0 <*> t1 v1)
          _ -> throwInternalError $ "expected 1 argument, got " ++ show (length args)
    let go1 t0 t1 ret f = go1' t0 t1 ret ((return .) . f)
    case a of
      UnresolvedAttribute a -> throwInternalError $ "Jikka.RestrictedPython.Evaluate.evalAttribute: unresolved attribute: " ++ unAttributeName a
      BuiltinCount _ -> go1 toList pure IntVal $ \xs x -> toInteger (V.length (V.filter (== x) xs))
      BuiltinIndex _ -> go1' toList pure IntVal $ \xs x -> case V.elemIndex x xs of
        Nothing -> throwRuntimeError $ "not in list: " ++ formatValue x
        Just i -> return (toInteger i)
      BuiltinCopy _ -> go0 toList ListVal id
      BuiltinAppend _ -> throwSemanticError "cannot use `append' out of expr-statements"
      BuiltinSplit -> throwSemanticError "cannot use `split' out of main function"
  