diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Changelog for Jikka
 
+## 2021-08-16: v5.3.0.0
+
+Many bugs are removed.
+
 ## 2021-08-07: v5.2.0.0
 
 Now we are fixing many bugs to use Jikka during contests!
diff --git a/Jikka.cabal b/Jikka.cabal
--- a/Jikka.cabal
+++ b/Jikka.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           Jikka
-version:        5.2.0.0
+version:        5.3.0.0
 synopsis:       A transpiler from Python to C++ for competitive programming
 description:    Please see the README on GitHub at <https://github.com/kmyk/Jikka>
 category:       Compilers/Interpreters
@@ -65,7 +65,7 @@
       Jikka.Core.Convert
       Jikka.Core.Convert.Alpha
       Jikka.Core.Convert.ANormal
-      Jikka.Core.Convert.ArithmeticalExpr
+      Jikka.Core.Convert.ArithmeticExpr
       Jikka.Core.Convert.Beta
       Jikka.Core.Convert.BubbleLet
       Jikka.Core.Convert.CloseAll
@@ -91,7 +91,7 @@
       Jikka.Core.Convert.UnpackTuple
       Jikka.Core.Evaluate
       Jikka.Core.Format
-      Jikka.Core.Language.ArithmeticalExpr
+      Jikka.Core.Language.ArithmeticExpr
       Jikka.Core.Language.Beta
       Jikka.Core.Language.BuiltinPatterns
       Jikka.Core.Language.Expr
@@ -112,6 +112,7 @@
       Jikka.CPlusPlus.Convert.AddMain
       Jikka.CPlusPlus.Convert.BundleRuntime
       Jikka.CPlusPlus.Convert.FromCore
+      Jikka.CPlusPlus.Convert.InlineSetAt
       Jikka.CPlusPlus.Convert.MoveSemantics
       Jikka.CPlusPlus.Convert.OptimizeRange
       Jikka.CPlusPlus.Convert.UnpackTuples
@@ -236,6 +237,7 @@
       Jikka.Core.Convert.CloseSumSpec
       Jikka.Core.Convert.ConstantFoldingSpec
       Jikka.Core.Convert.ConstantPropagationSpec
+      Jikka.Core.Convert.ConvexHullTrickSpec
       Jikka.Core.Convert.EtaSpec
       Jikka.Core.Convert.MakeScanlSpec
       Jikka.Core.Convert.MatrixExponentiationSpec
@@ -248,7 +250,7 @@
       Jikka.Core.Convert.UnpackTupleSpec
       Jikka.Core.EvaluateSpec
       Jikka.Core.FormatSpec
-      Jikka.Core.Language.ArithmeticalExprSpec
+      Jikka.Core.Language.ArithmeticExprSpec
       Jikka.Core.Language.BetaSpec
       Jikka.Core.ParseSpec
       Jikka.CPlusPlus.Convert.FromCoreSpec
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -73,6 +73,9 @@
   - 実装方針について
 - [docs/internal.ja.md](https://github.com/kmyk/Jikka/blob/master/docs/internal.ja.md) (Japanese)
   - 具体的な処理の流れについて
+- [docs/core.md](https://github.com/kmyk/Jikka/blob/master/docs/core.md)
+  - [docs/core.ja.md](https://github.com/kmyk/Jikka/blob/master/docs/core.ja.md) (Japanese)
+  - core 言語の説明
 - [Haddock](https://hackage.haskell.org/package/Jikka)
   - [Haddock (master)](https://kmyk.github.io/Jikka/haddock)
 
diff --git a/src/Jikka/CPlusPlus/Convert.hs b/src/Jikka/CPlusPlus/Convert.hs
--- a/src/Jikka/CPlusPlus/Convert.hs
+++ b/src/Jikka/CPlusPlus/Convert.hs
@@ -7,6 +7,7 @@
 
 import qualified Jikka.CPlusPlus.Convert.AddMain as AddMain
 import qualified Jikka.CPlusPlus.Convert.FromCore as FromCore
+import qualified Jikka.CPlusPlus.Convert.InlineSetAt as InlineSetAt
 import qualified Jikka.CPlusPlus.Convert.MoveSemantics as MoveSemantics
 import qualified Jikka.CPlusPlus.Convert.OptimizeRange as OptimizeRange
 import qualified Jikka.CPlusPlus.Convert.UnpackTuples as UnpackTuples
@@ -17,7 +18,7 @@
 import Jikka.Common.IOFormat
 import qualified Jikka.Core.Language.Expr as X
 
-run :: (MonadAlpha m, MonadError Error m) => X.Program -> IOFormat -> m Y.Program
+run :: (MonadAlpha m, MonadError Error m) => X.Program -> Maybe IOFormat -> m Y.Program
 run prog format = do
   prog <- FromCore.run prog
   let go prog = do
@@ -26,6 +27,7 @@
         OptimizeRange.run prog
   prog <- go prog
   prog <- go prog
+  prog <- InlineSetAt.run prog
   prog <- go prog
-  prog <- AddMain.run prog format
+  prog <- maybe (return prog) (AddMain.run prog) format
   UseInitialization.run prog
diff --git a/src/Jikka/CPlusPlus/Convert/FromCore.hs b/src/Jikka/CPlusPlus/Convert/FromCore.hs
--- a/src/Jikka/CPlusPlus/Convert/FromCore.hs
+++ b/src/Jikka/CPlusPlus/Convert/FromCore.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 
@@ -17,6 +18,7 @@
   )
 where
 
+import Control.Monad.Writer.Strict
 import qualified Jikka.CPlusPlus.Language.Expr as Y
 import qualified Jikka.CPlusPlus.Language.Util as Y
 import Jikka.Common.Alpha
@@ -24,6 +26,7 @@
 import qualified Jikka.Core.Format as X (formatBuiltinIsolated, formatType)
 import qualified Jikka.Core.Language.BuiltinPatterns as X
 import qualified Jikka.Core.Language.Expr as X
+import qualified Jikka.Core.Language.LambdaPatterns as X
 import qualified Jikka.Core.Language.TypeCheck as X
 import qualified Jikka.Core.Language.Util as X
 
@@ -43,6 +46,20 @@
   Just y -> return y
   Nothing -> throwInternalError $ "undefined variable: " ++ X.unVarName x
 
+class Monad m => MonadStatements m where
+  useStatement :: Y.Statement -> m ()
+
+instance Monad m => MonadStatements (WriterT (Dual [Y.Statement]) m) where
+  useStatement stmt = tell $ Dual [stmt]
+
+useStatements :: MonadStatements m => [Y.Statement] -> m ()
+useStatements = mapM_ useStatement
+
+runStatementsT :: Monad m => WriterT (Dual [Y.Statement]) m a -> m ([Y.Statement], a)
+runStatementsT f = do
+  (a, stmts) <- runWriterT f
+  return (reverse (getDual stmts), a)
+
 --------------------------------------------------------------------------------
 -- run
 
@@ -74,7 +91,7 @@
 runLiteral :: (MonadAlpha m, MonadError Error m) => Env -> X.Literal -> m Y.Expr
 runLiteral env = \case
   X.LitBuiltin builtin ts -> do
-    (stmts, e) <- runAppBuiltin env builtin ts []
+    (stmts, e) <- runStatementsT $ runAppBuiltin env builtin ts []
     case stmts of
       [] -> return e
       _ -> throwInternalError "now builtin values don't use statements"
@@ -101,89 +118,146 @@
   X.Proj _ -> return 1
   builtin -> length . fst . X.uncurryFunTy <$> X.builtinToType builtin ts
 
-runAppBuiltin :: (MonadAlpha m, MonadError Error m) => Env -> X.Builtin -> [X.Type] -> [X.Expr] -> m ([Y.Statement], Y.Expr)
+runIterate :: (MonadStatements m, MonadAlpha m, MonadError Error m) => Env -> X.Type -> X.Expr -> X.Expr -> X.Expr -> m Y.Expr
+runIterate env t n f x = do
+  t <- runType t
+  n <- runExpr env n
+  x <- runExpr env x
+  y <- Y.newFreshName Y.LocalNameKind
+  i <- Y.newFreshName Y.LoopCounterNameKind
+  (stmtsF, body, f) <- runExprFunction env f (Y.Var y)
+  useStatement $ Y.Declare t y (Y.DeclareCopy x)
+  useStatements stmtsF
+  useStatement $ Y.repStatement i (Y.cast Y.TyInt32 n) (body ++ [Y.assignSimple y f])
+  return $ Y.Var y
+
+runIf :: (MonadStatements m, MonadAlpha m, MonadError Error m) => Env -> X.Type -> X.Expr -> X.Expr -> X.Expr -> m Y.Expr
+runIf env t e1 e2 e3 = do
+  e1' <- runExpr env e1
+  (stmts2, e2') <- runStatementsT $ runExpr env e2
+  (stmts3, e3') <- runStatementsT $ runExpr env e3
+  case (stmts2, stmts3) of
+    ([], [])
+      | X.isConstantTimeExpr e2 && X.isConstantTimeExpr e3 ->
+        return $ Y.Cond e1' e2' e3'
+    _ -> do
+      t <- runType t
+      phi <- Y.newFreshName Y.LocalNameKind
+      let assign = Y.Assign . Y.AssignExpr Y.SimpleAssign (Y.LeftVar phi)
+      useStatement $ Y.Declare t phi Y.DeclareDefault
+      useStatement $ Y.If e1' (stmts2 ++ [assign e2']) (Just (stmts3 ++ [assign e3']))
+      return $ Y.Var phi
+
+runFoldl :: (MonadStatements m, MonadAlpha m, MonadError Error m) => Env -> X.Type -> X.Type -> X.Expr -> X.Expr -> X.Expr -> m Y.Expr
+runFoldl env t1 t2 f init xs = do
+  init <- runExpr env init
+  xs <- runExpr env xs
+  t1 <- runType t1
+  t2 <- runType t2
+  y <- Y.newFreshName Y.LocalNameKind
+  x <- Y.newFreshName Y.LocalNameKind
+  (stmtsF, body, f) <- runExprFunction2 env f (Y.Var y) (Y.Var x)
+  useStatement $ Y.Declare t2 y (Y.DeclareCopy init)
+  useStatements stmtsF
+  useStatement $ Y.ForEach t1 x xs (body ++ [Y.assignSimple y f])
+  return $ Y.Var y
+
+runMap :: (MonadStatements m, MonadAlpha m, MonadError Error m) => Env -> X.Type -> X.Type -> X.Expr -> X.Expr -> m Y.Expr
+runMap env _ t2 f xs = do
+  ys <- Y.newFreshName Y.LocalNameKind
+  t2 <- runType t2
+  case (f, xs) of
+    -- optimize @map (const e) xs@
+    (X.LamConst _ e, xs) -> do
+      xs <- runExpr env xs
+      e <- runExpr env e
+      useStatement $ Y.Declare (Y.TyVector t2) ys (Y.DeclareCopy (Y.vecCtor t2 [Y.size xs, e]))
+      return $ Y.Var ys
+    -- other cases
+    _ -> do
+      xs <- runExpr env xs
+      i <- Y.newFreshName Y.LoopCounterNameKind
+      (stmtsF, body, f) <- runExprFunction env f (Y.at xs (Y.Var i))
+      useStatement $ Y.Declare (Y.TyVector t2) ys (Y.DeclareCopy (Y.vecCtor t2 [Y.size xs]))
+      useStatements stmtsF
+      useStatement $ Y.repStatement i (Y.cast Y.TyInt32 (Y.size xs)) (body ++ [Y.assignAt ys (Y.Var i) f])
+      return $ Y.Var ys
+
+runAppBuiltin :: (MonadStatements m, MonadAlpha m, MonadError Error m) => Env -> X.Builtin -> [X.Type] -> [X.Expr] -> m Y.Expr
 runAppBuiltin env f ts args = wrapError' ("converting builtin " ++ X.formatBuiltinIsolated f ts) $ do
-  let go0T f = case ts of
+  let go0T :: (MonadAlpha m, MonadError Error m, MonadStatements m) => m Y.Expr -> m Y.Expr
+      go0T f = case ts of
         [] -> f
         _ -> throwInternalError $ "expected 0 type arguments, got " ++ show (length ts)
-  let go1T' f = case ts of
+  let go1T' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (X.Type -> m Y.Expr) -> m Y.Expr
+      go1T' f = case ts of
         [t1] -> f t1
         _ -> throwInternalError $ "expected 1 type argument, got " ++ show (length ts)
-  let go1T f = go1T' $ f <=< runType
+  let go1T :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Type -> m Y.Expr) -> m Y.Expr
+      go1T f = go1T' $ f <=< runType
   let go2T' f = case ts of
         [t1, t2] -> f t1 t2
         _ -> throwInternalError $ "expected 2 type arguments, got " ++ show (length ts)
-  let go0E f = case args of
+  let go0E :: (MonadAlpha m, MonadError Error m, MonadStatements m) => m Y.Expr -> m Y.Expr
+      go0E f = case args of
         [] -> f
         _ -> throwInternalError $ "expected 0 type arguments, got " ++ show (length args)
-  let go1E' f = case args of
+  let go1E' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (X.Expr -> m Y.Expr) -> m Y.Expr
+      go1E' f = case args of
         [e1] -> f e1
         _ -> throwInternalError $ "expected 1 type argument, got " ++ show (length args)
-  let go1E f = go1E' $ \e1 -> do
-        (stmts1, e1) <- runExpr env e1
-        (stmts, e) <- f e1
-        return (stmts1 ++ stmts, e)
+  let go1E :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Expr -> m Y.Expr) -> m Y.Expr
+      go1E f = go1E' $ f <=< runExpr env
   let go2E' f = case args of
         [e1, e2] -> f e1 e2
         _ -> throwInternalError $ "expected 2 type arguments, got " ++ show (length args)
-  let go2E f = go2E' $ \e1 e2 -> do
-        (stmts1, e1) <- runExpr env e1
-        (stmts2, e2) <- runExpr env e2
-        (stmts, e) <- f e1 e2
-        return (stmts1 ++ stmts2 ++ stmts, e)
+  let go2E f = go2E' $ \e1 e2 -> join $ f <$> runExpr env e1 <*> runExpr env e2
   let go3E' f = case args of
         [e1, e2, e3] -> f e1 e2 e3
         _ -> throwInternalError $ "expected 2 type arguments, got " ++ show (length args)
-  let go3E f = go3E' $ \e1 e2 e3 -> do
-        (stmts1, e1) <- runExpr env e1
-        (stmts2, e2) <- runExpr env e2
-        (stmts3, e3) <- runExpr env e3
-        (stmts, e) <- f e1 e2 e3
-        return (stmts1 ++ stmts2 ++ stmts3 ++ stmts, e)
-  let goP f = return ([], f)
-  let go00 f = go0T $ go0E $ goP f
-  let go01' :: (MonadAlpha m, MonadError Error m) => (Y.Expr -> m ([Y.Statement], Y.Expr)) -> m ([Y.Statement], Y.Expr)
+  let go3E f = go3E' $ \e1 e2 e3 -> join $ f <$> runExpr env e1 <*> runExpr env e2 <*> runExpr env e3
+  let go00 f = go0T $ go0E $ return f
+  let go01' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Expr -> m Y.Expr) -> m Y.Expr
       go01' f = go0T $ go1E f
-  let go01 :: (MonadAlpha m, MonadError Error m) => (Y.Expr -> Y.Expr) -> m ([Y.Statement], Y.Expr)
-      go01 f = go0T $ go1E $ \e1 -> goP $ f e1
-  let go11' :: (MonadAlpha m, MonadError Error m) => (Y.Type -> Y.Expr -> m ([Y.Statement], Y.Expr)) -> m ([Y.Statement], Y.Expr)
+  let go01 :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Expr -> Y.Expr) -> m Y.Expr
+      go01 f = go0T $ go1E $ \e1 -> return $ f e1
+  let go11' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Type -> Y.Expr -> m Y.Expr) -> m Y.Expr
       go11' f = go1T $ \t1 -> go1E $ \e1 -> f t1 e1
-  let go11 :: (MonadAlpha m, MonadError Error m) => (Y.Type -> Y.Expr -> Y.Expr) -> m ([Y.Statement], Y.Expr)
-      go11 f = go1T $ \t1 -> go1E $ \e1 -> goP $ f t1 e1
-  let go02' :: (MonadAlpha m, MonadError Error m) => (Y.Expr -> Y.Expr -> m ([Y.Statement], Y.Expr)) -> m ([Y.Statement], Y.Expr)
+  let go11 :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Type -> Y.Expr -> Y.Expr) -> m Y.Expr
+      go11 f = go1T $ \t1 -> go1E $ \e1 -> return $ f t1 e1
+  let go02' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Expr -> Y.Expr -> m Y.Expr) -> m Y.Expr
       go02' f = go0T $ go2E f
-  let go02 :: (MonadAlpha m, MonadError Error m) => (Y.Expr -> Y.Expr -> Y.Expr) -> m ([Y.Statement], Y.Expr)
-      go02 f = go0T $ go2E $ \e1 e2 -> goP $ f e1 e2
-  let go12'' :: (MonadAlpha m, MonadError Error m) => (X.Type -> X.Expr -> X.Expr -> m ([Y.Statement], Y.Expr)) -> m ([Y.Statement], Y.Expr)
+  let go02 :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Expr -> Y.Expr -> Y.Expr) -> m Y.Expr
+      go02 f = go0T $ go2E $ \e1 e2 -> return $ f e1 e2
+  let go12'' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (X.Type -> X.Expr -> X.Expr -> m Y.Expr) -> m Y.Expr
       go12'' f = go1T' $ \t1 -> go2E' $ \e1 e2 -> f t1 e1 e2
-  let go12' :: (MonadAlpha m, MonadError Error m) => (Y.Type -> Y.Expr -> Y.Expr -> m ([Y.Statement], Y.Expr)) -> m ([Y.Statement], Y.Expr)
+  let go12' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Type -> Y.Expr -> Y.Expr -> m Y.Expr) -> m Y.Expr
       go12' f = go1T $ \t1 -> go2E $ \e1 e2 -> f t1 e1 e2
-  let go12 :: (MonadAlpha m, MonadError Error m) => (Y.Type -> Y.Expr -> Y.Expr -> Y.Expr) -> m ([Y.Statement], Y.Expr)
-      go12 f = go1T $ \t1 -> go2E $ \e1 e2 -> goP $ f t1 e1 e2
-  let go22'' :: (MonadAlpha m, MonadError Error m) => (X.Type -> X.Type -> X.Expr -> X.Expr -> m ([Y.Statement], Y.Expr)) -> m ([Y.Statement], Y.Expr)
+  let go12 :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Type -> Y.Expr -> Y.Expr -> Y.Expr) -> m Y.Expr
+      go12 f = go1T $ \t1 -> go2E $ \e1 e2 -> return $ f t1 e1 e2
+  let go22'' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (X.Type -> X.Type -> X.Expr -> X.Expr -> m Y.Expr) -> m Y.Expr
       go22'' f = go2T' $ \t1 t2 -> go2E' $ \e1 e2 -> f t1 t2 e1 e2
-  let go03' :: (MonadAlpha m, MonadError Error m) => (Y.Expr -> Y.Expr -> Y.Expr -> m ([Y.Statement], Y.Expr)) -> m ([Y.Statement], Y.Expr)
+  let go03' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Expr -> Y.Expr -> Y.Expr -> m Y.Expr) -> m Y.Expr
       go03' f = go0T $ go3E f
-  let go03 f = go0T $ go3E $ \e1 e2 e3 -> goP $ f e1 e2 e3
-  let go13'' :: (MonadAlpha m, MonadError Error m) => (X.Type -> X.Expr -> X.Expr -> X.Expr -> m ([Y.Statement], Y.Expr)) -> m ([Y.Statement], Y.Expr)
+  let go03 f = go0T $ go3E $ \e1 e2 e3 -> return $ f e1 e2 e3
+  let go13'' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (X.Type -> X.Expr -> X.Expr -> X.Expr -> m Y.Expr) -> m Y.Expr
       go13'' f = go1T' $ \t1 -> go3E' $ \e1 e2 e3 -> f t1 e1 e2 e3
-  let go13' :: (MonadAlpha m, MonadError Error m) => (Y.Type -> Y.Expr -> Y.Expr -> Y.Expr -> m ([Y.Statement], Y.Expr)) -> m ([Y.Statement], Y.Expr)
-      go13' f = go1T $ \t1 -> go3E $ \e1 e2 e3 -> f t1 e1 e2 e3
-  let go23'' :: (MonadAlpha m, MonadError Error m) => (X.Type -> X.Type -> X.Expr -> X.Expr -> X.Expr -> m ([Y.Statement], Y.Expr)) -> m ([Y.Statement], Y.Expr)
+  let go13 :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (Y.Type -> Y.Expr -> Y.Expr -> Y.Expr -> Y.Expr) -> m Y.Expr
+      go13 f = go1T $ \t1 -> go3E $ \e1 e2 e3 -> return $ f t1 e1 e2 e3
+  let go23'' :: (MonadAlpha m, MonadError Error m, MonadStatements m) => (X.Type -> X.Type -> X.Expr -> X.Expr -> X.Expr -> m Y.Expr) -> m Y.Expr
       go23'' f = go2T' $ \t1 t2 -> go3E' $ \e1 e2 e3 -> f t1 t2 e1 e2 e3
-  let goN1 :: (MonadAlpha m, MonadError Error m) => ([Y.Type] -> Y.Expr -> Y.Expr) -> m ([Y.Statement], Y.Expr)
+  let goN1 :: (MonadAlpha m, MonadError Error m, MonadStatements m) => ([Y.Type] -> Y.Expr -> Y.Expr) -> m Y.Expr
       goN1 f = case args of
         [e1] -> do
           ts <- mapM runType ts
-          (stmts1, e1) <- runExpr env e1
-          return (stmts1, f ts e1)
+          e1 <- runExpr env e1
+          return $ f ts e1
         _ -> throwInternalError $ "expected 1 argument, got " ++ show (length args)
-  let goNN :: (MonadAlpha m, MonadError Error m) => ([Y.Type] -> [Y.Expr] -> Y.Expr) -> m ([Y.Statement], Y.Expr)
+  let goNN :: (MonadAlpha m, MonadError Error m, MonadStatements m) => ([Y.Type] -> [Y.Expr] -> Y.Expr) -> m Y.Expr
       goNN f = do
         ts <- mapM runType ts
         args <- mapM (runExpr env) args
-        let e = f ts (map snd args)
-        return (concatMap fst args, e)
+        return $ f ts args
   case f of
     -- arithmetical functions
     X.Negate -> go01 $ \e -> Y.UnOp Y.Negate e
@@ -201,42 +275,13 @@
     X.Lcm -> go02 $ \e1 e2 -> Y.Call (Y.Function "std::lcm" []) [e1, e2]
     X.Min2 -> go12 $ \t e1 e2 -> Y.Call (Y.Function "std::min" [t]) [e1, e2]
     X.Max2 -> go12 $ \t e1 e2 -> Y.Call (Y.Function "std::max" [t]) [e1, e2]
-    X.Iterate -> go13'' $ \t n f x -> do
-      t <- runType t
-      (stmtsN, n) <- runExpr env n
-      (stmtsX, x) <- runExpr env x
-      y <- Y.newFreshName Y.LocalNameKind
-      i <- Y.newFreshName Y.LoopCounterNameKind
-      (stmtsF, body, f) <- runExprFunction env f (Y.Var y)
-      return
-        ( stmtsN ++ stmtsX
-            ++ [Y.Declare t y (Y.DeclareCopy x)]
-            ++ stmtsF
-            ++ [ Y.repStatement
-                   i
-                   (Y.cast Y.TyInt32 n)
-                   (body ++ [Y.assignSimple y f])
-               ],
-          Y.Var y
-        )
+    X.Iterate -> go13'' $ runIterate env
     -- logical functions
     X.Not -> go01 $ \e -> Y.UnOp Y.Not e
     X.And -> go02 $ \e1 e2 -> Y.BinOp Y.And e1 e2
     X.Or -> go02 $ \e1 e2 -> Y.BinOp Y.Or e1 e2
     X.Implies -> go02 $ \e1 e2 -> Y.BinOp Y.Or (Y.UnOp Y.Not e1) e2
-    X.If -> go13'' $ \t e1 e2 e3 -> do
-      (stmts1, e1') <- runExpr env e1
-      (stmts2, e2') <- runExpr env e2
-      (stmts3, e3') <- runExpr env e3
-      case (stmts2, stmts3) of
-        ([], [])
-          | X.isConstantTimeExpr e2 && X.isConstantTimeExpr e3 ->
-            return (stmts1, Y.Cond e1' e2' e3')
-        _ -> do
-          t <- runType t
-          phi <- Y.newFreshName Y.LocalNameKind
-          let assign = Y.Assign . Y.AssignExpr Y.SimpleAssign (Y.LeftVar phi)
-          return ([Y.Declare t phi Y.DeclareDefault] ++ stmts1 ++ [Y.If e1' (stmts2 ++ [assign e2']) (Just (stmts3 ++ [assign e3']))], Y.Var phi)
+    X.If -> go13'' $ runIf env
     -- bitwise functions
     X.BitNot -> go01 $ \e -> Y.UnOp Y.BitNot e
     X.BitAnd -> go02 $ \e1 e2 -> Y.BinOp Y.BitAnd e1 e2
@@ -245,14 +290,14 @@
     X.BitLeftShift -> go02 $ \e1 e2 -> Y.BinOp Y.BitLeftShift e1 e2
     X.BitRightShift -> go02 $ \e1 e2 -> Y.BinOp Y.BitRightShift e1 e2
     -- matrix functions
-    X.MatAp h w -> go02 $ \f x -> Y.Call (Y.Function "jikka::mat::ap" [Y.TyIntValue (fromIntegral h), Y.TyIntValue (fromIntegral w)]) [f, x]
-    X.MatZero n -> go00 $ Y.Call (Y.Function "jikka::mat::zero" [Y.TyIntValue (fromIntegral n)]) []
-    X.MatOne n -> go00 $ Y.Call (Y.Function "jikka::mat::one" [Y.TyIntValue (fromIntegral n)]) []
-    X.MatAdd h w -> go02 $ \f g -> Y.Call (Y.Function "jikka::mat::add" [Y.TyIntValue (fromIntegral h), Y.TyIntValue (fromIntegral w)]) [f, g]
-    X.MatMul h n w -> go02 $ \f g -> Y.Call (Y.Function "jikka::mat::mul" [Y.TyIntValue (fromIntegral h), Y.TyIntValue (fromIntegral n), Y.TyIntValue (fromIntegral w)]) [f, g]
-    X.MatPow n -> go02 $ \f k -> Y.Call (Y.Function "jikka::mat::pow" [Y.TyIntValue (fromIntegral n)]) [f, k]
-    X.VecFloorMod n -> go02 $ \x m -> Y.Call (Y.Function "jikka::modmat::floormod" [Y.TyIntValue (fromIntegral n)]) [x, m]
-    X.MatFloorMod h w -> go02 $ \f m -> Y.Call (Y.Function "jikka::modmat::floormod" [Y.TyIntValue (fromIntegral h), Y.TyIntValue (fromIntegral w)]) [f, m]
+    X.MatAp h w -> go02 $ \f x -> Y.Call (Y.Function "jikka::mat::ap" [Y.TyIntValue h, Y.TyIntValue w]) [f, x]
+    X.MatZero h w -> go00 $ Y.Call (Y.Function "jikka::mat::zero" [Y.TyIntValue h, Y.TyIntValue w]) []
+    X.MatOne n -> go00 $ Y.Call (Y.Function "jikka::mat::one" [Y.TyIntValue n]) []
+    X.MatAdd h w -> go02 $ \f g -> Y.Call (Y.Function "jikka::mat::add" [Y.TyIntValue h, Y.TyIntValue w]) [f, g]
+    X.MatMul h n w -> go02 $ \f g -> Y.Call (Y.Function "jikka::mat::mul" [Y.TyIntValue h, Y.TyIntValue n, Y.TyIntValue w]) [f, g]
+    X.MatPow n -> go02 $ \f k -> Y.Call (Y.Function "jikka::mat::pow" [Y.TyIntValue n]) [f, k]
+    X.VecFloorMod n -> go02 $ \x m -> Y.Call (Y.Function "jikka::modmat::floormod" [Y.TyIntValue n]) [x, m]
+    X.MatFloorMod h w -> go02 $ \f m -> Y.Call (Y.Function "jikka::modmat::floormod" [Y.TyIntValue h, Y.TyIntValue w]) [f, m]
     -- modular functions
     X.ModNegate -> go02 $ \e1 e2 -> Y.Call (Y.Function "jikka::mod::negate" []) [e1, e2]
     X.ModPlus -> go03 $ \e1 e2 e3 -> Y.Call (Y.Function "jikka::mod::plus" []) [e1, e2, e3]
@@ -260,295 +305,140 @@
     X.ModMult -> go03 $ \e1 e2 e3 -> Y.Call (Y.Function "jikka::mod::mult" []) [e1, e2, e3]
     X.ModInv -> go02 $ \e1 e2 -> Y.Call (Y.Function "jikka::mod::inv" []) [e1, e2]
     X.ModPow -> go03 $ \e1 e2 e3 -> Y.Call (Y.Function "jikka::mod::pow" []) [e1, e2, e3]
-    X.ModMatAp h w -> go03 $ \f x m -> Y.Call (Y.Function "jikka::modmat::ap" [Y.TyIntValue (fromIntegral h), Y.TyIntValue (fromIntegral w)]) [f, x, m]
-    X.ModMatAdd h w -> go03 $ \f g m -> Y.Call (Y.Function "jikka::modmat::add" [Y.TyIntValue (fromIntegral h), Y.TyIntValue (fromIntegral w)]) [f, g, m]
-    X.ModMatMul h n w -> go03 $ \f g m -> Y.Call (Y.Function "jikka::modmat::mul" [Y.TyIntValue (fromIntegral h), Y.TyIntValue (fromIntegral n), Y.TyIntValue (fromIntegral w)]) [f, g, m]
-    X.ModMatPow n -> go03 $ \f k m -> Y.Call (Y.Function "jikka::modmat::pow" [Y.TyIntValue (fromIntegral n)]) [f, k, m]
+    X.ModMatAp h w -> go03 $ \f x m -> Y.Call (Y.Function "jikka::modmat::ap" [Y.TyIntValue h, Y.TyIntValue w]) [f, x, m]
+    X.ModMatAdd h w -> go03 $ \f g m -> Y.Call (Y.Function "jikka::modmat::add" [Y.TyIntValue h, Y.TyIntValue w]) [f, g, m]
+    X.ModMatMul h n w -> go03 $ \f g m -> Y.Call (Y.Function "jikka::modmat::mul" [Y.TyIntValue h, Y.TyIntValue n, Y.TyIntValue w]) [f, g, m]
+    X.ModMatPow n -> go03 $ \f k m -> Y.Call (Y.Function "jikka::modmat::pow" [Y.TyIntValue n]) [f, k, m]
     -- list functions
     X.Cons -> go12' $ \t x xs -> do
       ys <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare (Y.TyVector t) ys Y.DeclareDefault,
-            Y.callMethod' (Y.Var ys) "push_back" [x],
-            Y.callMethod' (Y.Var ys) "insert" [Y.end (Y.Var ys), Y.begin xs, Y.end xs]
-          ],
-          Y.Var ys
-        )
+      useStatement $ Y.Declare (Y.TyVector t) ys Y.DeclareDefault
+      useStatement $ Y.callMethod' (Y.Var ys) "push_back" [x]
+      useStatement $ Y.callMethod' (Y.Var ys) "insert" [Y.end (Y.Var ys), Y.begin xs, Y.end xs]
+      return $ Y.Var ys
     X.Snoc -> go12' $ \t xs x -> do
       ys <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare (Y.TyVector t) ys (Y.DeclareCopy xs),
-            Y.callMethod' (Y.Var ys) "push_back" [x]
-          ],
-          Y.Var ys
-        )
-    X.Foldl -> go23'' $ \t1 t2 f init xs -> do
-      (stmtsInit, init) <- runExpr env init
-      (stmtsXs, xs) <- runExpr env xs
-      t1 <- runType t1
-      t2 <- runType t2
-      y <- Y.newFreshName Y.LocalNameKind
-      x <- Y.newFreshName Y.LocalNameKind
-      (stmtsF, body, f) <- runExprFunction2 env f (Y.Var y) (Y.Var x)
-      return
-        ( stmtsInit ++ stmtsXs
-            ++ [Y.Declare t2 y (Y.DeclareCopy init)]
-            ++ stmtsF
-            ++ [ Y.ForEach
-                   t1
-                   x
-                   xs
-                   (body ++ [Y.assignSimple y f])
-               ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare (Y.TyVector t) ys (Y.DeclareCopy xs)
+      useStatement $ Y.callMethod' (Y.Var ys) "push_back" [x]
+      return $ Y.Var ys
+    X.Foldl -> go23'' $ runFoldl env
     X.Scanl -> go23'' $ \_ t2 f init xs -> do
-      (stmtsInit, init) <- runExpr env init
-      (stmtsXs, xs) <- runExpr env xs
+      init <- runExpr env init
+      xs <- runExpr env xs
       t2 <- runType t2
       ys <- Y.newFreshName Y.LocalNameKind
       i <- Y.newFreshName Y.LoopCounterNameKind
       (stmtsF, body, f) <- runExprFunction2 env f (Y.at (Y.Var ys) (Y.Var i)) (Y.at xs (Y.Var i))
-      return
-        ( stmtsInit ++ stmtsXs
-            ++ [ Y.Declare (Y.TyVector t2) ys (Y.DeclareCopy (Y.vecCtor t2 [Y.incrExpr (Y.size xs)])),
-                 Y.assignAt ys (Y.litInt32 0) init
-               ]
-            ++ stmtsF
-            ++ [ Y.repStatement
-                   i
-                   (Y.cast Y.TyInt32 (Y.size xs))
-                   (body ++ [Y.assignAt ys (Y.incrExpr (Y.Var i)) f])
-               ],
-          Y.Var ys
-        )
+      useStatement $ Y.Declare (Y.TyVector t2) ys (Y.DeclareCopy (Y.vecCtor t2 [Y.incrExpr (Y.size xs)]))
+      useStatement $ Y.assignAt ys (Y.litInt32 0) init
+      useStatements stmtsF
+      useStatement $ Y.repStatement i (Y.cast Y.TyInt32 (Y.size xs)) (body ++ [Y.assignAt ys (Y.incrExpr (Y.Var i)) f])
+      return $ Y.Var ys
     X.Build -> go13'' $ \t f xs n -> do
-      (stmtsInit, xs) <- runExpr env xs
-      (stmtsXs, n) <- runExpr env n
+      xs <- runExpr env xs
+      n <- runExpr env n
       t <- runType t
       ys <- Y.newFreshName Y.LocalNameKind
       i <- Y.newFreshName Y.LoopCounterNameKind
       (stmtsF, body, f) <- runExprFunction env f (Y.Var ys)
-      return
-        ( stmtsInit ++ stmtsXs
-            ++ [ Y.Declare (Y.TyVector t) ys (Y.DeclareCopy xs)
-               ]
-            ++ stmtsF
-            ++ [ Y.repStatement
-                   i
-                   (Y.cast Y.TyInt32 n)
-                   (body ++ [Y.callMethod' (Y.Var ys) "push_back" [f]])
-               ],
-          Y.Var ys
-        )
+      useStatement $ Y.Declare (Y.TyVector t) ys (Y.DeclareCopy xs)
+      useStatements stmtsF
+      useStatement $ Y.repStatement i (Y.cast Y.TyInt32 n) (body ++ [Y.callMethod' (Y.Var ys) "push_back" [f]])
+      return $ Y.Var ys
     X.Len -> go11 $ \_ e -> Y.cast Y.TyInt64 (Y.size e)
-    X.Map -> go22'' $ \_ t2 f xs -> do
-      ys <- Y.newFreshName Y.LocalNameKind
-      t2 <- runType t2
-      stmts <- case (f, xs) of
-        (X.Lam _ _ (X.Lit lit), X.Range1' n) -> do
-          (stmtsN, n) <- runExpr env n
-          lit <- runLiteral env lit
-          return $
-            stmtsN
-              ++ [Y.Declare (Y.TyVector t2) ys (Y.DeclareCopy (Y.vecCtor t2 [n, lit]))]
-        _ -> do
-          (stmtsXs, xs) <- runExpr env xs
-          i <- Y.newFreshName Y.LoopCounterNameKind
-          (stmtsF, body, f) <- runExprFunction env f (Y.at xs (Y.Var i))
-          return $
-            stmtsXs
-              ++ [Y.Declare (Y.TyVector t2) ys (Y.DeclareCopy (Y.vecCtor t2 [Y.size xs]))]
-              ++ stmtsF
-              ++ [ Y.repStatement
-                     i
-                     (Y.cast Y.TyInt32 (Y.size xs))
-                     (body ++ [Y.assignAt ys (Y.Var i) f])
-                 ]
-      return (stmts, Y.Var ys)
+    X.Map -> go22'' $ runMap env
     X.Filter -> go12'' $ \t f xs -> do
-      (stmtsXs, xs) <- runExpr env xs
+      xs <- runExpr env xs
       t <- runType t
       ys <- Y.newFreshName Y.LocalNameKind
       x <- Y.newFreshName Y.LocalNameKind
       (stmtsF, body, f) <- runExprFunction env f (Y.Var x)
-      return
-        ( stmtsXs
-            ++ [Y.Declare (Y.TyVector t) ys Y.DeclareDefault]
-            ++ stmtsF
-            ++ [ Y.ForEach
-                   t
-                   x
-                   xs
-                   ( body
-                       ++ [ Y.If
-                              f
-                              [Y.callMethod' (Y.Var ys) "push_back" [Y.Var x]]
-                              Nothing
-                          ]
-                   )
-               ],
-          Y.Var ys
-        )
+      useStatement $ Y.Declare (Y.TyVector t) ys Y.DeclareDefault
+      useStatements stmtsF
+      useStatement $ Y.ForEach t x xs (body ++ [Y.If f [Y.callMethod' (Y.Var ys) "push_back" [Y.Var x]] Nothing])
+      return $ Y.Var ys
     X.At -> go12 $ \_ e1 e2 -> Y.at e1 e2
-    X.SetAt -> go13' $ \t xs i x -> do
-      ys <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare (Y.TyVector t) ys (Y.DeclareCopy xs),
-            Y.assignAt ys i x
-          ],
-          Y.Var ys
-        )
+    X.SetAt -> go13 $ \t xs i x -> Y.Call (Y.SetAt t) [xs, i, x]
     X.Elem -> go12' $ \_ xs x -> do
       y <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare Y.TyBool y (Y.DeclareCopy (Y.BinOp Y.NotEqual (Y.callFunction "std::find" [] [Y.begin xs, Y.end xs, x]) (Y.end xs)))
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare Y.TyBool y (Y.DeclareCopy (Y.BinOp Y.NotEqual (Y.callFunction "std::find" [] [Y.begin xs, Y.end xs, x]) (Y.end xs)))
+      return $ Y.Var y
     X.Sum -> go01' $ \xs -> do
       y <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare Y.TyInt64 y (Y.DeclareCopy (Y.callFunction "std::accumulate" [] [Y.begin xs, Y.end xs, Y.litInt64 0]))
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare Y.TyInt64 y (Y.DeclareCopy (Y.callFunction "std::accumulate" [] [Y.begin xs, Y.end xs, Y.litInt64 0]))
+      return $ Y.Var y
     X.ModSum -> go02' $ \xs m -> do
       y <- Y.newFreshName Y.LocalNameKind
       x <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare Y.TyInt64 y (Y.DeclareCopy (Y.litInt64 0)),
-            Y.ForEach
-              Y.TyInt64
-              x
-              xs
-              [Y.Assign (Y.AssignExpr Y.AddAssign (Y.LeftVar y) (Y.callFunction "jikka::floormod" [] [Y.Var x, m]))]
-          ],
-          Y.callFunction "jikka::floormod" [] [Y.Var y, m]
-        )
+      useStatement $ Y.Declare Y.TyInt64 y (Y.DeclareCopy (Y.litInt64 0))
+      useStatement $ Y.ForEach Y.TyInt64 x xs [Y.Assign (Y.AssignExpr Y.AddAssign (Y.LeftVar y) (Y.callFunction "jikka::floormod" [] [Y.Var x, m]))]
+      return $ Y.callFunction "jikka::floormod" [] [Y.Var y, m]
     X.Product -> go01' $ \xs -> do
       y <- Y.newFreshName Y.LocalNameKind
       x <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare Y.TyInt64 y (Y.DeclareCopy (Y.litInt64 1)),
-            Y.ForEach
-              Y.TyInt64
-              x
-              xs
-              [Y.Assign (Y.AssignExpr Y.MulAssign (Y.LeftVar y) (Y.Var x))]
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare Y.TyInt64 y (Y.DeclareCopy (Y.litInt64 1))
+      useStatement $ Y.ForEach Y.TyInt64 x xs [Y.Assign (Y.AssignExpr Y.MulAssign (Y.LeftVar y) (Y.Var x))]
+      return $ Y.Var y
     X.ModProduct -> go02' $ \xs m -> do
       y <- Y.newFreshName Y.LocalNameKind
       x <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare Y.TyInt64 y (Y.DeclareCopy (Y.litInt64 1)),
-            Y.ForEach
-              Y.TyInt64
-              x
-              xs
-              [Y.Assign (Y.AssignExpr Y.SimpleAssign (Y.LeftVar y) (Y.callFunction "jikka::mod::mult" [] [Y.Var y, Y.Var x, m]))]
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare Y.TyInt64 y (Y.DeclareCopy (Y.litInt64 1))
+      useStatement $ Y.ForEach Y.TyInt64 x xs [Y.Assign (Y.AssignExpr Y.SimpleAssign (Y.LeftVar y) (Y.callFunction "jikka::mod::mult" [] [Y.Var y, Y.Var x, m]))]
+      return $ Y.Var y
     X.Min1 -> go11' $ \t xs -> do
       y <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare t y (Y.DeclareCopy (Y.UnOp Y.Deref (Y.callFunction "std::min_element" [] [Y.begin xs, Y.end xs])))
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare t y (Y.DeclareCopy (Y.UnOp Y.Deref (Y.callFunction "std::min_element" [] [Y.begin xs, Y.end xs])))
+      return $ Y.Var y
     X.Max1 -> go11' $ \t xs -> do
       y <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare t y (Y.DeclareCopy (Y.UnOp Y.Deref (Y.callFunction "std::max_element" [] [Y.begin xs, Y.end xs])))
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare t y (Y.DeclareCopy (Y.UnOp Y.Deref (Y.callFunction "std::max_element" [] [Y.begin xs, Y.end xs])))
+      return $ Y.Var y
     X.ArgMin -> go11' $ \t xs -> do
       y <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare t y (Y.DeclareCopy (Y.BinOp Y.Sub (Y.callFunction "std::min_element" [] [Y.begin xs, Y.end xs]) (Y.begin xs)))
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare t y (Y.DeclareCopy (Y.BinOp Y.Sub (Y.callFunction "std::min_element" [] [Y.begin xs, Y.end xs]) (Y.begin xs)))
+      return $ Y.Var y
     X.ArgMax -> go11' $ \t xs -> do
       y <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare t y (Y.DeclareCopy (Y.BinOp Y.Sub (Y.callFunction "std::max_element" [] [Y.begin xs, Y.end xs]) (Y.begin xs)))
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare t y (Y.DeclareCopy (Y.BinOp Y.Sub (Y.callFunction "std::max_element" [] [Y.begin xs, Y.end xs]) (Y.begin xs)))
+      return $ Y.Var y
     X.Gcd1 -> go11' $ \t xs -> do
       y <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare t y (Y.DeclareCopy (Y.UnOp Y.Deref (Y.callFunction "std::accumulate" [] [Y.begin xs, Y.end xs, Y.litInt64 0, Y.Lam [(Y.TyAuto, Y.VarName "a"), (Y.TyAuto, Y.VarName "b")] Y.TyAuto [Y.Return $ Y.callFunction "std::gcd" [] [Y.Var $ Y.VarName "a", Y.Var $ Y.VarName "b"]]])))
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare t y (Y.DeclareCopy (Y.UnOp Y.Deref (Y.callFunction "std::accumulate" [] [Y.begin xs, Y.end xs, Y.litInt64 0, Y.Lam [(Y.TyAuto, Y.VarName "a"), (Y.TyAuto, Y.VarName "b")] Y.TyAuto [Y.Return $ Y.callFunction "std::gcd" [] [Y.Var $ Y.VarName "a", Y.Var $ Y.VarName "b"]]])))
+      return $ Y.Var y
     X.Lcm1 -> go11' $ \t xs -> do
       y <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare t y (Y.DeclareCopy (Y.UnOp Y.Deref (Y.callFunction "std::accumulate" [] [Y.begin xs, Y.end xs, Y.litInt64 1, Y.Lam [(Y.TyAuto, Y.VarName "a"), (Y.TyAuto, Y.VarName "b")] Y.TyAuto [Y.Return $ Y.callFunction "std::lcm" [] [Y.Var $ Y.VarName "a", Y.Var $ Y.VarName "b"]]])))
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare t y (Y.DeclareCopy (Y.UnOp Y.Deref (Y.callFunction "std::accumulate" [] [Y.begin xs, Y.end xs, Y.litInt64 1, Y.Lam [(Y.TyAuto, Y.VarName "a"), (Y.TyAuto, Y.VarName "b")] Y.TyAuto [Y.Return $ Y.callFunction "std::lcm" [] [Y.Var $ Y.VarName "a", Y.Var $ Y.VarName "b"]]])))
+      return $ Y.Var y
     X.All -> go01' $ \xs -> do
       y <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare Y.TyBool y (Y.DeclareCopy (Y.BinOp Y.Equal (Y.callFunction "std::find" [] [Y.begin xs, Y.end xs, Y.Lit (Y.LitBool False)]) (Y.end xs)))
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare Y.TyBool y (Y.DeclareCopy (Y.BinOp Y.Equal (Y.callFunction "std::find" [] [Y.begin xs, Y.end xs, Y.Lit (Y.LitBool False)]) (Y.end xs)))
+      return $ Y.Var y
     X.Any -> go01' $ \xs -> do
       y <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare Y.TyBool y (Y.DeclareCopy (Y.BinOp Y.NotEqual (Y.callFunction "std::find" [] [Y.begin xs, Y.end xs, Y.Lit (Y.LitBool True)]) (Y.end xs)))
-          ],
-          Y.Var y
-        )
+      useStatement $ Y.Declare Y.TyBool y (Y.DeclareCopy (Y.BinOp Y.NotEqual (Y.callFunction "std::find" [] [Y.begin xs, Y.end xs, Y.Lit (Y.LitBool True)]) (Y.end xs)))
+      return $ Y.Var y
     X.Sorted -> go11' $ \t xs -> do
       ys <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare (Y.TyVector t) ys (Y.DeclareCopy xs),
-            Y.callFunction' "std::sort" [] [Y.begin (Y.Var ys), Y.end (Y.Var ys)]
-          ],
-          Y.Var ys
-        )
+      useStatement $ Y.Declare (Y.TyVector t) ys (Y.DeclareCopy xs)
+      useStatement $ Y.callFunction' "std::sort" [] [Y.begin (Y.Var ys), Y.end (Y.Var ys)]
+      return $ Y.Var ys
     X.Reversed -> go11' $ \t xs -> do
       ys <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare (Y.TyVector t) ys (Y.DeclareCopy xs),
-            Y.callFunction' "std::reverse" [] [Y.begin (Y.Var ys), Y.end (Y.Var ys)]
-          ],
-          Y.Var ys
-        )
+      useStatement $ Y.Declare (Y.TyVector t) ys (Y.DeclareCopy xs)
+      useStatement $ Y.callFunction' "std::reverse" [] [Y.begin (Y.Var ys), Y.end (Y.Var ys)]
+      return $ Y.Var ys
     X.Range1 -> go01 $ \n -> Y.Call Y.Range [n]
     X.Range2 -> go02' $ \from to -> do
       ys <- Y.newFreshName Y.LocalNameKind
-      return
-        ( [ Y.Declare (Y.TyVector Y.TyInt64) ys (Y.DeclareCopy (Y.vecCtor Y.TyInt64 [Y.BinOp Y.Sub to from])),
-            Y.callFunction' "std::iota" [] [Y.begin (Y.Var ys), Y.end (Y.Var ys), from]
-          ],
-          Y.Var ys
-        )
+      useStatement $ Y.Declare (Y.TyVector Y.TyInt64) ys (Y.DeclareCopy (Y.vecCtor Y.TyInt64 [Y.BinOp Y.Sub to from]))
+      useStatement $ Y.callFunction' "std::iota" [] [Y.begin (Y.Var ys), Y.end (Y.Var ys), from]
+      return $ Y.Var ys
     X.Range3 -> go03' $ \from to step -> do
       ys <- Y.newFreshName Y.LocalNameKind
       i <- Y.newFreshName Y.LoopCounterNameKind
-      return
-        ( [ Y.Declare (Y.TyVector Y.TyInt64) ys Y.DeclareDefault,
-            Y.For
-              Y.TyInt32
-              i
-              from
-              (Y.BinOp Y.LessThan (Y.Var i) to)
-              (Y.AssignExpr Y.AddAssign (Y.LeftVar i) step)
-              [ Y.callMethod' (Y.Var ys) "push_back" [Y.Var i]
-              ]
-          ],
-          Y.Var ys
-        )
+      useStatement $ Y.Declare (Y.TyVector Y.TyInt64) ys Y.DeclareDefault
+      useStatement $ Y.For Y.TyInt32 i from (Y.BinOp Y.LessThan (Y.Var i) to) (Y.AssignExpr Y.AddAssign (Y.LeftVar i) step) [Y.callMethod' (Y.Var ys) "push_back" [Y.Var i]]
+      return $ Y.Var ys
     -- tuple functions
     X.Tuple -> goNN $ \ts es ->
       if Y.shouldBeArray ts
@@ -556,7 +446,7 @@
         else Y.Call (Y.StdTuple ts) es
     X.Proj n -> goN1 $ \ts e ->
       if Y.shouldBeArray ts
-        then Y.at e (Y.Lit (Y.LitInt32 (fromIntegral n)))
+        then Y.at e (Y.Lit (Y.LitInt32 n))
         else Y.Call (Y.StdGet (toInteger n)) [e]
     -- comparison
     X.LessThan -> go12 $ \_ e1 e2 -> Y.BinOp Y.LessThan e1 e2
@@ -582,12 +472,12 @@
 runExprFunction env f e = case f of
   X.Lam x t body -> do
     y <- renameVarName' Y.LocalArgumentNameKind x
-    (stmts, body) <- runExpr ((x, t, y) : env) body
+    (stmts, body) <- runStatementsT $ runExpr ((x, t, y) : env) body
     let stmts' = map (Y.replaceStatement y e) stmts
     let body' = Y.replaceExpr y e body
     return ([], stmts', body')
   f -> do
-    (stmts, f) <- runExpr env f
+    (stmts, f) <- runStatementsT $ runExpr env f
     return (stmts, [], Y.CallExpr f [e])
 
 runExprFunction2 :: (MonadAlpha m, MonadError Error m) => Env -> X.Expr -> Y.Expr -> Y.Expr -> m ([Y.Statement], [Y.Statement], Y.Expr)
@@ -595,22 +485,36 @@
   X.Lam2 x1 t1 x2 t2 body -> do
     y1 <- renameVarName' Y.LocalArgumentNameKind x1
     y2 <- renameVarName' Y.LocalArgumentNameKind x2
-    (stmts, body) <- runExpr ((x2, t2, y2) : (x1, t1, y1) : env) body
+    (stmts, body) <- runStatementsT $ runExpr ((x2, t2, y2) : (x1, t1, y1) : env) body
     let stmts' = map (Y.replaceStatement y2 e2 . Y.replaceStatement y1 e1) stmts
     let body' = Y.replaceExpr y2 e2 $ Y.replaceExpr y1 e1 body
     return ([], stmts', body')
   f -> do
-    (stmts, f) <- runExpr env f
+    (stmts, f) <- runStatementsT $ runExpr env f
     return (stmts, [], Y.CallExpr (Y.CallExpr f [e1]) [e2])
 
-runExpr :: (MonadAlpha m, MonadError Error m) => Env -> X.Expr -> m ([Y.Statement], Y.Expr)
+runAssert :: (MonadStatements m, MonadAlpha m, MonadError Error m) => Env -> X.Expr -> m ()
+runAssert env = \case
+  -- optimize @assert all(...)@
+  X.All' (X.Map' t _ f xs) -> do
+    t <- runType t
+    y <- Y.newFreshName Y.LocalNameKind
+    xs <- runExpr env xs
+    (stmtsF, body, e) <- runExprFunction env f (Y.Var y)
+    useStatements stmtsF
+    useStatement $ Y.ForEach t y xs (body ++ [Y.Assert e])
+  -- other cases
+  e -> do
+    e <- runExpr env e
+    useStatement $ Y.Assert e
+
+runExpr :: (MonadStatements m, MonadAlpha m, MonadError Error m) => Env -> X.Expr -> m Y.Expr
 runExpr env = \case
   X.Var x -> do
     y <- lookupVarName env x
-    return ([], Y.Var y)
+    return $ Y.Var y
   X.Lit lit -> do
-    lit <- runLiteral env lit
-    return ([], lit)
+    runLiteral env lit
   e@(X.App _ _) -> do
     let (f, args) = X.curryApp e
     case f of
@@ -623,40 +527,39 @@
             ret <- runType ret
             xs <- replicateM (arity - length args) X.genVarName'
             ys <- mapM (renameVarName' Y.LocalArgumentNameKind) xs
-            (stmts, e) <- runAppBuiltin env builtin bts (args ++ map X.Var xs)
+            e <- runAppBuiltin env builtin bts (args ++ map X.Var xs)
             let (_, e') = foldr (\(t, y) (ret, e) -> (Y.TyFunction ret [t], Y.Lam [(t, y)] ret [Y.Return e])) (ret, e) (zip (drop (length args) ts) ys)
-            return (stmts, e')
+            return e'
           else
             if length args == arity
               then do
                 runAppBuiltin env builtin bts args
               else do
-                (stmts, e) <- runAppBuiltin env builtin bts (take arity args)
-                args <- mapM (runExpr env) (drop arity args)
-                return (concatMap fst args ++ stmts, Y.CallExpr e (map snd args))
+                args' <- mapM (runExpr env) (drop arity args)
+                e <- runAppBuiltin env builtin bts (take arity args)
+                return $ Y.CallExpr e args'
       _ -> do
+        f <- runExpr env f
         args <- mapM (runExpr env) args
-        (stmts, f) <- runExpr env f
-        return (stmts ++ concatMap fst args, Y.CallExpr f (map snd args))
+        return $ Y.CallExpr f args
   e@(X.Lam _ _ _) -> do
     let (args, body) = X.uncurryLam e
     ys <- mapM (renameVarName' Y.LocalArgumentNameKind . fst) args
     let env' = reverse (zipWith (\(x, t) y -> (x, t, y)) args ys) ++ env
     ret <- runType =<< typecheckExpr env' body
-    (stmts, body) <- runExpr env' body
+    (stmts, body) <- runStatementsT $ runExpr env' body
     ts <- mapM (runType . snd) args
     let (_, [Y.Return e]) = foldr (\(t, y) (ret, body) -> (Y.TyFunction ret [t], [Y.Return (Y.Lam [(t, y)] ret body)])) (ret, stmts ++ [Y.Return body]) (zip ts ys)
-    return ([], e)
+    return e
   X.Let x t e1 e2 -> do
     y <- renameVarName' Y.LocalNameKind x
     t' <- runType t
-    (stmts1, e1) <- runExpr env e1
-    (stmts2, e2) <- runExpr ((x, t, y) : env) e2
-    return (stmts1 ++ Y.Declare t' y (Y.DeclareCopy e1) : stmts2, e2)
+    e1 <- runExpr env e1
+    useStatement $ Y.Declare t' y (Y.DeclareCopy e1)
+    runExpr ((x, t, y) : env) e2
   X.Assert e1 e2 -> do
-    (stmts1, e1) <- runExpr env e1
-    (stmts2, e2) <- runExpr env e2
-    return (stmts1 ++ Y.Assert e1 : stmts2, e2)
+    runAssert env e1
+    runExpr env e2
 
 runToplevelFunDef :: (MonadAlpha m, MonadError Error m) => Env -> Y.VarName -> [(X.VarName, X.Type)] -> X.Type -> X.Expr -> m [Y.ToplevelStatement]
 runToplevelFunDef env f args ret body = do
@@ -664,7 +567,7 @@
   args <- forM args $ \(x, t) -> do
     y <- renameVarName' Y.ArgumentNameKind x
     return (x, t, y)
-  (stmts, result) <- runExpr (reverse args ++ env) body
+  (stmts, result) <- runStatementsT $ runExpr (reverse args ++ env) body
   args <- forM args $ \(_, t, y) -> do
     t <- runType t
     return (t, y)
@@ -673,7 +576,7 @@
 runToplevelVarDef :: (MonadAlpha m, MonadError Error m) => Env -> Y.VarName -> X.Type -> X.Expr -> m [Y.ToplevelStatement]
 runToplevelVarDef env x t e = do
   t <- runType t
-  (stmts, e) <- runExpr env e
+  (stmts, e) <- runStatementsT $ runExpr env e
   case stmts of
     [] -> return [Y.VarDef t x e]
     _ -> return [Y.VarDef t x (Y.CallExpr (Y.Lam [] t (stmts ++ [Y.Return e])) [])]
@@ -691,7 +594,7 @@
             args <- forM args $ \(x, t) -> do
               y <- renameVarName' Y.ArgumentNameKind x
               return (x, t, y)
-            (stmts, e) <- runExpr (reverse args ++ env) body
+            (stmts, e) <- runStatementsT $ runExpr (reverse args ++ env) body
             let body = stmts ++ [Y.Return e]
             args' <- forM args $ \(_, t, y) -> do
               t <- runType t
@@ -702,7 +605,7 @@
               t <- runType t
               y <- Y.newFreshName Y.ArgumentNameKind
               return (t, y)
-            (stmts, e) <- runExpr env e
+            (stmts, e) <- runStatementsT $ runExpr env e
             let body = stmts ++ [Y.Return (Y.CallExpr e (map (Y.Var . snd) args))]
             return (args, body)
         ret <- runType ret
@@ -734,7 +637,7 @@
     cont <- runToplevelExpr ((f, t, g) : env) cont
     return $ stmt ++ cont
   X.ToplevelAssert e cont -> do
-    (stmts, e) <- runExpr env e
+    (stmts, e) <- runStatementsT $ runExpr env e
     let stmt = Y.StaticAssert (Y.CallExpr (Y.Lam [] Y.TyBool (stmts ++ [Y.Return e])) []) ""
     cont <- runToplevelExpr env cont
     return $ stmt : cont
diff --git a/src/Jikka/CPlusPlus/Convert/InlineSetAt.hs b/src/Jikka/CPlusPlus/Convert/InlineSetAt.hs
new file mode 100644
--- /dev/null
+++ b/src/Jikka/CPlusPlus/Convert/InlineSetAt.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+
+-- |
+-- Module      : Jikka.CPlusPlus.Convert.InlineSetAt
+-- Description : does inline expansion of @set_at@ function. / @set_at@ 関数を inline 展開します。
+-- Copyright   : (c) Kimiyuki Onaka, 2020
+-- License     : Apache License 2.0
+-- Maintainer  : kimiyuki95@gmail.com
+-- Stability   : experimental
+-- Portability : portable
+module Jikka.CPlusPlus.Convert.InlineSetAt
+  ( run,
+  )
+where
+
+import Control.Monad.Writer.Strict
+import Jikka.CPlusPlus.Language.Expr
+import Jikka.CPlusPlus.Language.Util
+import Jikka.Common.Alpha
+import Jikka.Common.Error
+
+runExpr :: (MonadAlpha m, MonadWriter [Statement] m) => Expr -> m Expr
+runExpr = \case
+  Call (SetAt t) [xs, i, x] -> do
+    y <- case xs of
+      Var (VarName xs) -> renameVarName LocalNameKind xs
+      _ -> newFreshName LocalNameKind
+    tell
+      [ Declare (TyVector t) y (DeclareCopy xs),
+        Assign (AssignExpr SimpleAssign (LeftAt (LeftVar y) i) x)
+      ]
+    return (Var y)
+  e -> return e
+
+runStatement :: MonadAlpha m => Statement -> m [Statement]
+runStatement stmt = do
+  (stmt, decls) <- runWriterT (mapDirectExprStatementM (mapSubExprM runExpr) stmt)
+  return $ decls ++ [stmt]
+
+runProgram :: MonadAlpha m => Program -> m Program
+runProgram = mapExprStatementProgramM return runStatement
+
+-- | `run` does inline expansion of @jikka::set_at<T>(...)@ function.
+--
+-- == Examples
+--
+-- Before:
+--
+-- > func(jikka::set_at<T>(xs, i, x));
+--
+-- After:
+--
+-- > vector<int> ys = xs;
+-- > ys[i] = x;
+-- > func(ys);
+run :: (MonadAlpha m, MonadError Error m) => Program -> m Program
+run prog = wrapError' "Jikka.CPlusPlus.Convert.InlineSetAt" $ do
+  runProgram prog
diff --git a/src/Jikka/CPlusPlus/Convert/MoveSemantics.hs b/src/Jikka/CPlusPlus/Convert/MoveSemantics.hs
--- a/src/Jikka/CPlusPlus/Convert/MoveSemantics.hs
+++ b/src/Jikka/CPlusPlus/Convert/MoveSemantics.hs
@@ -51,21 +51,38 @@
   AssignIncr e -> AssignIncr <$> runLeftExpr e
   AssignDecr e -> AssignDecr <$> runLeftExpr e
 
-isMovableTo :: VarName -> VarName -> [[Statement]] -> Bool
-isMovableTo x y cont
-  | x `S.notMember` readList' (analyzeStatements (concat cont)) = True
+data CopyType
+  = SimpleCopy
+  | UpdatedCopy
+  deriving (Eq, Ord, Show, Read, Enum, Bounded)
+
+-- | @isMovableTo x y env cont@ checkes whether @x@ is movable to @y@ instead of copying, under a context @env@ and @cont@.
+-- @x@ is already replaced by the mapping of @env@, but @y@ and @cont@ are not yet.
+isMovableTo :: VarName -> VarName -> CopyType -> M.Map VarName VarName -> [[Statement]] -> Bool
+isMovableTo x y0 typ env cont
+  | x `S.notMember` readList' (analyzeStatements' (concat cont)) = True -- @x@ is movable if @x@ is not used after the current position
   | otherwise =
     let go = \case
           [] -> False
-          (Assign (AssignExpr SimpleAssign (LeftVar x') (Var y')) : cont')
-            | x' == x && y' == y ->
-              let ReadWriteList _ ws' = analyzeStatements cont'
-                  ReadWriteList rs ws = analyzeStatements (concat (tail cont))
+          (Assign (AssignExpr SimpleAssign (LeftVar x') (Var _)) : cont')
+            | x' == x -> -- re-assignment to @x@
+              let ReadWriteList _ ws' = analyzeStatements' cont'
+                  ReadWriteList rs ws = analyzeStatements' (concat (tail cont))
                in y `S.notMember` S.unions [ws', rs, ws]
           (stmt : cont) ->
-            let ReadWriteList rs ws = analyzeStatement stmt
-             in x `S.notMember` S.unions [rs, ws] && go cont
-     in go (head cont)
+            let ReadWriteList rs ws = analyzeStatement' stmt
+                rws = if typ == SimpleCopy then ws else S.union rs ws -- Reading @x@ is okay when it's a copy without updating.
+             in x `S.notMember` rws && go cont -- @x@ is used
+     in go (head cont) -- @x@ is movable if @x@ is unused until a next re-assignment
+  where
+    y :: VarName
+    y = fromMaybe y0 (M.lookup y0 env)
+    applyEnv :: ReadWriteList -> ReadWriteList
+    applyEnv (ReadWriteList rs ws) =
+      let f = S.map (\x -> fromMaybe x (M.lookup x env))
+       in ReadWriteList (f rs) (f ws)
+    analyzeStatements' = applyEnv . analyzeStatements
+    analyzeStatement' = applyEnv . analyzeStatement
 
 runStatement :: MonadState (M.Map VarName VarName) m => Statement -> [[Statement]] -> m [Statement]
 runStatement stmt cont = case stmt of
@@ -98,17 +115,22 @@
       DeclareDefault -> return DeclareDefault
       DeclareCopy e -> DeclareCopy <$> runExpr e
       DeclareInitialize es -> DeclareInitialize <$> mapM runExpr es
+    env <- get
     case init of
-      DeclareCopy (Var x) | (x `isMovableTo` y) cont -> do
+      DeclareCopy (Var x) | (x `isMovableTo` y) SimpleCopy env cont -> do
         modify' (M.insert y x)
         return []
+      DeclareCopy (Call (SetAt _) [Var x, i, xi])
+        | (x `isMovableTo` y) UpdatedCopy env cont -> do
+          modify' (M.insert y x)
+          return [Assign (AssignExpr SimpleAssign (LeftAt (LeftVar x) i) xi)]
       DeclareCopy (Call ConvexHullTrickCtor []) -> return [Declare t y DeclareDefault]
       DeclareCopy (Call ConvexHullTrickCopyAddLine [Var x, a, b])
-        | (x `isMovableTo` y) cont -> do
+        | (x `isMovableTo` y) UpdatedCopy env cont -> do
           modify' (M.insert y x)
           return [callMethod' (Var x) "add_line" [a, b]]
       DeclareCopy (Call (SegmentTreeCopySetPoint _) [Var x, i, a])
-        | (x `isMovableTo` y) cont -> do
+        | (x `isMovableTo` y) UpdatedCopy env cont -> do
           modify' (M.insert y x)
           return [callMethod' (Var x) "set" [i, a]]
       _ -> do
@@ -118,17 +140,24 @@
     return [DeclareDestructure xs e]
   Assign e -> do
     e <- runAssignExpr e
+    env <- get
     case e of
       AssignExpr SimpleAssign (LeftVar y) (Var x) | x == y -> return []
+      AssignExpr SimpleAssign (LeftVar y) (Call (SetAt _) [Var x, i, xi])
+        | x == y -> return [Assign (AssignExpr SimpleAssign (LeftAt (LeftVar x) i) xi)]
+        | (x `isMovableTo` y) UpdatedCopy env cont -> do
+          modify' (M.insert y x)
+          return [Assign (AssignExpr SimpleAssign (LeftAt (LeftVar x) i) xi)]
+        | otherwise -> return [Assign e]
       AssignExpr SimpleAssign (LeftVar y) (Call ConvexHullTrickCopyAddLine [Var x, a, b])
         | x == y -> return [callMethod' (Var x) "add_line" [a, b]]
-        | (x `isMovableTo` y) cont -> do
+        | (x `isMovableTo` y) UpdatedCopy env cont -> do
           modify' (M.insert y x)
           return [callMethod' (Var x) "add_line" [a, b]]
         | otherwise -> return [Assign e]
       AssignExpr SimpleAssign (LeftVar y) (Call (SegmentTreeCopySetPoint _) [Var x, i, a])
         | x == y -> return [callMethod' (Var x) "set" [i, a]]
-        | (x `isMovableTo` y) cont -> do
+        | (x `isMovableTo` y) UpdatedCopy env cont -> do
           modify' (M.insert y x)
           return [callMethod' (Var x) "set" [i, a]]
         | otherwise -> return [Assign e]
diff --git a/src/Jikka/CPlusPlus/Convert/OptimizeRange.hs b/src/Jikka/CPlusPlus/Convert/OptimizeRange.hs
--- a/src/Jikka/CPlusPlus/Convert/OptimizeRange.hs
+++ b/src/Jikka/CPlusPlus/Convert/OptimizeRange.hs
@@ -30,7 +30,7 @@
   stmt -> return stmt
 
 runProgram :: Monad m => Program -> m Program
-runProgram = mapExprStatementProgramM runExpr runStatement
+runProgram = mapExprStatementProgramM runExpr (((: []) <$>) . runStatement)
 
 -- | `run` replaces superfluous copying.
 --
diff --git a/src/Jikka/CPlusPlus/Convert/UseInitialization.hs b/src/Jikka/CPlusPlus/Convert/UseInitialization.hs
--- a/src/Jikka/CPlusPlus/Convert/UseInitialization.hs
+++ b/src/Jikka/CPlusPlus/Convert/UseInitialization.hs
@@ -30,7 +30,7 @@
   stmt -> stmt
 
 runProgram :: Program -> Program
-runProgram = mapExprStatementProgram id runStatement
+runProgram = mapExprStatementProgram id ((: []) . runStatement)
 
 -- | `run` unpack tuples.
 --
diff --git a/src/Jikka/CPlusPlus/Format.hs b/src/Jikka/CPlusPlus/Format.hs
--- a/src/Jikka/CPlusPlus/Format.hs
+++ b/src/Jikka/CPlusPlus/Format.hs
@@ -239,6 +239,7 @@
                   e2' = formatExpr' ParenPrec e2
                in (e1' ++ "[" ++ e2' ++ "]", FunCallPrec)
             _ -> error $ "Jikka.CPlusPlus.Language.Format.formatExpr: wrong number of arguments for subscription: " ++ show (length args)
+          SetAt t -> call $ "jikka::set_at<" ++ formatType t ++ ">"
           Cast t -> call $ formatType t
           StdTuple ts -> call $ "std::tuple<" ++ intercalate ", " (map formatType ts) ++ ">"
           StdGet n -> call $ "std::get<" ++ show n ++ ">"
diff --git a/src/Jikka/CPlusPlus/Language/Expr.hs b/src/Jikka/CPlusPlus/Language/Expr.hs
--- a/src/Jikka/CPlusPlus/Language/Expr.hs
+++ b/src/Jikka/CPlusPlus/Language/Expr.hs
@@ -78,6 +78,8 @@
     Method FunName
   | -- | subscription @e1[e2]@
     At
+  | -- | updated array @auto tmp = e1; tmp[e2] = e3; return tmp;@
+    SetAt Type
   | -- | cast @(T)e@
     Cast Type
   | -- | functio @std::tuple\<T1, T2, ...\>(e1, e2, ...)@
diff --git a/src/Jikka/CPlusPlus/Language/Util.hs b/src/Jikka/CPlusPlus/Language/Util.hs
--- a/src/Jikka/CPlusPlus/Language/Util.hs
+++ b/src/Jikka/CPlusPlus/Language/Util.hs
@@ -4,7 +4,7 @@
 module Jikka.CPlusPlus.Language.Util where
 
 import Control.Monad.Identity
-import Data.Char (isAlphaNum)
+import Data.Char (isAlphaNum, isNumber)
 import qualified Data.Set as S
 import Jikka.CPlusPlus.Language.Expr
 import Jikka.Common.Alpha
@@ -39,7 +39,8 @@
 renameVarName :: MonadAlpha m => NameKind -> String -> m VarName
 renameVarName kind hint = do
   i <- nextCounter
-  let prefix = case takeWhile (\c -> isAlphaNum c || c == '_') hint of
+  let f = reverse . dropWhile (\c -> isNumber c || c == '_') . reverse . takeWhile (\c -> isAlphaNum c || c == '_')
+  let prefix = case f hint of
         "" -> fromNameKind kind
         hint' -> hint' ++ "_"
   return (VarName (prefix ++ show i))
@@ -147,7 +148,7 @@
 end :: Expr -> Expr
 end e = Call (Method "end") [e]
 
-mapExprStatementExprM :: Monad m => (Expr -> m Expr) -> (Statement -> m Statement) -> Expr -> m Expr
+mapExprStatementExprM :: Monad m => (Expr -> m Expr) -> (Statement -> m [Statement]) -> Expr -> m Expr
 mapExprStatementExprM f g = go
   where
     go = \case
@@ -156,33 +157,34 @@
       UnOp op e -> f . UnOp op =<< go e
       BinOp op e1 e2 -> f =<< (BinOp op <$> go e1 <*> go e2)
       Cond e1 e2 e3 -> f =<< (Cond <$> go e1 <*> go e2 <*> go e3)
-      Lam args ret body -> f . Lam args ret =<< mapM (mapExprStatementStatementM f g) body
+      Lam args ret body -> f . Lam args ret . concat =<< mapM (mapExprStatementStatementM f g) body
       Call g args -> f . Call g =<< mapM go args
       CallExpr g args -> f =<< (CallExpr <$> go g <*> mapM go args)
 
-mapExprStatementLeftExprM :: Monad m => (Expr -> m Expr) -> (Statement -> m Statement) -> LeftExpr -> m LeftExpr
+mapExprStatementLeftExprM :: Monad m => (Expr -> m Expr) -> (Statement -> m [Statement]) -> LeftExpr -> m LeftExpr
 mapExprStatementLeftExprM f g = \case
   LeftVar x -> return $ LeftVar x
   LeftAt e1 e2 -> LeftAt <$> mapExprStatementLeftExprM f g e1 <*> mapExprStatementExprM f g e2
   LeftGet n e -> LeftGet n <$> mapExprStatementLeftExprM f g e
 
-mapExprStatementAssignExprM :: Monad m => (Expr -> m Expr) -> (Statement -> m Statement) -> AssignExpr -> m AssignExpr
+mapExprStatementAssignExprM :: Monad m => (Expr -> m Expr) -> (Statement -> m [Statement]) -> AssignExpr -> m AssignExpr
 mapExprStatementAssignExprM f g = \case
   AssignExpr op e1 e2 -> AssignExpr op <$> mapExprStatementLeftExprM f g e1 <*> mapExprStatementExprM f g e2
   AssignIncr e -> AssignIncr <$> mapExprStatementLeftExprM f g e
   AssignDecr e -> AssignDecr <$> mapExprStatementLeftExprM f g e
 
-mapExprStatementStatementM :: Monad m => (Expr -> m Expr) -> (Statement -> m Statement) -> Statement -> m Statement
+mapExprStatementStatementM :: Monad m => (Expr -> m Expr) -> (Statement -> m [Statement]) -> Statement -> m [Statement]
 mapExprStatementStatementM f g = go
   where
-    go' = mapExprStatementExprM f g
+    go' e = mapExprStatementExprM f g e
+    go'' body = concat <$> mapM go body
     go = \case
       ExprStatement e -> g . ExprStatement =<< go' e
-      Block stmts -> g . Block =<< mapM go stmts
-      If e body1 body2 -> g =<< (If <$> go' e <*> mapM go body1 <*> traverse (mapM go) body2)
-      For t x init pred incr body -> g =<< (For t x <$> go' init <*> go' pred <*> mapExprStatementAssignExprM f g incr <*> mapM go body)
-      ForEach t x e body -> g =<< (ForEach t x <$> go' e <*> mapM go body)
-      While e body -> g =<< (While <$> go' e <*> mapM go body)
+      Block stmts -> g . Block =<< go'' stmts
+      If e body1 body2 -> g =<< (If <$> go' e <*> go'' body1 <*> traverse go'' body2)
+      For t x init pred incr body -> g =<< (For t x <$> go' init <*> go' pred <*> mapExprStatementAssignExprM f g incr <*> go'' body)
+      ForEach t x e body -> g =<< (ForEach t x <$> go' e <*> go'' body)
+      While e body -> g =<< (While <$> go' e <*> go'' body)
       Declare t x init -> do
         init <- case init of
           DeclareDefault -> return DeclareDefault
@@ -194,27 +196,61 @@
       Assert e -> g . Assert =<< go' e
       Return e -> g . Return =<< go' e
 
-mapExprStatementToplevelStatementM :: Monad m => (Expr -> m Expr) -> (Statement -> m Statement) -> ToplevelStatement -> m ToplevelStatement
+mapExprStatementToplevelStatementM :: Monad m => (Expr -> m Expr) -> (Statement -> m [Statement]) -> ToplevelStatement -> m ToplevelStatement
 mapExprStatementToplevelStatementM f g = \case
   VarDef t x e -> VarDef t x <$> mapExprStatementExprM f g e
-  FunDef ret h args body -> FunDef ret h args <$> mapM (mapExprStatementStatementM f g) body
+  FunDef ret h args body -> FunDef ret h args <$> (concat <$> mapM (mapExprStatementStatementM f g) body)
   StaticAssert e msg -> StaticAssert <$> mapExprStatementExprM f g e <*> pure msg
 
-mapExprStatementProgramM :: Monad m => (Expr -> m Expr) -> (Statement -> m Statement) -> Program -> m Program
+mapExprStatementProgramM :: Monad m => (Expr -> m Expr) -> (Statement -> m [Statement]) -> Program -> m Program
 mapExprStatementProgramM f g (Program decls) = Program <$> mapM (mapExprStatementToplevelStatementM f g) decls
 
-mapExprStatementProgram :: (Expr -> Expr) -> (Statement -> Statement) -> Program -> Program
+mapExprStatementProgram :: (Expr -> Expr) -> (Statement -> [Statement]) -> Program -> Program
 mapExprStatementProgram f g = runIdentity . mapExprStatementProgramM (return . f) (return . g)
 
+mapSubExprM :: Monad m => (Expr -> m Expr) -> Expr -> m Expr
+mapSubExprM f e = mapExprStatementExprM f (return . (: [])) e
+
+-- | `mapDirectExprStatementM` replaces exprs which are direct children of a given statement.
+mapDirectExprStatementM :: Monad m => (Expr -> m Expr) -> Statement -> m Statement
+mapDirectExprStatementM f = \case
+  ExprStatement e -> ExprStatement <$> f e
+  Block stmts -> return $ Block stmts
+  If e body1 body2 -> If <$> f e <*> pure body1 <*> pure body2
+  For t x init pred incr body -> For t x <$> f init <*> f pred <*> mapDirectExprAssignExprM f incr <*> pure body
+  ForEach t x e body -> ForEach t x <$> f e <*> pure body
+  While e body -> While <$> f e <*> pure body
+  Declare t x init ->
+    Declare t x <$> case init of
+      DeclareDefault -> return DeclareDefault
+      DeclareCopy e -> DeclareCopy <$> f e
+      DeclareInitialize es -> DeclareInitialize <$> mapM f es
+  DeclareDestructure xs e -> DeclareDestructure xs <$> f e
+  Assign e -> Assign <$> mapDirectExprAssignExprM f e
+  Assert e -> Assert <$> f e
+  Return e -> Return <$> f e
+
+mapDirectExprAssignExprM :: Monad m => (Expr -> m Expr) -> AssignExpr -> m AssignExpr
+mapDirectExprAssignExprM f = \case
+  AssignExpr op e1 e2 -> AssignExpr op <$> mapDirectExprLeftExprM f e1 <*> f e2
+  AssignIncr e -> AssignIncr <$> mapDirectExprLeftExprM f e
+  AssignDecr e -> AssignDecr <$> mapDirectExprLeftExprM f e
+
+mapDirectExprLeftExprM :: Monad m => (Expr -> m Expr) -> LeftExpr -> m LeftExpr
+mapDirectExprLeftExprM f = \case
+  LeftVar x -> pure $ LeftVar x
+  LeftAt e1 e2 -> LeftAt <$> mapDirectExprLeftExprM f e1 <*> f e2
+  LeftGet i e -> LeftGet i <$> mapDirectExprLeftExprM f e
+
 replaceExpr :: VarName -> Expr -> Expr -> Expr
-replaceExpr x e = runIdentity . mapExprStatementExprM go return
+replaceExpr x e = runIdentity . mapExprStatementExprM go (return . (: []))
   where
     go = \case
       Var y | y == x -> return e
       e' -> return e'
 
 replaceStatement :: VarName -> Expr -> Statement -> Statement
-replaceStatement x e = runIdentity . mapExprStatementStatementM go return
+replaceStatement x e = head . runIdentity . mapExprStatementStatementM go (return . (: []))
   where
     go = \case
       Var y | y == x -> return e
diff --git a/src/Jikka/Common/Error.hs b/src/Jikka/Common/Error.hs
--- a/src/Jikka/Common/Error.hs
+++ b/src/Jikka/Common/Error.hs
@@ -23,6 +23,7 @@
     wrapAt',
     maybeToError,
     eitherToError,
+    fromSuccess,
 
     -- * utilities to report multiple errors
     catchError',
@@ -149,6 +150,11 @@
 
 eitherToError :: MonadError a m => Either a b -> m b
 eitherToError = liftEither
+
+fromSuccess :: Either Error a -> a
+fromSuccess f = case f of
+  Left err -> error $ "Jikka.Common.Error.fromSuccess: unexpected failure: " ++ show err
+  Right y -> y
 
 -- | `catchError'` is the inverse of `liftError`.
 catchError' :: MonadError e m => m a -> m (Either e a)
diff --git a/src/Jikka/Common/Matrix.hs b/src/Jikka/Common/Matrix.hs
--- a/src/Jikka/Common/Matrix.hs
+++ b/src/Jikka/Common/Matrix.hs
@@ -58,8 +58,8 @@
   Nothing -> error "Jikka.Common.Matrix.makeMatrix': the input is not a matrix"
   Just a -> a
 
-matzero :: Num a => Int -> Matrix a
-matzero n = Matrix $ V.replicate n (V.replicate n 0)
+matzero :: Num a => Int -> Int -> Matrix a
+matzero h w = Matrix $ V.replicate h (V.replicate w 0)
 
 matone :: Num a => Int -> Matrix a
 matone n = Matrix $ V.generate n (\y -> V.generate n (\x -> if y == x then 1 else 0))
diff --git a/src/Jikka/Core/Convert.hs b/src/Jikka/Core/Convert.hs
--- a/src/Jikka/Core/Convert.hs
+++ b/src/Jikka/Core/Convert.hs
@@ -18,7 +18,7 @@
 import Jikka.Common.Alpha
 import Jikka.Common.Error
 import qualified Jikka.Core.Convert.Alpha as Alpha
-import qualified Jikka.Core.Convert.ArithmeticalExpr as ArithmeticalExpr
+import qualified Jikka.Core.Convert.ArithmeticExpr as ArithmeticExpr
 import qualified Jikka.Core.Convert.Beta as Beta
 import qualified Jikka.Core.Convert.BubbleLet as BubbleLet
 import qualified Jikka.Core.Convert.CloseAll as CloseAll
@@ -63,7 +63,7 @@
   prog <- CumulativeSum.run prog
   prog <- SegmentTree.run prog
   prog <- BubbleLet.run prog
-  prog <- ArithmeticalExpr.run prog
+  prog <- ArithmeticExpr.run prog
   prog <- ConvexHullTrick.run prog
   prog <- StrengthReduction.run prog
   Eta.run prog
diff --git a/src/Jikka/Core/Convert/ArithmeticExpr.hs b/src/Jikka/Core/Convert/ArithmeticExpr.hs
new file mode 100644
--- /dev/null
+++ b/src/Jikka/Core/Convert/ArithmeticExpr.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+-- |
+-- Module      : Jikka.Core.Convert.ArithmeticExpr
+-- Description : sorts arithmetical exprs. / 算術式を整理します。
+-- Copyright   : (c) Kimiyuki Onaka, 2021
+-- License     : Apache License 2.0
+-- Maintainer  : kimiyuki95@gmail.com
+-- Stability   : experimental
+-- Portability : portable
+module Jikka.Core.Convert.ArithmeticExpr
+  ( run,
+  )
+where
+
+import Jikka.Common.Error
+import Jikka.Core.Language.ArithmeticExpr
+import Jikka.Core.Language.Expr
+import Jikka.Core.Language.Lint
+import Jikka.Core.Language.TypeCheck
+import Jikka.Core.Language.Util
+
+runExpr :: MonadError Error m => [(VarName, Type)] -> Expr -> m Expr
+runExpr env e = do
+  t <- typecheckExpr env e
+  if t == IntTy
+    then return . formatArithmeticExpr $ parseArithmeticExpr e
+    else return e
+
+runProgram :: MonadError Error m => Program -> m Program
+runProgram = mapExprProgramM (mapSubExprM runExpr) -- Doesn't use RewriteRules because the rewriting may not terminate.
+
+-- | `run` sorts arithmetical exprs.
+--
+-- == Examples
+--
+-- Before:
+--
+-- > 1 + a * 1 + b - b
+--
+-- After:
+--
+-- > a + 1
+run :: MonadError Error m => Program -> m Program
+run prog = wrapError' "Jikka.Core.Convert.ArithmeticExpr" $ do
+  precondition $ do
+    ensureWellTyped prog
+  prog <- runProgram prog
+  postcondition $ do
+    ensureWellTyped prog
+  return prog
diff --git a/src/Jikka/Core/Convert/ArithmeticalExpr.hs b/src/Jikka/Core/Convert/ArithmeticalExpr.hs
deleted file mode 100644
--- a/src/Jikka/Core/Convert/ArithmeticalExpr.hs
+++ /dev/null
@@ -1,51 +0,0 @@
-{-# LANGUAGE FlexibleContexts #-}
-
--- |
--- Module      : Jikka.Core.Convert.ArithmeticalExpr
--- Description : sorts arithmetical exprs. / 算術式を整理します。
--- Copyright   : (c) Kimiyuki Onaka, 2021
--- License     : Apache License 2.0
--- Maintainer  : kimiyuki95@gmail.com
--- Stability   : experimental
--- Portability : portable
-module Jikka.Core.Convert.ArithmeticalExpr
-  ( run,
-  )
-where
-
-import Jikka.Common.Error
-import Jikka.Core.Language.ArithmeticalExpr
-import Jikka.Core.Language.Expr
-import Jikka.Core.Language.Lint
-import Jikka.Core.Language.TypeCheck
-import Jikka.Core.Language.Util
-
-runExpr :: MonadError Error m => [(VarName, Type)] -> Expr -> m Expr
-runExpr env e = do
-  t <- typecheckExpr env e
-  if t == IntTy
-    then return . formatArithmeticalExpr $ parseArithmeticalExpr e
-    else return e
-
-runProgram :: MonadError Error m => Program -> m Program
-runProgram = mapExprProgramM runExpr -- Doesn't use RewriteRules because the rewriting may not terminate.
-
--- | `run` sorts arithmetical exprs.
---
--- == Examples
---
--- Before:
---
--- > 1 + a * 1 + b - b
---
--- After:
---
--- > a + 1
-run :: MonadError Error m => Program -> m Program
-run prog = wrapError' "Jikka.Core.Convert.ArithmeticalExpr" $ do
-  precondition $ do
-    ensureWellTyped prog
-  prog <- runProgram prog
-  postcondition $ do
-    ensureWellTyped prog
-  return prog
diff --git a/src/Jikka/Core/Convert/CloseAll.hs b/src/Jikka/Core/Convert/CloseAll.hs
--- a/src/Jikka/Core/Convert/CloseAll.hs
+++ b/src/Jikka/Core/Convert/CloseAll.hs
@@ -34,13 +34,13 @@
   mconcat
     [ -- list build functions
       [r| "all/nil" all nil = true |],
-      [r| "all/cons" forall x xs. all (cons x xs) = x and all xs |],
+      [r| "all/cons" forall x xs. all (cons x xs) = x && all xs |],
       -- list map functions
       [r| "all/reversed" forall xs. all (reversed xs) = all xs |],
       [r| "all/sorted" forall xs. all (sorted xs) = all xs |],
-      [r| "all/filter" forall f xs. all (filter f xs) = all (map (fun x -> f x implies x) xs) |],
+      [r| "all/filter" forall f xs. all (filter f xs) = all (map (fun x -> implies (f x) x) xs) |],
       [r| "all/map/not" forall e xs. all (map (fun x -> not e) xs) = not (any (map (fun x -> e) xs)) |],
-      [r| "all/map/and" forall e1 e2 xs. all (map (fun x -> e1 and e2) xs) = all (map (fun x -> e1) xs) and all (map (fun x -> e2) xs) |]
+      [r| "all/map/and" forall e1 e2 xs. all (map (fun x -> e1 && e2) xs) = all (map (fun x -> e1) xs) && all (map (fun x -> e2) xs) |]
     ]
 
 reduceAny :: MonadAlpha m => RewriteRule m
@@ -48,14 +48,14 @@
   mconcat
     [ -- list build functions
       [r| "any/nil" any nil = false |],
-      [r| "any/cons" forall x xs. any (cons x xs) = x or any xs |],
+      [r| "any/cons" forall x xs. any (cons x xs) = x || any xs |],
       -- list map functions
       [r| "any/reversed" forall xs. any (reversed xs) = any xs |],
       [r| "any/sorted" forall xs. any (sorted xs) = any xs |],
-      [r| "any/filter" forall f xs. any (filter f xs) = any (map (fun x -> f x and x) xs) |],
+      [r| "any/filter" forall f xs. any (filter f xs) = any (map (fun x -> f x && x) xs) |],
       [r| "any/map/not" forall e xs. any (map (fun x -> not e) xs) = not (all (map (fun x -> e) xs)) |],
-      [r| "any/map/or" forall e1 e2 xs. any (map (fun x -> e1 or e2) xs) = any (map (fun x -> e1) xs) or any (map (fun x -> e2) xs) |],
-      [r| "any/map/implies" forall e1 e2 xs. any (map (fun x -> e1 implies e2) xs) = any (map (fun x -> not e1) xs) or any (map (fun x -> e2) xs) |]
+      [r| "any/map/or" forall e1 e2 xs. any (map (fun x -> e1 || e2) xs) = any (map (fun x -> e1) xs) || any (map (fun x -> e2) xs) |],
+      [r| "any/map/implies" forall e1 e2 xs. any (map (fun x -> implies e1 e2) xs) = any (map (fun x -> not e1) xs) || any (map (fun x -> e2) xs) |]
     ]
 
 rule :: MonadAlpha m => RewriteRule m
diff --git a/src/Jikka/Core/Convert/ConstantFolding.hs b/src/Jikka/Core/Convert/ConstantFolding.hs
--- a/src/Jikka/Core/Convert/ConstantFolding.hs
+++ b/src/Jikka/Core/Convert/ConstantFolding.hs
@@ -20,7 +20,7 @@
 
     -- * internal rules
     rule,
-    reduceConstArithmeticalExpr,
+    reduceConstArithmeticExpr,
     reduceConstMaxExpr,
     reduceConstBooleanExpr,
     reduceConstBitExpr,
@@ -57,10 +57,10 @@
 -- * `Abs` \(: \int \to \int\)
 -- * `Gcd` \(: \int \to \int \to \int\)
 -- * `Lcm` \(: \int \to \int \to \int\)
-reduceConstArithmeticalExpr :: Monad m => RewriteRule m
-reduceConstArithmeticalExpr =
+reduceConstArithmeticExpr :: Monad m => RewriteRule m
+reduceConstArithmeticExpr =
   let return' = Just . LitInt'
-   in simpleRewriteRule "reduceConstArithmeticalExpr" $ \case
+   in simpleRewriteRule "reduceConstArithmeticExpr" $ \case
         Negate' (LitInt' a) -> return' $ - a
         Plus' a (LitInt' 0) -> Just a
         Plus' (LitInt' 0) b -> Just b
@@ -209,7 +209,7 @@
 rule :: MonadError Error m => RewriteRule m
 rule =
   mconcat
-    [ reduceConstArithmeticalExpr,
+    [ reduceConstArithmeticExpr,
       reduceConstMaxExpr,
       reduceConstBooleanExpr,
       reduceConstBitExpr,
diff --git a/src/Jikka/Core/Convert/ConvexHullTrick.hs b/src/Jikka/Core/Convert/ConvexHullTrick.hs
--- a/src/Jikka/Core/Convert/ConvexHullTrick.hs
+++ b/src/Jikka/Core/Convert/ConvexHullTrick.hs
@@ -28,7 +28,7 @@
 import Control.Monad.Trans.Maybe
 import Jikka.Common.Alpha
 import Jikka.Common.Error
-import Jikka.Core.Language.ArithmeticalExpr
+import Jikka.Core.Language.ArithmeticExpr
 import Jikka.Core.Language.Beta
 import Jikka.Core.Language.BuiltinPatterns
 import Jikka.Core.Language.Expr
@@ -38,22 +38,22 @@
 import Jikka.Core.Language.Util
 
 -- | This is something commutative because only one kind of @c@ is allowed.
-plusPair :: (ArithmeticalExpr, ArithmeticalExpr) -> (ArithmeticalExpr, ArithmeticalExpr) -> Maybe (ArithmeticalExpr, ArithmeticalExpr)
-plusPair (a1, c1) (a2, _) | isZeroArithmeticalExpr a2 = Just (a1, c1)
-plusPair (a1, c1) (_, c2) | isZeroArithmeticalExpr c2 = Just (a1, c1)
-plusPair (a1, _) (a2, c2) | isZeroArithmeticalExpr a1 = Just (a2, c2)
-plusPair (_, c1) (a2, c2) | isZeroArithmeticalExpr c1 = Just (a2, c2)
+plusPair :: (ArithmeticExpr, ArithmeticExpr) -> (ArithmeticExpr, ArithmeticExpr) -> Maybe (ArithmeticExpr, ArithmeticExpr)
+plusPair (a1, c1) (a2, _) | isZeroArithmeticExpr a2 = Just (a1, c1)
+plusPair (a1, c1) (_, c2) | isZeroArithmeticExpr c2 = Just (a1, c1)
+plusPair (a1, _) (a2, c2) | isZeroArithmeticExpr a1 = Just (a2, c2)
+plusPair (_, c1) (a2, c2) | isZeroArithmeticExpr c1 = Just (a2, c2)
 plusPair (a1, c1) (a2, c2) =
-  let (k1, c1') = splitConstantFactorArithmeticalExpr c1
-      (k2, c2') = splitConstantFactorArithmeticalExpr c2
-      a1' = multArithmeticalExpr (integerArithmeticalExpr k1) a1
-      a2' = multArithmeticalExpr (integerArithmeticalExpr k2) a2
+  let (k1, c1') = splitConstantFactorArithmeticExpr c1
+      (k2, c2') = splitConstantFactorArithmeticExpr c2
+      a1' = multArithmeticExpr (integerArithmeticExpr k1) a1
+      a2' = multArithmeticExpr (integerArithmeticExpr k2) a2
    in if c1' == c2'
-        then Just (plusArithmeticalExpr a1' a2', c1')
+        then Just (plusArithmeticExpr a1' a2', c1')
         else Nothing
 
-sumPairs :: [(ArithmeticalExpr, ArithmeticalExpr)] -> Maybe (ArithmeticalExpr, ArithmeticalExpr)
-sumPairs = foldr (\e1 e2 -> plusPair e1 =<< e2) (Just (integerArithmeticalExpr 1, integerArithmeticalExpr 0))
+sumPairs :: [(ArithmeticExpr, ArithmeticExpr)] -> Maybe (ArithmeticExpr, ArithmeticExpr)
+sumPairs = foldr (\e1 e2 -> plusPair e1 =<< e2) (Just (integerArithmeticExpr 1, integerArithmeticExpr 0))
 
 -- | `parseLinearFunctionBody'` parses the body of a linear function which can be decomposed to convex hull trick.
 -- @parseLinearFunctionBody' f i j e@ finds a 4-tuple @a, b, c, d@ where @e = a(f[j], j) c(f[< i], i) + b(f[j], j) + d(f[< i], i)@.
@@ -63,56 +63,56 @@
 parseLinearFunctionBody' f i j e = result <$> go e
   where
     result (a, c, b, d) =
-      let (k, a') = splitConstantFactorArithmeticalExpr a
-          c' = multArithmeticalExpr (integerArithmeticalExpr k) c
-       in (formatArithmeticalExpr a', formatArithmeticalExpr c', formatArithmeticalExpr b, formatArithmeticalExpr d)
+      let (k, a') = splitConstantFactorArithmeticExpr a
+          c' = multArithmeticExpr (integerArithmeticExpr k) c
+       in (formatArithmeticExpr a', formatArithmeticExpr c', formatArithmeticExpr b, formatArithmeticExpr d)
     go = \case
       Negate' e -> do
         (a, c, b, d) <- go e
-        return (a, negateArithmeticalExpr c, negateArithmeticalExpr b, negateArithmeticalExpr d)
+        return (a, negateArithmeticExpr c, negateArithmeticExpr b, negateArithmeticExpr d)
       Plus' e1 e2 -> do
         (a1, c1, b1, d1) <- go e1
         (a2, c2, b2, d2) <- go e2
         (a, c) <- plusPair (a1, c1) (a2, c2)
-        return (a, c, plusArithmeticalExpr b1 b2, plusArithmeticalExpr d1 d2)
+        return (a, c, plusArithmeticExpr b1 b2, plusArithmeticExpr d1 d2)
       Minus' e1 e2 -> do
         (a1, c1, b1, d1) <- go e1
         (a2, c2, b2, d2) <- go e2
-        (a, c) <- plusPair (a1, c1) (negateArithmeticalExpr a2, c2)
-        return (a, c, minusArithmeticalExpr b1 b2, minusArithmeticalExpr d1 d2)
+        (a, c) <- plusPair (a1, c1) (negateArithmeticExpr a2, c2)
+        return (a, c, minusArithmeticExpr b1 b2, minusArithmeticExpr d1 d2)
       Mult' e1 e2 -> do
         (a1, c1, b1, d1) <- go e1
         (a2, c2, b2, d2) <- go e2
         (a, c) <-
           sumPairs
-            [ (multArithmeticalExpr a1 a2, multArithmeticalExpr c1 c2),
-              (multArithmeticalExpr b2 a1, c1),
-              (multArithmeticalExpr b1 a2, c2),
-              (a1, multArithmeticalExpr c1 d2),
-              (a2, multArithmeticalExpr c2 d1),
+            [ (multArithmeticExpr a1 a2, multArithmeticExpr c1 c2),
+              (multArithmeticExpr b2 a1, c1),
+              (multArithmeticExpr b1 a2, c2),
+              (a1, multArithmeticExpr c1 d2),
+              (a2, multArithmeticExpr c2 d1),
               (b2, d1),
               (b1, d2)
             ]
-        return (a, c, multArithmeticalExpr b1 b2, multArithmeticalExpr d1 d2)
+        return (a, c, multArithmeticExpr b1 b2, multArithmeticExpr d1 d2)
       e
         | f `isUnusedVar` e && j `isUnusedVar` e ->
           -- NOTE: Put constants to @d@ and simplify @a, b@
-          return (integerArithmeticalExpr 1, integerArithmeticalExpr 0, integerArithmeticalExpr 0, parseArithmeticalExpr e)
+          return (integerArithmeticExpr 1, integerArithmeticExpr 0, integerArithmeticExpr 0, parseArithmeticExpr e)
       e
         | f `isUnusedVar` e && i `isUnusedVar` e ->
-          return (integerArithmeticalExpr 1, integerArithmeticalExpr 0, parseArithmeticalExpr e, integerArithmeticalExpr 0)
-      e@(At' _ (Var f') index) | f' == f -> case unNPlusKPattern (parseArithmeticalExpr index) of
+          return (integerArithmeticExpr 1, integerArithmeticExpr 0, parseArithmeticExpr e, integerArithmeticExpr 0)
+      e@(At' _ (Var f') index) | f' == f -> case unNPlusKPattern (parseArithmeticExpr index) of
         Just (i', k) | i' == i && k < 0 -> do
-          return (integerArithmeticalExpr 1, integerArithmeticalExpr 0, integerArithmeticalExpr 0, parseArithmeticalExpr e)
+          return (integerArithmeticExpr 1, integerArithmeticExpr 0, integerArithmeticExpr 0, parseArithmeticExpr e)
         Just (j', 0) | j' == j -> do
-          return (integerArithmeticalExpr 1, integerArithmeticalExpr 0, parseArithmeticalExpr e, integerArithmeticalExpr 0)
+          return (integerArithmeticExpr 1, integerArithmeticExpr 0, parseArithmeticExpr e, integerArithmeticExpr 0)
         _ -> Nothing
       _ -> Nothing
 
 parseLinearFunctionBody :: MonadAlpha m => VarName -> VarName -> Integer -> Expr -> m (Maybe (Expr, Expr, Expr, Expr, Expr, Maybe Expr))
 parseLinearFunctionBody f i k = runMaybeT . go
   where
-    goMin e j step size = case unNPlusKPattern (parseArithmeticalExpr size) of
+    goMin e j step size = case unNPlusKPattern (parseArithmeticExpr size) of
       Just (i', k') | i' == i && k' == k -> do
         (a, b, c, d) <- hoistMaybe $ parseLinearFunctionBody' f i j step
         -- raname @j@ to @i@
@@ -175,7 +175,8 @@
       (Just e, 0) -> do
         e0 <- lift $ substitute i (LitInt' 0) e
         d0 <- lift $ substitute i (LitInt' 0) d
-        let base' = Let f (ListTy IntTy) base $ Snoc' IntTy base (Plus' (Mult' sign e0) d0)
+        let e0' = Let f (ListTy IntTy) base e0
+        let base' = Snoc' IntTy base (Plus' (Mult' sign e0') d0)
         c <- lift $ substitute i (Plus' (Var i) (LitInt' 1)) c
         d <- lift $ substitute i (Plus' (Var i) (LitInt' 1)) d
         e <- lift $ substitute i (Plus' (Var i) (LitInt' 1)) e
diff --git a/src/Jikka/Core/Convert/CumulativeSum.hs b/src/Jikka/Core/Convert/CumulativeSum.hs
--- a/src/Jikka/Core/Convert/CumulativeSum.hs
+++ b/src/Jikka/Core/Convert/CumulativeSum.hs
@@ -21,7 +21,7 @@
 import Jikka.Common.Alpha
 import Jikka.Common.Error
 import qualified Jikka.Core.Convert.Alpha as Alpha
-import Jikka.Core.Language.ArithmeticalExpr
+import Jikka.Core.Language.ArithmeticExpr
 import Jikka.Core.Language.BuiltinPatterns
 import Jikka.Core.Language.Expr
 import Jikka.Core.Language.FreeVars
@@ -41,13 +41,13 @@
 rule :: MonadAlpha m => RewriteRule m
 rule = makeRewriteRule "Jikka.Core.Convert.CumulativeSum" $ \_ -> \case
   Sum' (Map' _ _ (Lam x _ (At' _ a index)) (Range1' n)) | x `isUnusedVar` a -> do
-    case makeAffineFunctionFromArithmeticalExpr x (parseArithmeticalExpr index) of
-      Just (coeff, shift) | isOneArithmeticalExpr coeff -> do
+    case makeAffineFunctionFromArithmeticExpr x (parseArithmeticExpr index) of
+      Just (coeff, shift) | isOneArithmeticExpr coeff -> do
         b <- genVarName'
         let e =
-              if isZeroArithmeticalExpr shift
+              if isZeroArithmeticExpr shift
                 then At' IntTy (Var b) n
-                else Minus' (At' IntTy (Var b) (Plus' n (formatArithmeticalExpr shift))) (At' IntTy (Var b) (formatArithmeticalExpr shift))
+                else Minus' (At' IntTy (Var b) (Plus' n (formatArithmeticExpr shift))) (At' IntTy (Var b) (formatArithmeticExpr shift))
         return . Just $
           Let b (ListTy IntTy) (Scanl' IntTy IntTy (Builtin Plus) Lit0 a) e
       _ -> return Nothing
diff --git a/src/Jikka/Core/Convert/KubaruToMorau.hs b/src/Jikka/Core/Convert/KubaruToMorau.hs
--- a/src/Jikka/Core/Convert/KubaruToMorau.hs
+++ b/src/Jikka/Core/Convert/KubaruToMorau.hs
@@ -21,7 +21,7 @@
 import Control.Monad.Trans.Maybe
 import Jikka.Common.Alpha
 import Jikka.Common.Error
-import Jikka.Core.Language.ArithmeticalExpr
+import Jikka.Core.Language.ArithmeticExpr
 import Jikka.Core.Language.Beta
 import Jikka.Core.Language.BuiltinPatterns
 import Jikka.Core.Language.Expr
@@ -40,8 +40,8 @@
           | otherwise -> return $ Var x
         Lit lit -> return $ Lit lit
         At' _ (Var c') index | c' == c -> case () of
-          () | parseArithmeticalExpr index == parseArithmeticalExpr (Var i) -> return $ Var x
-          () | parseArithmeticalExpr index == parseArithmeticalExpr (Var k) -> return $ Var y
+          () | parseArithmeticExpr index == parseArithmeticExpr (Var i) -> return $ Var x
+          () | parseArithmeticExpr index == parseArithmeticExpr (Var k) -> return $ Var y
           () | otherwise -> hoistMaybe Nothing
         App e1 e2 -> App <$> go e1 <*> go e2
         Let x t e1 e2
@@ -60,9 +60,9 @@
   Foldl' IntTy (ListTy t2) (Lam2 b _ i _ (Foldl' IntTy (ListTy t2') (Lam2 c _ j _ (SetAt' _ (Var c') index step)) (Var b') (Range1' m))) a (Range1' n)
     | t2' == t2 && b' == b && c == c' && b `isUnusedVar` m && b `isUnusedVar` index && b `isUnusedVar` step && c `isUnusedVar` index -> runMaybeT $ do
       -- m(i) = n - i - 1
-      guard $ parseArithmeticalExpr m == parseArithmeticalExpr (Minus' (Minus' n (Var i)) (LitInt' 1))
+      guard $ parseArithmeticExpr m == parseArithmeticExpr (Minus' (Minus' n (Var i)) (LitInt' 1))
       -- index(i, j) = i + j + 1
-      guard $ parseArithmeticalExpr index == parseArithmeticalExpr (Plus' (Var i) (Plus' (Var j) (LitInt' 1)))
+      guard $ parseArithmeticExpr index == parseArithmeticExpr (Plus' (Var i) (Plus' (Var j) (LitInt' 1)))
       x <- lift genVarName'
       y <- lift genVarName'
       k <- lift genVarName'
diff --git a/src/Jikka/Core/Convert/MakeScanl.hs b/src/Jikka/Core/Convert/MakeScanl.hs
--- a/src/Jikka/Core/Convert/MakeScanl.hs
+++ b/src/Jikka/Core/Convert/MakeScanl.hs
@@ -35,7 +35,7 @@
 import qualified Data.Map as M
 import Jikka.Common.Alpha
 import Jikka.Common.Error
-import Jikka.Core.Language.ArithmeticalExpr
+import Jikka.Core.Language.ArithmeticExpr
 import Jikka.Core.Language.Beta
 import Jikka.Core.Language.BuiltinPatterns
 import Jikka.Core.Language.Expr
@@ -66,7 +66,7 @@
           else Nothing
   let go :: Expr -> Maybe Expr
       go = \case
-        At' _ (Var a') i' | a' == a -> case unNPlusKPattern (parseArithmeticalExpr i') of
+        At' _ (Var a') i' | a' == a -> case unNPlusKPattern (parseArithmeticExpr i') of
           Just (i', k) | i' == i -> proj k
           _ -> Nothing
         Var x -> if x == a then Nothing else Just (Var x)
@@ -90,7 +90,7 @@
           else Nothing
   let go :: Expr -> Maybe Expr
       go = \case
-        At' _ (Var a') i' | a' == a -> case unNPlusKPattern (parseArithmeticalExpr i') of
+        At' _ (Var a') i' | a' == a -> case unNPlusKPattern (parseArithmeticExpr i') of
           Just (i', k) | i' == i -> proj k
           _ -> Nothing
         Var x -> if x == a then Nothing else Just (Var x)
@@ -112,7 +112,7 @@
   -- foldl (fun a i -> setat a index(i) step(a, i)) base indices
   Foldl' _ (ListTy t2) (Lam2 a _ i _ (SetAt' _ (Var a') index step)) base indices | a' == a && a `isUnusedVar` index -> runMaybeT $ do
     -- index(i) = i + k
-    k <- hoistMaybe $ case unNPlusKPattern (parseArithmeticalExpr index) of
+    k <- hoistMaybe $ case unNPlusKPattern (parseArithmeticExpr index) of
       Just (i', k) | i' == i -> Just k
       _ -> Nothing
     -- indices = range n
@@ -184,12 +184,12 @@
     -- (i, k) in env menas a[i + k] is accessible but a[i + k + 1] is not.
     go :: M.Map VarName Integer -> Expr -> Bool
     go env = \case
-      At' _ (Var a') i | a' == a -> case unNPlusKPattern (parseArithmeticalExpr i) of
+      At' _ (Var a') i | a' == a -> case unNPlusKPattern (parseArithmeticExpr i) of
         Just (i, k) -> case M.lookup i env of
           Just limit -> k <= limit
           Nothing -> False
         _ -> False
-      Map' _ _ (Lam j _ body) (Range1' n) | j /= a -> case unNPlusKPattern (parseArithmeticalExpr n) of
+      Map' _ _ (Lam j _ body) (Range1' n) | j /= a -> case unNPlusKPattern (parseArithmeticExpr n) of
         Just (i, k) -> case M.lookup i env of
           Just limit -> go (M.insert j (limit - k + 1) env) body
           Nothing -> go env body && go env n
@@ -206,7 +206,7 @@
   -- foldl (fun a i -> setat a index(i) step(a, i)) base indices
   Foldl' _ (ListTy t2) (Lam2 a _ i _ (SetAt' _ (Var a') index step)) base indices | a' == a && a `isUnusedVar` index -> runMaybeT $ do
     -- index(i) = i + k
-    k <- hoistMaybe $ case unNPlusKPattern (parseArithmeticalExpr index) of
+    k <- hoistMaybe $ case unNPlusKPattern (parseArithmeticExpr index) of
       Just (i', k) | i' == i -> Just k
       _ -> Nothing
     -- indices = range n
diff --git a/src/Jikka/Core/Convert/MatrixExponentiation.hs b/src/Jikka/Core/Convert/MatrixExponentiation.hs
--- a/src/Jikka/Core/Convert/MatrixExponentiation.hs
+++ b/src/Jikka/Core/Convert/MatrixExponentiation.hs
@@ -21,7 +21,7 @@
 import Jikka.Common.Alpha
 import Jikka.Common.Error
 import Jikka.Common.Matrix
-import Jikka.Core.Language.ArithmeticalExpr
+import Jikka.Core.Language.ArithmeticExpr
 import Jikka.Core.Language.BuiltinPatterns
 import Jikka.Core.Language.Expr
 import Jikka.Core.Language.FreeVars
@@ -31,29 +31,29 @@
 
 toLinearExpression :: VarName -> Expr -> Maybe (Maybe Expr, Maybe Expr)
 toLinearExpression x e = do
-  (a, b) <- makeVectorFromArithmeticalExpr (V.singleton x) (parseArithmeticalExpr e)
+  (a, b) <- makeVectorFromArithmeticExpr (V.singleton x) (parseArithmeticExpr e)
   case V.toList a of
     [a] ->
-      let a' = if isOneArithmeticalExpr a then Nothing else Just (formatArithmeticalExpr a)
-          b' = if isZeroArithmeticalExpr b then Nothing else Just (formatArithmeticalExpr b)
+      let a' = if isOneArithmeticExpr a then Nothing else Just (formatArithmeticExpr a)
+          b' = if isZeroArithmeticExpr b then Nothing else Just (formatArithmeticExpr b)
        in Just (a', b')
     _ -> error $ "Jikka.Core.Convert.MatrixExponentiation.toLinearExpression: size mismtach: " ++ show (V.length a)
 
-fromMatrix :: Matrix ArithmeticalExpr -> Expr
+fromMatrix :: Matrix ArithmeticExpr -> Expr
 fromMatrix f =
   let (h, w) = matsize f
-      go row = uncurryApp (Tuple' (replicate w IntTy)) (map formatArithmeticalExpr (V.toList row))
+      go row = uncurryApp (Tuple' (replicate w IntTy)) (map formatArithmeticExpr (V.toList row))
    in uncurryApp (Tuple' (replicate h (TupleTy (replicate w IntTy)))) (map go (V.toList (unMatrix f)))
 
-fromAffineMatrix :: Matrix ArithmeticalExpr -> V.Vector ArithmeticalExpr -> Expr
+fromAffineMatrix :: Matrix ArithmeticExpr -> V.Vector ArithmeticExpr -> Expr
 fromAffineMatrix a b | fst (matsize a) /= V.length b = error $ "Jikka.Core.Convert.MatrixExponentiation.fromAffineMatrix: size mismtach: " ++ show (matsize a) ++ " and " ++ show (V.length b)
 fromAffineMatrix a b =
   let (h, w) = matsize a
-      go row c = uncurryApp (Tuple' (replicate (w + 1) IntTy)) (map formatArithmeticalExpr (V.toList row ++ [c]))
+      go row c = uncurryApp (Tuple' (replicate (w + 1) IntTy)) (map formatArithmeticExpr (V.toList row ++ [c]))
       bottom = uncurryApp (Tuple' (replicate (w + 1) IntTy)) (replicate w (LitInt' 0) ++ [LitInt' 1])
    in uncurryApp (Tuple' (replicate (h + 1) (TupleTy (replicate (w + 1) IntTy)))) (V.toList (V.zipWith go (unMatrix a) b) ++ [bottom])
 
-toMatrix :: MonadAlpha m => [(VarName, Type)] -> VarName -> Integer -> Expr -> m (Maybe (Matrix ArithmeticalExpr, Maybe (V.Vector ArithmeticalExpr)))
+toMatrix :: MonadAlpha m => [(VarName, Type)] -> VarName -> Integer -> Expr -> m (Maybe (Matrix ArithmeticExpr, Maybe (V.Vector ArithmeticExpr)))
 toMatrix env x n step =
   case curryApp step of
     (Tuple' _, es) -> runMaybeT $ do
@@ -62,11 +62,11 @@
             Proj' _ i (Var x') | x' == x -> Var (xs V.! fromInteger i)
             _ -> e
       rows <- MaybeT . return . forM es $ \e -> do
-        let e' = mapExpr unpackTuple env e
+        let e' = mapSubExpr unpackTuple env e
         guard $ x `isUnusedVar` e'
-        makeVectorFromArithmeticalExpr xs (parseArithmeticalExpr e')
+        makeVectorFromArithmeticExpr xs (parseArithmeticExpr e')
       a <- MaybeT . return $ makeMatrix (V.fromList (map fst rows))
-      let b = if all (isZeroArithmeticalExpr . snd) rows then Nothing else Just (V.fromList (map snd rows))
+      let b = if all (isZeroArithmeticExpr . snd) rows then Nothing else Just (V.fromList (map snd rows))
       return (a, b)
     _ -> return Nothing
 
diff --git a/src/Jikka/Core/Convert/RemoveUnusedVars.hs b/src/Jikka/Core/Convert/RemoveUnusedVars.hs
--- a/src/Jikka/Core/Convert/RemoveUnusedVars.hs
+++ b/src/Jikka/Core/Convert/RemoveUnusedVars.hs
@@ -24,7 +24,7 @@
 import Jikka.Core.Language.Util
 
 runExpr :: [(VarName, Type)] -> Expr -> Expr
-runExpr _ = mapExpr go []
+runExpr _ = mapSubExpr go []
   where
     go _ = \case
       Let x _ _ e2 | x `isUnusedVar` e2 -> e2
@@ -40,7 +40,7 @@
   e -> e
 
 run' :: Program -> Program
-run' = mapToplevelExprProgram runToplevelExpr . mapExprProgram runExpr
+run' = mapToplevelExprProgram runToplevelExpr . mapExprProgram (mapSubExpr runExpr)
 
 -- | `run` removes unused variables in given programs.
 --
diff --git a/src/Jikka/Core/Convert/ShortCutFusion.hs b/src/Jikka/Core/Convert/ShortCutFusion.hs
--- a/src/Jikka/Core/Convert/ShortCutFusion.hs
+++ b/src/Jikka/Core/Convert/ShortCutFusion.hs
@@ -85,7 +85,7 @@
   mconcat
     [ [r| "map/map" forall f g xs. map g (map f xs) = map (fun x -> g (f x)) xs |],
       [r| "map/reversed" forall f xs. map f (reversed xs) = reversed (map f xs) |],
-      [r| "filter/filter" forall f g xs. filter g (filter f xs) = filter (fun x -> f x and g x) xs |],
+      [r| "filter/filter" forall f g xs. filter g (filter f xs) = filter (fun x -> f x && g x) xs |],
       [r| "filter/sorted" forall f xs. filter f (sorted xs) = sorted (filter f xs) |],
       [r| "filter/reversed" forall f xs. filter f (reversed xs) = reversed (filter f xs) |],
       [r| "reversed/reversed" forall xs. reversed (reversed xs) = xs |],
@@ -136,8 +136,8 @@
       [r| "at/range" forall n i. (range n)[i] = i |],
       -- reduce `Elem`
       [r| "elem/nil" forall y. elem y nil = false |],
-      [r| "elem/cons" forall y x xs. elem y (cons x xs) = y == x or elem y xs |],
-      [r| "elem/range" forall i n. elem i (range n) = 0 <= i and i < n |],
+      [r| "elem/cons" forall y x xs. elem y (cons x xs) = y == x || elem y xs |],
+      [r| "elem/range" forall i n. elem i (range n) = 0 <= i && i < n |],
       -- others
       [r| "len/build" forall f base n. len (build f base n) = len base + n |]
     ]
diff --git a/src/Jikka/Core/Convert/TypeInfer.hs b/src/Jikka/Core/Convert/TypeInfer.hs
--- a/src/Jikka/Core/Convert/TypeInfer.hs
+++ b/src/Jikka/Core/Convert/TypeInfer.hs
@@ -21,6 +21,7 @@
     mergeAssertions,
     Subst (..),
     subst,
+    substDefault,
     solveEquations,
     substProgram,
   )
@@ -34,6 +35,7 @@
 import Jikka.Common.Alpha
 import Jikka.Common.Error
 import Jikka.Core.Format (formatType)
+import Jikka.Core.Language.BuiltinPatterns
 import Jikka.Core.Language.Expr
 import Jikka.Core.Language.FreeVars
 import Jikka.Core.Language.Lint
@@ -59,7 +61,9 @@
     t <- genType
     formularizeVarName x t
     return t
-  Lit lit -> literalToType lit
+  Lit lit -> case lit of
+    LitBuiltin (Proj _) [] -> genType -- Proj may have a empty list.
+    _ -> literalToType lit
   App f e -> do
     ret <- genType
     t <- formularizeExpr e
@@ -166,26 +170,36 @@
 solveEquations eqns = wrapError' "failed to solve type equations" $ do
   execStateT (mapM_ (uncurry unifyType) eqns) (Subst M.empty)
 
--- | `substUnit` replaces all undetermined type variables with the unit type.
-substUnit :: Type -> Type
-substUnit = \case
+-- | `substDefault` replaces all undetermined type variables with the given default type.
+substDefault :: Type -> Type -> Type
+substDefault t0 = \case
   VarTy _ -> TupleTy []
   IntTy -> IntTy
   BoolTy -> BoolTy
-  ListTy t -> ListTy (substUnit t)
-  TupleTy ts -> TupleTy (map substUnit ts)
-  FunTy t ret -> FunTy (substUnit t) (substUnit ret)
+  ListTy t -> ListTy (substDefault t0 t)
+  TupleTy ts -> TupleTy (map (substDefault t0) ts)
+  FunTy t ret -> FunTy (substDefault t0 t) (substDefault t0 ret)
   DataStructureTy ds -> DataStructureTy ds
 
-subst' :: Subst -> Type -> Type
-subst' sigma = substUnit . subst sigma
+subst' :: Maybe Type -> Subst -> Type -> Type
+subst' t0 sigma = maybe id substDefault t0 . subst sigma
 
-substProgram :: Subst -> Program -> Program
-substProgram sigma = mapTypeProgram (subst' sigma)
+fixProj :: MonadError Error m => [(VarName, Type)] -> Expr -> m Expr
+fixProj env = \case
+  Proj' [] i e -> do
+    -- fix Proj with a empty list
+    t <- typecheckExpr env e
+    case t of
+      TupleTy ts -> return $ Proj' ts i e
+      _ -> throwInternalError $ "type of argument of proj must be a tuple: " ++ formatType t
+  e -> return e
 
-substExpr :: Subst -> Expr -> Expr
-substExpr sigma = mapTypeExpr (subst' sigma)
+substProgram :: MonadError Error m => Maybe Type -> Subst -> Program -> m Program
+substProgram t0 sigma = mapExprProgramM (mapSubExprM fixProj) . mapTypeProgram (subst' t0 sigma)
 
+substExpr :: MonadError Error m => Maybe Type -> Subst -> [(VarName, Type)] -> Expr -> m Expr
+substExpr t0 sigma env = mapSubExprM fixProj env . mapTypeExpr (subst' t0 sigma)
+
 -- | `run` does type inference.
 --
 -- * This assumes that program has no name conflicts.
@@ -207,7 +221,8 @@
   let (eqns', assertions) = sortEquations eqns
   let eqns'' = mergeAssertions assertions
   sigma <- solveEquations (eqns' ++ eqns'')
-  prog <- return $ substProgram sigma prog
+  let t0 = Just UnitTy
+  prog <- substProgram t0 sigma prog
   postcondition $ do
     typecheckProgram prog
   return prog
@@ -218,8 +233,9 @@
   let (eqns', assertions) = sortEquations eqns
   let eqns'' = mergeAssertions assertions
   sigma <- solveEquations (eqns' ++ eqns'')
-  env <- return $ map (second (subst' sigma)) env
-  e <- return $ substExpr sigma e
+  let t0 = Nothing -- don't use substDefault
+  env <- return $ map (second (subst' t0 sigma)) env
+  e <- substExpr t0 sigma env e
   postcondition $ do
     typecheckExpr env e
   return e
@@ -232,7 +248,7 @@
   let (eqns', assertions) = sortEquations eqns
   let eqns'' = mergeAssertions assertions
   sigma <- solveEquations (eqns' ++ eqns'')
-  args <- return $ map (second (subst sigma)) args -- don't use substUnit
-  e1 <- return $ mapTypeExpr (subst sigma) e1 -- don't use substUnit
-  e2 <- return $ mapTypeExpr (subst sigma) e2 -- don't use substUnit
+  args <- return $ map (second (subst sigma)) args -- don't use substDefault
+  e1 <- return $ mapTypeExpr (subst sigma) e1 -- don't use substDefault
+  e2 <- return $ mapTypeExpr (subst sigma) e2 -- don't use substDefault
   return (args, e1, e2)
diff --git a/src/Jikka/Core/Evaluate.hs b/src/Jikka/Core/Evaluate.hs
--- a/src/Jikka/Core/Evaluate.hs
+++ b/src/Jikka/Core/Evaluate.hs
@@ -187,7 +187,7 @@
     BitRightShift -> go2 valueToInt valueToInt ValInt $ \a b -> a `shift` fromInteger (- b)
     -- matrix functions
     MatAp _ _ -> go2' valueToMatrix valueToVector valueFromVector matap'
-    MatZero n -> go0 valueFromMatrix (matzero (fromInteger n))
+    MatZero h w -> go0 valueFromMatrix (matzero (fromInteger h) (fromInteger w))
     MatOne n -> go0 valueFromMatrix (matone (fromInteger n))
     MatAdd _ _ -> go2' valueToMatrix valueToMatrix valueFromMatrix matadd'
     MatMul _ _ _ -> go2' valueToMatrix valueToMatrix valueFromMatrix matmul'
diff --git a/src/Jikka/Core/Format.hs b/src/Jikka/Core/Format.hs
--- a/src/Jikka/Core/Format.hs
+++ b/src/Jikka/Core/Format.hs
@@ -114,7 +114,7 @@
   ListTy t -> (resolvePrec funCallPrec (formatType' t) ++ " list", funCallPrec)
   TupleTy ts -> case ts of
     [] -> ("unit", identPrec)
-    [t] -> (resolvePrec (pred multPrec) (formatType' t) ++ ",", multPrec)
+    [t] -> (resolvePrec funCallPrec (formatType' t) ++ " one_tuple", funCallPrec)
     _ -> (intercalate " * " (map (resolvePrec (pred multPrec) . formatType') ts), multPrec)
   FunTy t1 t2 ->
     (resolvePrecLeft impliesPrec RightToLeft (formatType' t1) ++ " -> " ++ resolvePrecRight impliesPrec RightToLeft (formatType' t2), impliesPrec)
@@ -125,16 +125,16 @@
 
 formatDataStructure :: DataStructure -> String
 formatDataStructure = \case
-  ConvexHullTrick -> "convex-hull-trick"
-  SegmentTree semigrp -> "segment-tree<" ++ formatSemigroup semigrp ++ ">"
+  ConvexHullTrick -> "convex_hull_trick"
+  SegmentTree semigrp -> "segment_tree<" ++ formatSemigroup semigrp ++ ">"
 
 formatSemigroup :: Semigroup' -> String
 formatSemigroup = \case
-  SemigroupIntPlus -> "int.plus"
-  SemigroupIntMin -> "int.min"
-  SemigroupIntMax -> "int.max"
-  SemigroupIntGcd -> "int.gcd"
-  SemigroupIntLcm -> "int.lcm"
+  SemigroupIntPlus -> "int_plus"
+  SemigroupIntMin -> "int_min"
+  SemigroupIntMax -> "int_max"
+  SemigroupIntGcd -> "int_gcd"
+  SemigroupIntLcm -> "int_lcm"
 
 data Builtin'
   = Fun String
@@ -147,6 +147,9 @@
   | If'
   deriving (Eq, Ord, Show, Read)
 
+funMat :: String -> [Integer] -> Builtin'
+funMat f args = Fun $ intercalate "@" (f : map show args)
+
 analyzeBuiltin :: Builtin -> Builtin'
 analyzeBuiltin = \case
   -- arithmetical functions
@@ -163,13 +166,13 @@
   Abs -> Fun "abs"
   Gcd -> Fun "gcd"
   Lcm -> Fun "lcm"
-  Min2 -> InfixOp "<?" appendPrec LeftToRight
-  Max2 -> InfixOp ">?" appendPrec LeftToRight
+  Min2 -> Fun "min"
+  Max2 -> Fun "max"
   -- logical functions
-  Not -> PrefixOp "not"
-  And -> InfixOp "and" andPrec RightToLeft
-  Or -> InfixOp "or" orPrec RightToLeft
-  Implies -> InfixOp "implies" impliesPrec RightToLeft
+  Not -> Fun "not"
+  And -> InfixOp "&&" andPrec RightToLeft
+  Or -> InfixOp "||" orPrec RightToLeft
+  Implies -> Fun "implies"
   If -> If'
   -- bitwise functions
   BitNot -> PrefixOp "~"
@@ -179,14 +182,14 @@
   BitLeftShift -> InfixOp "<<" powerPrec LeftToRight
   BitRightShift -> InfixOp ">>" powerPrec LeftToRight
   -- matrix functions
-  MatAp _ _ -> Fun "matap"
-  MatZero _ -> Fun "matzero"
-  MatOne _ -> Fun "matone"
-  MatAdd _ _ -> Fun "matadd"
-  MatMul _ _ _ -> Fun "matmul"
-  MatPow _ -> Fun "matpow"
-  VecFloorMod _ -> Fun "vecfloormod"
-  MatFloorMod _ _ -> Fun "matfloormod"
+  MatAp h w -> funMat "matap" [h, w]
+  MatZero h w -> funMat "matzero" [h, w]
+  MatOne n -> funMat "matone" [n]
+  MatAdd h w -> funMat "matadd" [h, w]
+  MatMul h n w -> funMat "matmul" [h, n, w]
+  MatPow n -> funMat "matpow" [n]
+  VecFloorMod n -> funMat "vecfloormod" [n]
+  MatFloorMod h w -> funMat "matfloormod" [h, w]
   -- modular functions
   ModNegate -> Fun "modnegate"
   ModPlus -> Fun "modplus"
@@ -194,10 +197,10 @@
   ModMult -> Fun "modmult"
   ModInv -> Fun "modinv"
   ModPow -> Fun "modpow"
-  ModMatAp _ _ -> Fun "modmatap"
-  ModMatAdd _ _ -> Fun "modmatadd"
-  ModMatMul _ _ _ -> Fun "modmatmul"
-  ModMatPow _ -> Fun "modmatpow"
+  ModMatAp h w -> funMat "modmatap" [h, w]
+  ModMatAdd h w -> funMat "modmatadd" [h, w]
+  ModMatMul h n w -> funMat "modmatmul" [h, n, w]
+  ModMatPow n -> funMat "modmatpow" [n]
   -- list functions
   Cons -> Fun "cons"
   Snoc -> Fun "snoc"
@@ -215,12 +218,12 @@
   Product -> Fun "product"
   ModSum -> Fun "modsum"
   ModProduct -> Fun "modproduct"
-  Min1 -> Fun "min"
-  Max1 -> Fun "max"
+  Min1 -> Fun "minimum"
+  Max1 -> Fun "maximum"
   ArgMin -> Fun "argmin"
   ArgMax -> Fun "argmax"
-  Gcd1 -> Fun "gcd"
-  Lcm1 -> Fun "lcm"
+  Gcd1 -> Fun "gcds"
+  Lcm1 -> Fun "lcms"
   All -> Fun "all"
   Any -> Fun "any"
   Sorted -> Fun "sort"
@@ -244,22 +247,22 @@
   Permute -> Fun "permute"
   MultiChoose -> Fun "multichoose"
   -- data structures
-  ConvexHullTrickInit -> Fun "cht.init"
-  ConvexHullTrickGetMin -> Fun "cht.getmin"
-  ConvexHullTrickInsert -> Fun "cht.insert"
-  SegmentTreeInitList _ -> Fun "segtree.initlist"
-  SegmentTreeGetRange _ -> Fun "segtree.getrange"
-  SegmentTreeSetPoint _ -> Fun "segtree.setpoint"
+  ConvexHullTrickInit -> Fun "cht_init"
+  ConvexHullTrickGetMin -> Fun "cht_getmin"
+  ConvexHullTrickInsert -> Fun "cht_insert"
+  SegmentTreeInitList _ -> Fun "segtree_initlist"
+  SegmentTreeGetRange _ -> Fun "segtree_getrange"
+  SegmentTreeSetPoint _ -> Fun "segtree_setpoint"
 
 formatTemplate :: [Type] -> String
-formatTemplate = \case
-  [] -> ""
-  ts -> "<" ++ intercalate ", " (map formatType ts) ++ ">"
+formatTemplate ts = concatMap (('@' :) . formatType) ts
 
 formatFunCall :: (String, Prec) -> [Expr] -> (String, Prec)
-formatFunCall f = \case
-  [] -> f
-  args -> (resolvePrec funCallPrec f ++ "(" ++ intercalate ", " (map (resolvePrec commaPrec . formatExpr') args) ++ ")", funCallPrec)
+formatFunCall f [] = f
+formatFunCall f args =
+  let f' = resolvePrecLeft funCallPrec LeftToRight f
+      args' = map (resolvePrecRight funCallPrec LeftToRight . formatExpr') args
+   in (unwords (f' : args'), funCallPrec)
 
 formatBuiltinIsolated' :: Builtin' -> [Type] -> String
 formatBuiltinIsolated' builtin ts = case builtin of
@@ -275,30 +278,30 @@
 formatBuiltinIsolated :: Builtin -> [Type] -> String
 formatBuiltinIsolated builtin ts = formatBuiltinIsolated' (analyzeBuiltin builtin) ts
 
-formatBuiltin' :: Builtin' -> [Type] -> [Expr] -> (String, Prec)
-formatBuiltin' builtin ts args = case (builtin, ts, args) of
+formatBuiltin' :: Builtin -> [Type] -> [Expr] -> (String, Prec)
+formatBuiltin' builtin ts args = case (analyzeBuiltin builtin, ts, args) of
   (Fun "map", _, [Lam x IntTy e, Range1' n]) | x `isUnusedVar` e -> formatFunCall ("replicate", identPrec) [n, e]
   (Fun name, _, _) -> formatFunCall (name, identPrec) args
   (PrefixOp op, _, e1 : args) -> formatFunCall (op ++ " " ++ resolvePrec unaryPrec (formatExpr' e1), unaryPrec) args
   (InfixOp op prec assoc, _, e1 : e2 : args) -> formatFunCall (resolvePrecLeft prec assoc (formatExpr' e1) ++ " " ++ op ++ " " ++ resolvePrecRight prec assoc (formatExpr' e2), prec) args
   (At', _, e1 : e2 : args) -> formatFunCall (resolvePrec identPrec (formatExpr' e1) ++ "[" ++ resolvePrec parenPrec (formatExpr' e2) ++ "]", identPrec) args
-  (SetAt', _, e1 : e2 : e3 : args) -> formatFunCall (resolvePrec identPrec (formatExpr' e1) ++ "[" ++ resolvePrec parenPrec (formatExpr' e2) ++ " := " ++ resolvePrec parenPrec (formatExpr' e3) ++ "]", identPrec) args
+  (SetAt', _, e1 : e2 : e3 : args) -> formatFunCall (resolvePrec identPrec (formatExpr' e1) ++ "[" ++ resolvePrec parenPrec (formatExpr' e2) ++ " <- " ++ resolvePrec parenPrec (formatExpr' e3) ++ "]", identPrec) args
   (Tuple', [_], e : args) -> formatFunCall (paren (resolvePrec commaPrec (formatExpr' e) ++ ","), identPrec) args
   (Tuple', _, args) | length args >= length ts -> formatFunCall (paren (intercalate ", " (map (resolvePrec commaPrec . formatExpr') (take (length ts) args))), identPrec) (drop (length ts) args)
   (Proj' n, _, e : args) -> formatFunCall (resolvePrec identPrec (formatExpr' e) ++ "." ++ show n, identPrec) args
   (If', _, e1 : e2 : e3 : args) -> formatFunCall ("if" ++ " " ++ resolvePrec parenPrec (formatExpr' e1) ++ " then " ++ resolvePrec parenPrec (formatExpr' e2) ++ " else " ++ resolvePrec lambdaPrec (formatExpr' e3), lambdaPrec) args
-  _ -> formatFunCall (formatBuiltinIsolated' builtin ts, identPrec) args
+  _ -> formatFunCall (formatBuiltinIsolated' (analyzeBuiltin builtin) ts, identPrec) args
 
 formatBuiltin :: Builtin -> [Type] -> [Expr] -> String
-formatBuiltin f ts args = resolvePrec parenPrec (formatBuiltin' (analyzeBuiltin f) ts args)
+formatBuiltin f ts args = resolvePrec parenPrec (formatBuiltin' f ts args)
 
 formatLiteral :: Literal -> String
 formatLiteral = \case
   LitBuiltin builtin ts -> formatBuiltinIsolated builtin ts
   LitInt n -> show n
   LitBool p -> map toLower $ show p
-  LitNil t -> "nil" ++ formatTemplate [t]
-  LitBottom t _ -> "bottom" ++ formatTemplate [t]
+  LitNil _ -> "nil"
+  LitBottom _ msg -> "bottom<" ++ show msg ++ ">"
 
 formatFormalArgs :: [(VarName, Type)] -> String
 formatFormalArgs args = unwords $ map (\(x, t) -> paren (unVarName x ++ ": " ++ formatType t)) args
@@ -311,15 +314,15 @@
     let (f, args) = curryApp e
      in case f of
           Var x -> formatFunCall (unVarName x, identPrec) args
-          Lit (LitBuiltin builtin ts) -> (formatBuiltin builtin ts args, identPrec)
+          Lit (LitBuiltin builtin ts) -> formatBuiltin' builtin ts args
           _ -> formatFunCall (formatExpr' f) args
   LamId _ -> ("id", identPrec)
   LamConst _ e -> formatFunCall ("const", identPrec) [e]
   e@(Lam _ _ _) ->
     let (args, body) = uncurryLam e
      in ("fun " ++ formatFormalArgs args ++ " ->\n" ++ indent ++ "\n" ++ resolvePrec parenPrec (formatExpr' body) ++ "\n" ++ dedent ++ "\n", lambdaPrec)
-  Let x t e1 e2 -> ("let " ++ unVarName x ++ ": " ++ formatType t ++ " =\n" ++ indent ++ "\n" ++ resolvePrec parenPrec (formatExpr' e1) ++ "\n" ++ dedent ++ "\nin " ++ resolvePrec lambdaPrec (formatExpr' e2), lambdaPrec)
-  Assert e1 e2 -> ("assert " ++ resolvePrec parenPrec (formatExpr' e1) ++ " in " ++ resolvePrec lambdaPrec (formatExpr' e2), lambdaPrec)
+  Let x t e1 e2 -> ("let " ++ unVarName x ++ ": " ++ formatType t ++ " = " ++ resolvePrec parenPrec (formatExpr' e1) ++ "\nin " ++ resolvePrec lambdaPrec (formatExpr' e2), lambdaPrec)
+  Assert e1 e2 -> ("assert " ++ resolvePrec parenPrec (formatExpr' e1) ++ " in\n" ++ resolvePrec lambdaPrec (formatExpr' e2), lambdaPrec)
 
 formatExpr :: Expr -> String
 formatExpr = unlines . makeIndentFromMarkers 4 . lines . resolvePrec parenPrec . formatExpr'
diff --git a/src/Jikka/Core/Language/ArithmeticExpr.hs b/src/Jikka/Core/Language/ArithmeticExpr.hs
new file mode 100644
--- /dev/null
+++ b/src/Jikka/Core/Language/ArithmeticExpr.hs
@@ -0,0 +1,282 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TupleSections #-}
+
+module Jikka.Core.Language.ArithmeticExpr
+  ( -- * Basic functions
+    ArithmeticExpr,
+    parseArithmeticExpr,
+    formatArithmeticExpr,
+    integerArithmeticExpr,
+    negateArithmeticExpr,
+    plusArithmeticExpr,
+    minusArithmeticExpr,
+    multArithmeticExpr,
+    isZeroArithmeticExpr,
+    isOneArithmeticExpr,
+
+    -- * Advanced functions
+    unNPlusKPattern,
+    makeVectorFromArithmeticExpr,
+    makeAffineFunctionFromArithmeticExpr,
+    splitConstantFactorArithmeticExpr,
+  )
+where
+
+import Control.Arrow
+import Control.Monad
+import Control.Monad.ST
+import Control.Monad.Trans
+import Control.Monad.Trans.Maybe
+import Data.List (findIndices, groupBy, sort, sortBy)
+import Data.STRef
+import qualified Data.Vector as V
+import qualified Data.Vector.Mutable as MV
+import Jikka.Core.Language.BuiltinPatterns
+import Jikka.Core.Language.Expr
+import Jikka.Core.Language.FreeVars
+
+data ProductExpr = ProductExpr
+  { productExprConst :: Integer,
+    productExprList :: [Expr]
+  }
+  deriving (Eq, Ord, Show, Read)
+
+data SumExpr = SumExpr
+  { sumExprList :: [ProductExpr],
+    sumExprConst :: Integer
+  }
+  deriving (Eq, Ord, Show, Read)
+
+newtype ArithmeticExpr = ArithmeticExpr {unArithmeticExpr :: SumExpr}
+  deriving (Show)
+
+instance Eq ArithmeticExpr where
+  e1 == e2 = unArithmeticExpr (normalizeArithmeticExpr e1) == unArithmeticExpr (normalizeArithmeticExpr e2)
+
+instance Ord ArithmeticExpr where
+  e1 `compare` e2 = unArithmeticExpr (normalizeArithmeticExpr e1) `compare` unArithmeticExpr (normalizeArithmeticExpr e2)
+
+integerProductExpr :: Integer -> ProductExpr
+integerProductExpr n =
+  ProductExpr
+    { productExprConst = n,
+      productExprList = []
+    }
+
+negateProductExpr :: ProductExpr -> ProductExpr
+negateProductExpr e = e {productExprConst = negate (productExprConst e)}
+
+multProductExpr :: ProductExpr -> ProductExpr -> ProductExpr
+multProductExpr e1 e2 =
+  ProductExpr
+    { productExprConst = productExprConst e1 * productExprConst e2,
+      productExprList = productExprList e1 ++ productExprList e2
+    }
+
+iterateN :: Integer -> (a -> a) -> a -> a
+iterateN n _ _ | n < 0 = error $ "iterateN: negative number: " ++ show n
+iterateN 0 _ x = x
+iterateN n f x = iterateN (n - 1) f (f x)
+
+parseProductExpr :: Expr -> ProductExpr
+parseProductExpr = \case
+  LitInt' n -> ProductExpr {productExprConst = n, productExprList = []}
+  Negate' e -> negateProductExpr (parseProductExpr e)
+  Mult' e1 e2 -> multProductExpr (parseProductExpr e1) (parseProductExpr e2)
+  Pow' e1 (LitInt' k) | 0 <= k && k < 10 -> iterateN k (multProductExpr (parseProductExpr e1)) (integerProductExpr 1)
+  e -> ProductExpr {productExprConst = 1, productExprList = [e]}
+
+sumExprFromProductExpr :: ProductExpr -> SumExpr
+sumExprFromProductExpr e =
+  SumExpr
+    { sumExprList = [e],
+      sumExprConst = 0
+    }
+
+arithmeticalExprFromProductExpr :: ProductExpr -> ArithmeticExpr
+arithmeticalExprFromProductExpr = ArithmeticExpr . sumExprFromProductExpr
+
+integerSumExpr :: Integer -> SumExpr
+integerSumExpr n =
+  SumExpr
+    { sumExprConst = n,
+      sumExprList = []
+    }
+
+integerArithmeticExpr :: Integer -> ArithmeticExpr
+integerArithmeticExpr = ArithmeticExpr . integerSumExpr
+
+negateSumExpr :: SumExpr -> SumExpr
+negateSumExpr e =
+  SumExpr
+    { sumExprList = map negateProductExpr (sumExprList e),
+      sumExprConst = negate (sumExprConst e)
+    }
+
+plusSumExpr :: SumExpr -> SumExpr -> SumExpr
+plusSumExpr e1 e2 =
+  SumExpr
+    { sumExprList = sumExprList e1 ++ sumExprList e2,
+      sumExprConst = sumExprConst e1 + sumExprConst e2
+    }
+
+multSumExpr :: SumExpr -> SumExpr -> SumExpr
+multSumExpr e1 e2 =
+  SumExpr
+    { sumExprList =
+        let es1 = parseProductExpr (LitInt' (sumExprConst e1)) : sumExprList e1
+            es2 = parseProductExpr (LitInt' (sumExprConst e2)) : sumExprList e2
+         in tail $ map (uncurry multProductExpr) ((,) <$> es1 <*> es2),
+      sumExprConst = sumExprConst e1 * sumExprConst e2
+    }
+
+negateArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr
+negateArithmeticExpr (ArithmeticExpr e) = ArithmeticExpr $ negateSumExpr e
+
+plusArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr -> ArithmeticExpr
+plusArithmeticExpr (ArithmeticExpr e1) (ArithmeticExpr e2) = ArithmeticExpr $ plusSumExpr e1 e2
+
+minusArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr -> ArithmeticExpr
+minusArithmeticExpr (ArithmeticExpr e1) (ArithmeticExpr e2) = ArithmeticExpr $ plusSumExpr e1 (negateSumExpr e2)
+
+multArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr -> ArithmeticExpr
+multArithmeticExpr (ArithmeticExpr e1) (ArithmeticExpr e2) = ArithmeticExpr $ multSumExpr e1 e2
+
+parseSumExpr :: Expr -> SumExpr
+parseSumExpr = \case
+  LitInt' n -> SumExpr {sumExprList = [], sumExprConst = n}
+  Negate' e -> negateSumExpr (parseSumExpr e)
+  Plus' e1 e2 -> plusSumExpr (parseSumExpr e1) (parseSumExpr e2)
+  Minus' e1 e2 -> plusSumExpr (parseSumExpr e1) (negateSumExpr (parseSumExpr e2))
+  Mult' e1 e2 -> multSumExpr (parseSumExpr e1) (parseSumExpr e2)
+  e -> sumExprFromProductExpr (parseProductExpr e)
+
+-- | `parseArithmeticExpr` converts a given expr to a normal form \(\sum_i \prod_j e _ {i,j})\).
+-- This assumes given exprs have the type \(\mathbf{int}\).
+parseArithmeticExpr :: Expr -> ArithmeticExpr
+parseArithmeticExpr = ArithmeticExpr . parseSumExpr
+
+formatProductExpr :: ProductExpr -> Expr
+formatProductExpr e =
+  let k = LitInt' (productExprConst e)
+      k' e' = case productExprConst e of
+        0 -> LitInt' 0
+        1 -> e'
+        -1 -> Negate' e'
+        _ -> Mult' e' k
+   in case productExprList e of
+        [] -> k
+        eHead : esTail -> k' (foldl Mult' eHead esTail)
+
+formatSumExpr :: SumExpr -> Expr
+formatSumExpr e = case sumExprList e of
+  [] -> LitInt' (sumExprConst e)
+  eHead : esTail ->
+    let op e'
+          | productExprConst e' > 0 = Plus'
+          | productExprConst e' < 0 = Minus'
+          | otherwise = const
+        go e1 e2 = op e2 e1 (formatProductExpr (e2 {productExprConst = abs (productExprConst e2)}))
+        k' e'
+          | sumExprConst e > 0 = Plus' e' (LitInt' (sumExprConst e))
+          | sumExprConst e < 0 = Minus' e' (LitInt' (abs (sumExprConst e)))
+          | otherwise = e'
+     in k' (foldl go (formatProductExpr eHead) esTail)
+
+formatArithmeticExpr :: ArithmeticExpr -> Expr
+formatArithmeticExpr = formatSumExpr . unArithmeticExpr . normalizeArithmeticExpr
+
+normalizeProductExpr :: ProductExpr -> ProductExpr
+normalizeProductExpr e =
+  let es =
+        if productExprConst e == 0
+          then []
+          else sort (productExprList e)
+   in e {productExprList = es}
+
+normalizeSumExpr :: SumExpr -> SumExpr
+normalizeSumExpr e =
+  let cmp e1 e2 = productExprList e1 `compare` productExprList e2
+      cmp' e1 e2 = cmp e1 e2 == EQ
+      es = sortBy cmp (map normalizeProductExpr (sumExprList e))
+      es' = groupBy cmp' es
+      es'' = map (\group -> ProductExpr {productExprConst = sum (map productExprConst group), productExprList = productExprList (head group)}) es'
+      es''' = filter (\e -> productExprConst e /= 0 && not (null (productExprList e))) es''
+      k = sum (map (\e -> if null (productExprList e) then productExprConst e else 0) es'')
+   in SumExpr
+        { sumExprList = es''',
+          sumExprConst = sumExprConst e + k
+        }
+
+normalizeArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr
+normalizeArithmeticExpr = ArithmeticExpr . normalizeSumExpr . unArithmeticExpr
+
+-- | `makeVectorFromArithmeticExpr` makes a vector \(f\) and a expr \(c\) from a given vector of variables \(x_0, x_1, \dots, x _ {n - 1}\) and a given expr \(e\) s.t. \(f\) and \(c\) don't have \(x_0, x_1, \dots, x _ {n - 1}\) as free variables and \(e = c + f \cdot (x_0, x_1, \dots, x _ {n - 1})\) holds.
+-- This assumes given variables and exprs have the type \(\mathbf{int}\).
+--
+-- * The returned exprs are normalized with `normalizeArithmeticExpr`.
+makeVectorFromArithmeticExpr :: V.Vector VarName -> ArithmeticExpr -> Maybe (V.Vector ArithmeticExpr, ArithmeticExpr)
+makeVectorFromArithmeticExpr xs es = runST $ do
+  runMaybeT $ do
+    f <- lift $ MV.replicate (V.length xs) (integerArithmeticExpr 0)
+    c <- lift $ newSTRef (integerArithmeticExpr (sumExprConst (unArithmeticExpr es)))
+    forM_ (sumExprList (unArithmeticExpr es)) $ \e -> do
+      let indices = V.imap (\i x -> map (i,) (findIndices (x `isFreeVar`) (productExprList e))) xs
+      case concat (V.toList indices) of
+        [] -> lift $ modifySTRef c (plusArithmeticExpr (arithmeticalExprFromProductExpr e))
+        [(i, j)] -> do
+          let e' = e {productExprList = take j (productExprList e) ++ drop (j + 1) (productExprList e)}
+          lift $ MV.modify f (plusArithmeticExpr (arithmeticalExprFromProductExpr e')) i
+        _ -> MaybeT $ return Nothing
+    f <- V.freeze f
+    c <- lift $ readSTRef c
+    return (V.map normalizeArithmeticExpr f, normalizeArithmeticExpr c)
+
+isZeroArithmeticExpr :: ArithmeticExpr -> Bool
+isZeroArithmeticExpr e = normalizeArithmeticExpr e == integerArithmeticExpr 0
+
+isOneArithmeticExpr :: ArithmeticExpr -> Bool
+isOneArithmeticExpr e = normalizeArithmeticExpr e == integerArithmeticExpr 1
+
+-- | `unNPlusKPattern` recognizes a pattern of \(x + k\) for a variable \(x\) and an integer constant \(k \in \mathbb{Z}\).
+unNPlusKPattern :: ArithmeticExpr -> Maybe (VarName, Integer)
+unNPlusKPattern e = case normalizeArithmeticExpr e of
+  ArithmeticExpr
+    SumExpr
+      { sumExprList =
+          [ ProductExpr
+              { productExprConst = 1,
+                productExprList = [Var x]
+              }
+            ],
+        sumExprConst = k
+      } -> Just (x, k)
+  _ -> Nothing
+
+-- | `makeAffineFunctionFromArithmeticExpr` is a specialized version of `makeVectorFromArithmeticExpr`.
+-- This function returns \(a, b\) for a given variable \(x\) and a given expr \(e = a x + b\) where \(a, b\) which doesn't use \(x\) free.
+makeAffineFunctionFromArithmeticExpr :: VarName -> ArithmeticExpr -> Maybe (ArithmeticExpr, ArithmeticExpr)
+makeAffineFunctionFromArithmeticExpr x es = first V.head <$> makeVectorFromArithmeticExpr (V.singleton x) es
+
+-- | `splitConstantFactorArithmeticExpr` finds \(k\) and \(e'\) for given \(e\) s.t. \(e = k e'\).
+splitConstantFactorArithmeticExpr :: ArithmeticExpr -> (Integer, ArithmeticExpr)
+splitConstantFactorArithmeticExpr e =
+  let e' = unArithmeticExpr $ normalizeArithmeticExpr e
+   in case (sumExprConst e', sumExprList e') of
+        (0, []) -> (0, integerArithmeticExpr 0)
+        (k, []) -> (k, integerArithmeticExpr 1)
+        (0, [e]) -> second arithmeticalExprFromProductExpr $ splitConstantFactorProductExpr e
+        (k, es) ->
+          let kes = map splitConstantFactorProductExpr es
+              d = foldl gcd k (map fst kes)
+           in ( d,
+                ArithmeticExpr
+                  SumExpr
+                    { sumExprConst = k `div` d,
+                      sumExprList = map (\(k, e) -> e {productExprConst = (k * productExprConst e) `div` d}) kes
+                    }
+              )
+
+splitConstantFactorProductExpr :: ProductExpr -> (Integer, ProductExpr)
+splitConstantFactorProductExpr e = (productExprConst e, e {productExprConst = 1})
diff --git a/src/Jikka/Core/Language/ArithmeticalExpr.hs b/src/Jikka/Core/Language/ArithmeticalExpr.hs
deleted file mode 100644
--- a/src/Jikka/Core/Language/ArithmeticalExpr.hs
+++ /dev/null
@@ -1,277 +0,0 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TupleSections #-}
-
-module Jikka.Core.Language.ArithmeticalExpr
-  ( -- * Basic functions
-    ArithmeticalExpr,
-    parseArithmeticalExpr,
-    formatArithmeticalExpr,
-    integerArithmeticalExpr,
-    negateArithmeticalExpr,
-    plusArithmeticalExpr,
-    minusArithmeticalExpr,
-    multArithmeticalExpr,
-    isZeroArithmeticalExpr,
-    isOneArithmeticalExpr,
-
-    -- * Advanced functions
-    unNPlusKPattern,
-    makeVectorFromArithmeticalExpr,
-    makeAffineFunctionFromArithmeticalExpr,
-    splitConstantFactorArithmeticalExpr,
-  )
-where
-
-import Control.Arrow
-import Control.Monad
-import Control.Monad.ST
-import Control.Monad.Trans
-import Control.Monad.Trans.Maybe
-import Data.List (findIndices, groupBy, sort, sortBy)
-import Data.STRef
-import qualified Data.Vector as V
-import qualified Data.Vector.Mutable as MV
-import Jikka.Core.Language.BuiltinPatterns
-import Jikka.Core.Language.Expr
-import Jikka.Core.Language.FreeVars
-
-data ProductExpr = ProductExpr
-  { productExprConst :: Integer,
-    productExprList :: [Expr]
-  }
-  deriving (Eq, Ord, Show, Read)
-
-data SumExpr = SumExpr
-  { sumExprList :: [ProductExpr],
-    sumExprConst :: Integer
-  }
-  deriving (Eq, Ord, Show, Read)
-
-newtype ArithmeticalExpr = ArithmeticalExpr {unArithmeticalExpr :: SumExpr}
-  deriving (Show)
-
-instance Eq ArithmeticalExpr where
-  e1 == e2 = unArithmeticalExpr (normalizeArithmeticalExpr e1) == unArithmeticalExpr (normalizeArithmeticalExpr e2)
-
-instance Ord ArithmeticalExpr where
-  e1 `compare` e2 = unArithmeticalExpr (normalizeArithmeticalExpr e1) `compare` unArithmeticalExpr (normalizeArithmeticalExpr e2)
-
-integerProductExpr :: Integer -> ProductExpr
-integerProductExpr n =
-  ProductExpr
-    { productExprConst = n,
-      productExprList = []
-    }
-
-negateProductExpr :: ProductExpr -> ProductExpr
-negateProductExpr e = e {productExprConst = negate (productExprConst e)}
-
-multProductExpr :: ProductExpr -> ProductExpr -> ProductExpr
-multProductExpr e1 e2 =
-  ProductExpr
-    { productExprConst = productExprConst e1 * productExprConst e2,
-      productExprList = productExprList e1 ++ productExprList e2
-    }
-
-parseProductExpr :: Expr -> ProductExpr
-parseProductExpr = \case
-  LitInt' n -> ProductExpr {productExprConst = n, productExprList = []}
-  Negate' e -> negateProductExpr (parseProductExpr e)
-  Mult' e1 e2 -> multProductExpr (parseProductExpr e1) (parseProductExpr e2)
-  Pow' e1 (LitInt' k) | 0 <= k && k < 10 -> iterate (multProductExpr (parseProductExpr e1)) (integerProductExpr 1) !! fromInteger k
-  e -> ProductExpr {productExprConst = 1, productExprList = [e]}
-
-sumExprFromProductExpr :: ProductExpr -> SumExpr
-sumExprFromProductExpr e =
-  SumExpr
-    { sumExprList = [e],
-      sumExprConst = 0
-    }
-
-arithmeticalExprFromProductExpr :: ProductExpr -> ArithmeticalExpr
-arithmeticalExprFromProductExpr = ArithmeticalExpr . sumExprFromProductExpr
-
-integerSumExpr :: Integer -> SumExpr
-integerSumExpr n =
-  SumExpr
-    { sumExprConst = n,
-      sumExprList = []
-    }
-
-integerArithmeticalExpr :: Integer -> ArithmeticalExpr
-integerArithmeticalExpr = ArithmeticalExpr . integerSumExpr
-
-negateSumExpr :: SumExpr -> SumExpr
-negateSumExpr e =
-  SumExpr
-    { sumExprList = map negateProductExpr (sumExprList e),
-      sumExprConst = negate (sumExprConst e)
-    }
-
-plusSumExpr :: SumExpr -> SumExpr -> SumExpr
-plusSumExpr e1 e2 =
-  SumExpr
-    { sumExprList = sumExprList e1 ++ sumExprList e2,
-      sumExprConst = sumExprConst e1 + sumExprConst e2
-    }
-
-multSumExpr :: SumExpr -> SumExpr -> SumExpr
-multSumExpr e1 e2 =
-  SumExpr
-    { sumExprList =
-        let es1 = parseProductExpr (LitInt' (sumExprConst e1)) : sumExprList e1
-            es2 = parseProductExpr (LitInt' (sumExprConst e2)) : sumExprList e2
-         in tail $ map (uncurry multProductExpr) ((,) <$> es1 <*> es2),
-      sumExprConst = sumExprConst e1 * sumExprConst e2
-    }
-
-negateArithmeticalExpr :: ArithmeticalExpr -> ArithmeticalExpr
-negateArithmeticalExpr (ArithmeticalExpr e) = ArithmeticalExpr $ negateSumExpr e
-
-plusArithmeticalExpr :: ArithmeticalExpr -> ArithmeticalExpr -> ArithmeticalExpr
-plusArithmeticalExpr (ArithmeticalExpr e1) (ArithmeticalExpr e2) = ArithmeticalExpr $ plusSumExpr e1 e2
-
-minusArithmeticalExpr :: ArithmeticalExpr -> ArithmeticalExpr -> ArithmeticalExpr
-minusArithmeticalExpr (ArithmeticalExpr e1) (ArithmeticalExpr e2) = ArithmeticalExpr $ plusSumExpr e1 (negateSumExpr e2)
-
-multArithmeticalExpr :: ArithmeticalExpr -> ArithmeticalExpr -> ArithmeticalExpr
-multArithmeticalExpr (ArithmeticalExpr e1) (ArithmeticalExpr e2) = ArithmeticalExpr $ multSumExpr e1 e2
-
-parseSumExpr :: Expr -> SumExpr
-parseSumExpr = \case
-  LitInt' n -> SumExpr {sumExprList = [], sumExprConst = n}
-  Negate' e -> negateSumExpr (parseSumExpr e)
-  Plus' e1 e2 -> plusSumExpr (parseSumExpr e1) (parseSumExpr e2)
-  Minus' e1 e2 -> plusSumExpr (parseSumExpr e1) (negateSumExpr (parseSumExpr e2))
-  Mult' e1 e2 -> multSumExpr (parseSumExpr e1) (parseSumExpr e2)
-  e -> sumExprFromProductExpr (parseProductExpr e)
-
--- | `parseArithmeticalExpr` converts a given expr to a normal form \(\sum_i \prod_j e _ {i,j})\).
--- This assumes given exprs have the type \(\mathbf{int}\).
-parseArithmeticalExpr :: Expr -> ArithmeticalExpr
-parseArithmeticalExpr = ArithmeticalExpr . parseSumExpr
-
-formatProductExpr :: ProductExpr -> Expr
-formatProductExpr e =
-  let k = LitInt' (productExprConst e)
-      k' e' = case productExprConst e of
-        0 -> LitInt' 0
-        1 -> e'
-        -1 -> Negate' e'
-        _ -> Mult' e' k
-   in case productExprList e of
-        [] -> k
-        eHead : esTail -> k' (foldl Mult' eHead esTail)
-
-formatSumExpr :: SumExpr -> Expr
-formatSumExpr e = case sumExprList e of
-  [] -> LitInt' (sumExprConst e)
-  eHead : esTail ->
-    let op e'
-          | productExprConst e' > 0 = Plus'
-          | productExprConst e' < 0 = Minus'
-          | otherwise = const
-        go e1 e2 = op e2 e1 (formatProductExpr (e2 {productExprConst = abs (productExprConst e2)}))
-        k' e'
-          | sumExprConst e > 0 = Plus' e' (LitInt' (sumExprConst e))
-          | sumExprConst e < 0 = Minus' e' (LitInt' (abs (sumExprConst e)))
-          | otherwise = e'
-     in k' (foldl go (formatProductExpr eHead) esTail)
-
-formatArithmeticalExpr :: ArithmeticalExpr -> Expr
-formatArithmeticalExpr = formatSumExpr . unArithmeticalExpr . normalizeArithmeticalExpr
-
-normalizeProductExpr :: ProductExpr -> ProductExpr
-normalizeProductExpr e =
-  let es =
-        if productExprConst e == 0
-          then []
-          else sort (productExprList e)
-   in e {productExprList = es}
-
-normalizeSumExpr :: SumExpr -> SumExpr
-normalizeSumExpr e =
-  let cmp e1 e2 = productExprList e1 `compare` productExprList e2
-      cmp' e1 e2 = cmp e1 e2 == EQ
-      es = sortBy cmp (map normalizeProductExpr (sumExprList e))
-      es' = groupBy cmp' es
-      es'' = map (\group -> ProductExpr {productExprConst = sum (map productExprConst group), productExprList = productExprList (head group)}) es'
-      es''' = filter (\e -> productExprConst e /= 0 && not (null (productExprList e))) es''
-      k = sum (map (\e -> if null (productExprList e) then productExprConst e else 0) es'')
-   in SumExpr
-        { sumExprList = es''',
-          sumExprConst = sumExprConst e + k
-        }
-
-normalizeArithmeticalExpr :: ArithmeticalExpr -> ArithmeticalExpr
-normalizeArithmeticalExpr = ArithmeticalExpr . normalizeSumExpr . unArithmeticalExpr
-
--- | `makeVectorFromArithmeticalExpr` makes a vector \(f\) and a expr \(c\) from a given vector of variables \(x_0, x_1, \dots, x _ {n - 1}\) and a given expr \(e\) s.t. \(f\) and \(c\) don't have \(x_0, x_1, \dots, x _ {n - 1}\) as free variables and \(e = c + f \cdot (x_0, x_1, \dots, x _ {n - 1})\) holds.
--- This assumes given variables and exprs have the type \(\mathbf{int}\).
---
--- * The returned exprs are normalized with `normalizeArithmeticalExpr`.
-makeVectorFromArithmeticalExpr :: V.Vector VarName -> ArithmeticalExpr -> Maybe (V.Vector ArithmeticalExpr, ArithmeticalExpr)
-makeVectorFromArithmeticalExpr xs es = runST $ do
-  runMaybeT $ do
-    f <- lift $ MV.replicate (V.length xs) (integerArithmeticalExpr 0)
-    c <- lift $ newSTRef (integerArithmeticalExpr (sumExprConst (unArithmeticalExpr es)))
-    forM_ (sumExprList (unArithmeticalExpr es)) $ \e -> do
-      let indices = V.imap (\i x -> map (i,) (findIndices (x `isFreeVar`) (productExprList e))) xs
-      case concat (V.toList indices) of
-        [] -> lift $ modifySTRef c (plusArithmeticalExpr (arithmeticalExprFromProductExpr e))
-        [(i, j)] -> do
-          let e' = e {productExprList = take j (productExprList e) ++ drop (j + 1) (productExprList e)}
-          lift $ MV.modify f (plusArithmeticalExpr (arithmeticalExprFromProductExpr e')) i
-        _ -> MaybeT $ return Nothing
-    f <- V.freeze f
-    c <- lift $ readSTRef c
-    return (V.map normalizeArithmeticalExpr f, normalizeArithmeticalExpr c)
-
-isZeroArithmeticalExpr :: ArithmeticalExpr -> Bool
-isZeroArithmeticalExpr e = normalizeArithmeticalExpr e == integerArithmeticalExpr 0
-
-isOneArithmeticalExpr :: ArithmeticalExpr -> Bool
-isOneArithmeticalExpr e = normalizeArithmeticalExpr e == integerArithmeticalExpr 1
-
--- | `unNPlusKPattern` recognizes a pattern of \(x + k\) for a variable \(x\) and an integer constant \(k \in \mathbb{Z}\).
-unNPlusKPattern :: ArithmeticalExpr -> Maybe (VarName, Integer)
-unNPlusKPattern e = case normalizeArithmeticalExpr e of
-  ArithmeticalExpr
-    SumExpr
-      { sumExprList =
-          [ ProductExpr
-              { productExprConst = 1,
-                productExprList = [Var x]
-              }
-            ],
-        sumExprConst = k
-      } -> Just (x, k)
-  _ -> Nothing
-
--- | `makeAffineFunctionFromArithmeticalExpr` is a specialized version of `makeVectorFromArithmeticalExpr`.
--- This function returns \(a, b\) for a given variable \(x\) and a given expr \(e = a x + b\) where \(a, b\) which doesn't use \(x\) free.
-makeAffineFunctionFromArithmeticalExpr :: VarName -> ArithmeticalExpr -> Maybe (ArithmeticalExpr, ArithmeticalExpr)
-makeAffineFunctionFromArithmeticalExpr x es = first V.head <$> makeVectorFromArithmeticalExpr (V.singleton x) es
-
--- | `splitConstantFactorArithmeticalExpr` finds \(k\) and \(e'\) for given \(e\) s.t. \(e = k e'\).
-splitConstantFactorArithmeticalExpr :: ArithmeticalExpr -> (Integer, ArithmeticalExpr)
-splitConstantFactorArithmeticalExpr e =
-  let e' = unArithmeticalExpr $ normalizeArithmeticalExpr e
-   in case (sumExprConst e', sumExprList e') of
-        (0, []) -> (0, integerArithmeticalExpr 0)
-        (k, []) -> (k, integerArithmeticalExpr 1)
-        (0, [e]) -> second arithmeticalExprFromProductExpr $ splitConstantFactorProductExpr e
-        (k, es) ->
-          let kes = map splitConstantFactorProductExpr es
-              d = foldl gcd k (map fst kes)
-           in ( d,
-                ArithmeticalExpr
-                  SumExpr
-                    { sumExprConst = k `div` d,
-                      sumExprList = map (\(k, e) -> e {productExprConst = (k * productExprConst e) `div` d}) kes
-                    }
-              )
-
-splitConstantFactorProductExpr :: ProductExpr -> (Integer, ProductExpr)
-splitConstantFactorProductExpr e = (productExprConst e, e {productExprConst = 1})
diff --git a/src/Jikka/Core/Language/Expr.hs b/src/Jikka/Core/Language/Expr.hs
--- a/src/Jikka/Core/Language/Expr.hs
+++ b/src/Jikka/Core/Language/Expr.hs
@@ -136,8 +136,8 @@
 
     -- | matrix application \(: \int^{H \times W} \to \int^W \to \int^H\)
     MatAp Integer Integer
-  | -- | zero matrix \(: \to \int^{n \times n}\)
-    MatZero Integer
+  | -- | zero matrix \(: \to \int^{h \times w}\)
+    MatZero Integer Integer
   | -- | unit matrix \(: \to \int^{n \times n}\)
     MatOne Integer
   | -- | matrix addition \(: \int^{H \times W} \to \int^{H \times W} \to \int^{H \times W}\)
@@ -235,6 +235,8 @@
     -- | \(: \forall \alpha_0 \alpha_1 \dots \alpha _ {n - 1}. \alpha_0 \to \dots \to \alpha _ {n - 1} \to \alpha_0 \times \dots \times \alpha _ {n - 1}\)
     Tuple
   | -- | \(: \forall \alpha_0 \alpha_1 \dots \alpha _ {n - 1}. \alpha_0 \times \dots \times \alpha _ {n - 1} \to \alpha_i\)
+    --
+    -- `Jikka.Core.Parse` may make broken `Proj` with its list of type arguments is empty. This is fixed by `Jikka.Core.Convert.TypeInfer` module.
     Proj Integer
   | -- comparison
 
diff --git a/src/Jikka/Core/Language/TypeCheck.hs b/src/Jikka/Core/Language/TypeCheck.hs
--- a/src/Jikka/Core/Language/TypeCheck.hs
+++ b/src/Jikka/Core/Language/TypeCheck.hs
@@ -58,7 +58,7 @@
         BitRightShift -> go0 $ Fun2STy IntTy
         -- matrix functions
         MatAp h w -> go0 $ Fun2Ty (matrixTy h w) (vectorTy w) (vectorTy h)
-        MatZero n -> go0 $ matrixTy n n
+        MatZero h w -> go0 $ matrixTy h w
         MatOne n -> go0 $ matrixTy n n
         MatAdd h w -> go0 $ Fun2Ty (matrixTy h w) (matrixTy h w) (matrixTy h w)
         MatMul h n w -> go0 $ Fun2Ty (matrixTy h n) (matrixTy n w) (matrixTy h w)
@@ -107,7 +107,10 @@
         Range3 -> go0 $ Fun3Ty IntTy IntTy IntTy (ListTy IntTy)
         -- tuple functions
         Tuple -> return $ curryFunTy ts (TupleTy ts)
-        Proj n -> return $ FunTy (TupleTy ts) (ts !! fromInteger n)
+        Proj n ->
+          if 0 <= n && n < toInteger (length ts)
+            then return $ FunTy (TupleTy ts) (ts !! fromInteger n)
+            else throwTypeError $ "projection index is out of range: type = " ++ formatType (TupleTy ts) ++ ", index = " ++ show n
         -- comparison
         LessThan -> go1 $ \t -> Fun2Ty t t BoolTy
         LessEqual -> go1 $ \t -> Fun2Ty t t BoolTy
diff --git a/src/Jikka/Core/Language/Util.hs b/src/Jikka/Core/Language/Util.hs
--- a/src/Jikka/Core/Language/Util.hs
+++ b/src/Jikka/Core/Language/Util.hs
@@ -77,11 +77,11 @@
 mapTypeProgram :: (Type -> Type) -> Program -> Program
 mapTypeProgram f prog = runIdentity (mapTypeProgramM (return . f) prog)
 
--- | `mapExprM'` substitutes exprs using given two functions, which are called in pre-order and post-order.
-mapExprM' :: Monad m => ([(VarName, Type)] -> Expr -> m Expr) -> ([(VarName, Type)] -> Expr -> m Expr) -> [(VarName, Type)] -> Expr -> m Expr
-mapExprM' pre post env e = do
+-- | `mapSubExprM'` substitutes exprs using given two functions, which are called in pre-order and post-order.
+mapSubExprM' :: Monad m => ([(VarName, Type)] -> Expr -> m Expr) -> ([(VarName, Type)] -> Expr -> m Expr) -> [(VarName, Type)] -> Expr -> m Expr
+mapSubExprM' pre post env e = do
   e <- pre env e
-  let go = mapExprM' pre post
+  let go = mapSubExprM' pre post
   e <- case e of
     Var y -> return $ Var y
     Lit lit -> return $ Lit lit
@@ -105,37 +105,32 @@
       ToplevelAssert e <$> mapToplevelExprM' pre post env cont
   post env e
 
-mapExprToplevelExprM' :: Monad m => ([(VarName, Type)] -> Expr -> m Expr) -> ([(VarName, Type)] -> Expr -> m Expr) -> [(VarName, Type)] -> ToplevelExpr -> m ToplevelExpr
-mapExprToplevelExprM' pre post env = mapToplevelExprM' pre' (\_ e -> return e) env
+mapExprToplevelExprM :: Monad m => ([(VarName, Type)] -> Expr -> m Expr) -> [(VarName, Type)] -> ToplevelExpr -> m ToplevelExpr
+mapExprToplevelExprM f env = mapToplevelExprM' pre' (\_ e -> return e) env
   where
-    go = mapExprM' pre post
     pre' env = \case
-      ResultExpr e -> ResultExpr <$> go env e
-      ToplevelLet y t e cont -> ToplevelLet y t <$> go env e <*> pure cont
+      ResultExpr e -> ResultExpr <$> f env e
+      ToplevelLet y t e cont -> ToplevelLet y t <$> f env e <*> pure cont
       ToplevelLetRec g args ret body cont ->
         let env' = (g, foldr (FunTy . snd) ret args) : env
-         in ToplevelLetRec g args ret <$> go (reverse args ++ env') body <*> pure cont
-      ToplevelAssert e cont -> ToplevelAssert <$> go env e <*> pure cont
-
-mapExprProgramM' :: Monad m => ([(VarName, Type)] -> Expr -> m Expr) -> ([(VarName, Type)] -> Expr -> m Expr) -> Program -> m Program
-mapExprProgramM' pre post = mapExprToplevelExprM' pre post []
-
--- | `mapExprM` is a wrapper of `mapExprM'`. This function works in post-order.
-mapExprM :: Monad m => ([(VarName, Type)] -> Expr -> m Expr) -> [(VarName, Type)] -> Expr -> m Expr
-mapExprM f = mapExprM' (\_ e -> return e) f
-
-mapExprToplevelExprM :: Monad m => ([(VarName, Type)] -> Expr -> m Expr) -> [(VarName, Type)] -> ToplevelExpr -> m ToplevelExpr
-mapExprToplevelExprM f = mapExprToplevelExprM' (\_ e -> return e) f
+         in ToplevelLetRec g args ret <$> f (reverse args ++ env') body <*> pure cont
+      ToplevelAssert e cont -> ToplevelAssert <$> f env e <*> pure cont
 
 mapExprProgramM :: Monad m => ([(VarName, Type)] -> Expr -> m Expr) -> Program -> m Program
-mapExprProgramM f = mapExprProgramM' (\_ e -> return e) f
+mapExprProgramM f = mapExprToplevelExprM f []
 
-mapExpr :: ([(VarName, Type)] -> Expr -> Expr) -> [(VarName, Type)] -> Expr -> Expr
-mapExpr f env e = runIdentity $ mapExprM (\env e -> return $ f env e) env e
+-- | `mapSubExprM` is a wrapper of `mapSubExprM'`. This function works in post-order.
+mapSubExprM :: Monad m => ([(VarName, Type)] -> Expr -> m Expr) -> [(VarName, Type)] -> Expr -> m Expr
+mapSubExprM f = mapSubExprM' (\_ e -> return e) f
 
+mapSubExpr :: ([(VarName, Type)] -> Expr -> Expr) -> [(VarName, Type)] -> Expr -> Expr
+mapSubExpr f env e = runIdentity $ mapSubExprM (\env e -> return $ f env e) env e
+
 mapExprToplevelExpr :: ([(VarName, Type)] -> Expr -> Expr) -> [(VarName, Type)] -> ToplevelExpr -> ToplevelExpr
 mapExprToplevelExpr f env e = runIdentity $ mapExprToplevelExprM (\env e -> return $ f env e) env e
 
+-- | @mapExprProgram f prog@ applies @f@ to each root exprs in @prog@.
+-- This doesn't run into sub-exprs. For example, @toplevel-let x = (e1 + e2) in ...@ becomes @toplevel-let x = (f (e1 + e2)) in ...@, instead of @toplevel-let x = (f (f e1 + f e2)) in ...@
 mapExprProgram :: ([(VarName, Type)] -> Expr -> Expr) -> Program -> Program
 mapExprProgram f prog = runIdentity $ mapExprProgramM (\env e -> return $ f env e) prog
 
@@ -150,7 +145,7 @@
 mapToplevelExprProgram f prog = runIdentity $ mapToplevelExprProgramM (\env e -> return $ f env e) prog
 
 listSubExprs :: Expr -> [Expr]
-listSubExprs e = getDual . execWriter $ mapExprM go [] e
+listSubExprs e = getDual . execWriter $ mapSubExprM go [] e
   where
     go _ e = do
       tell $ Dual [e]
@@ -236,7 +231,7 @@
   BitRightShift -> True
   -- matrix functions
   MatAp _ _ -> True
-  MatZero _ -> True
+  MatZero _ _ -> True
   MatOne _ -> True
   MatAdd _ _ -> True
   MatMul _ _ _ -> True
diff --git a/src/Jikka/Core/Parse/Alex.x b/src/Jikka/Core/Parse/Alex.x
--- a/src/Jikka/Core/Parse/Alex.x
+++ b/src/Jikka/Core/Parse/Alex.x
@@ -93,10 +93,8 @@
     "**"            { tok (Operator Pow) }
 
     -- boolean operators
-    "and"           { tok (Operator And) }
-    "or"            { tok (Operator Or) }
-    "not"           { tok (Operator Not) }
-    "implies"       { tok (Operator Implies) }
+    "&&"            { tok (Operator And) }
+    "||"            { tok (Operator Or) }
 
     -- bit operators
     "~"             { tok (Operator BitNot) }
@@ -106,10 +104,6 @@
     "<<"            { tok (Operator BitLShift) }
     ">>"            { tok (Operator BitRShift) }
 
-    -- min max operators
-    "<?"            { tok (Operator Min) }
-    ">?"            { tok (Operator Max) }
-
     -- comparators
     ">"             { tok (Operator GreaterThan) }
     "<"             { tok (Operator LessThan) }
@@ -121,6 +115,7 @@
     -- identifier
     $alpha ($alnum | "_") *                 { tok' Ident }
     $alpha ($alnum | "_") * "$" $digit +    { tok' Ident }
+    "$" $digit +                            { tok' Ident }
 
     -- catch error
     .               { skip' }
diff --git a/src/Jikka/Core/Parse/Happy.y b/src/Jikka/Core/Parse/Happy.y
--- a/src/Jikka/Core/Parse/Happy.y
+++ b/src/Jikka/Core/Parse/Happy.y
@@ -28,6 +28,7 @@
 import Jikka.Common.Location
 import Jikka.Core.Language.BuiltinPatterns
 import Jikka.Core.Language.Expr
+import Jikka.Core.Language.TypeCheck
 import Jikka.Core.Language.Util
 import qualified Jikka.Core.Parse.Token as L
 }
@@ -79,6 +80,7 @@
     "bool"          { WithLoc _ (L.Ident "bool") }
     "list"          { WithLoc _ (L.Ident "list") }
     "unit"          { WithLoc _ (L.Ident "unit") }
+    "one_tuple"     { WithLoc _ (L.Ident "one_tuple") }
     "convex_hull_trick" { WithLoc _ (L.Ident "convex_hull_trick") }
     "segment_tree"  { WithLoc _ (L.Ident "segment_tree") }
     "int_plus"      { WithLoc _ (L.Ident "int_plus") }
@@ -90,6 +92,10 @@
     "abs"           { WithLoc _ (L.Ident "abs") }
     "gcd"           { WithLoc _ (L.Ident "gcd") }
     "lcm"           { WithLoc _ (L.Ident "lcm") }
+    "max"           { WithLoc _ (L.Ident "max") }
+    "min"           { WithLoc _ (L.Ident "min") }
+    "not"           { WithLoc _ (L.Ident "not") }
+    "implies"       { WithLoc _ (L.Ident "implies") }
     "iterate"       { WithLoc _ (L.Ident "iterate") }
     "matap"         { WithLoc _ (L.Ident "matap") }
     "matzero"       { WithLoc _ (L.Ident "matzero") }
@@ -122,10 +128,12 @@
     "product"       { WithLoc _ (L.Ident "product") }
     "modsum"        { WithLoc _ (L.Ident "modsum") }
     "modproduct"    { WithLoc _ (L.Ident "modproduct") }
-    "min"           { WithLoc _ (L.Ident "min") }
-    "max"           { WithLoc _ (L.Ident "max") }
+    "minimum"       { WithLoc _ (L.Ident "minimum") }
+    "maximum"       { WithLoc _ (L.Ident "maximum") }
     "argmin"        { WithLoc _ (L.Ident "argmin") }
     "argmax"        { WithLoc _ (L.Ident "argmax") }
+    "gcds"          { WithLoc _ (L.Ident "gcds") }
+    "lcms"          { WithLoc _ (L.Ident "lcms") }
     "all"           { WithLoc _ (L.Ident "all") }
     "any"           { WithLoc _ (L.Ident "any") }
     "sorted"        { WithLoc _ (L.Ident "sorted") }
@@ -158,10 +166,8 @@
     "**"            { WithLoc _ (L.Operator L.Pow) }
 
     -- boolean operators
-    "and"           { WithLoc _ (L.Operator L.And) }
-    "or"            { WithLoc _ (L.Operator L.Or) }
-    "not"           { WithLoc _ (L.Operator L.Not) }
-    "implies"       { WithLoc _ (L.Operator L.Implies) }
+    "&&"             { WithLoc _ (L.Operator L.And) }
+    "||"             { WithLoc _ (L.Operator L.Or) }
 
     -- bit operators
     "~"             { WithLoc _ (L.Operator L.BitNot) }
@@ -171,10 +177,6 @@
     "<<"            { WithLoc _ (L.Operator L.BitLShift) }
     ">>"            { WithLoc _ (L.Operator L.BitRShift) }
 
-    -- min max operators
-    "<?"            { WithLoc _ (L.Operator L.Min) }
-    ">?"            { WithLoc _ (L.Operator L.Max) }
-
     -- comparators
     ">"             { WithLoc _ (L.Operator L.GreaterThan) }
     "<"             { WithLoc _ (L.Operator L.LessThan) }
@@ -232,6 +234,7 @@
     | "bool"                           { BoolTy }
     | atom_type "list"                 { ListTy $1 }
     | "unit"                           { TupleTy [] }
+    | atom_type "one_tuple"            { TupleTy [$1] }
     | datastructure                    { DataStructureTy $1 }
     | "(" type ")"                     { $2 }
 
@@ -291,26 +294,32 @@
     : "abs"                            { (Abs, []) }
     | "gcd"                            { (Gcd, []) }
     | "lcm"                            { (Lcm, []) }
+    | "min"                            { (Min2, [underscoreTy]) }
+    | "min" "@" atom_type              { (Min2, [$3]) }
+    | "max"                            { (Max2, [underscoreTy]) }
+    | "max" "@" atom_type              { (Max2, [$3]) }
+    | "not"                            { (Not, []) }
+    | "implies"                        { (Implies, []) }
     | "iterate"                        { (Iterate, [underscoreTy]) }
     | "iterate" "@" atom_type          { (Iterate, [$3]) }
-    | "matap" integer integer          { (MatAp $2 $3, []) }
-    | "matzero" integer                { (MatZero $2, []) }
-    | "matone" integer                 { (MatOne $2, []) }
-    | "matadd" integer integer         { (MatAdd $2 $3, []) }
-    | "matmul" integer integer integer { (MatMul $2 $3 $4, []) }
-    | "matpow" integer                 { (MatPow $2, []) }
-    | "vecfloormod" integer            { (VecFloorMod $2, []) }
-    | "matfloormod" integer integer    { (MatFloorMod $2 $3, []) }
+    | "matap" "@" integer "@" integer  { (MatAp $3 $5, []) }
+    | "matzero" "@" integer "@" integer    { (MatZero $3 $5, []) }
+    | "matone" "@" integer             { (MatOne $3, []) }
+    | "matadd" "@" integer "@" integer { (MatAdd $3 $5, []) }
+    | "matmul" "@" integer "@" integer "@" integer { (MatMul $3 $5 $7, []) }
+    | "matpow" "@" integer             { (MatPow $3, []) }
+    | "vecfloormod" "@" integer        { (VecFloorMod $3, []) }
+    | "matfloormod" "@" integer "@" integer    { (MatFloorMod $3 $5, []) }
     | "modnegate"                      { (ModNegate, []) }
     | "modplus"                        { (ModPlus, []) }
     | "modminus"                       { (ModMinus, []) }
     | "modmult"                        { (ModMult, []) }
     | "modinv"                         { (ModInv, []) }
     | "modpow"                         { (ModPow, []) }
-    | "modmatap" integer integer       { (ModMatAp $2 $3, []) }
-    | "modmatadd" integer integer      { (ModMatAdd $2 $3, []) }
-    | "modmatmul" integer integer integer    { (ModMatMul $2 $3 $4, []) }
-    | "modmatpow" integer              { (ModMatPow $2, []) }
+    | "modmatap" "@" integer "@" integer    { (ModMatAp $3 $5, []) }
+    | "modmatadd" "@" integer "@" integer    { (ModMatAdd $3 $5, []) }
+    | "modmatmul" "@" integer "@" integer "@" integer    { (ModMatMul $3 $5 $7, []) }
+    | "modmatpow" "@" integer          { (ModMatPow $3, []) }
     | "cons"                           { (Cons, [underscoreTy]) }
     | "cons" "@" atom_type             { (Cons, [$3]) }
     | "snoc"                           { (Snoc, [underscoreTy]) }
@@ -333,14 +342,16 @@
     | "product"                        { (Product, []) }
     | "modsum"                         { (ModSum, []) }
     | "modproduct"                     { (ModProduct, []) }
-    | "min"                            { (Min1, [underscoreTy]) }
-    | "min" "@" atom_type              { (Min1, [$3]) }
-    | "max"                            { (Max1, [underscoreTy]) }
-    | "max" "@" atom_type              { (Max1, [$3]) }
+    | "minimum"                        { (Min1, [underscoreTy]) }
+    | "minimum" "@" atom_type          { (Min1, [$3]) }
+    | "maximum"                        { (Max1, [underscoreTy]) }
+    | "maximum" "@" atom_type          { (Max1, [$3]) }
     | "argmin"                         { (ArgMin, [underscoreTy]) }
     | "argmin" "@" atom_type           { (ArgMin, [$3]) }
     | "argmax"                         { (ArgMax, [underscoreTy]) }
     | "argmax" "@" atom_type           { (ArgMax, [$3]) }
+    | "gcds"                           { (Gcd1, []) }
+    | "lcms"                           { (Lcm1, []) }
     | "all"                            { (All, []) }
     | "any"                            { (Any, []) }
     | "sorted"                         { (Sorted, [underscoreTy]) }
@@ -372,7 +383,7 @@
     | primary "[" expression "]" "@" atom_type              { At' $6 $1 $3 }
     | primary "[" expression "<-" expression "]"            { SetAt' underscoreTy $1 $3 $5 }
     | primary "[" expression "<-" expression "]" "@" atom_type    { SetAt' $8 $1 $3 $5 }
-    -- | primary "." integer                                   {% makeProj $1 $3 underscoreTy }
+    | primary "." integer                                   {% makeProj $1 $3 underscoreTy }
     | primary "." integer "@" atom_type                     {% makeProj $1 $3 $5 }
 
 -- Function applications
@@ -422,19 +433,11 @@
     : xor_expr                                              { $1 }
     | or_expr "|" xor_expr                                  { BitOr' $1 $3 }
 
--- Min and max operations
-min_expr :: { Expr }
-    : or_expr                                               { $1 }
-    | min_expr "<?" or_expr                                 { Min2' underscoreTy $1 $3 }
-    | min_expr "<?" "@" atom_type or_expr                   { Min2' $4 $1 $5 }
-    | min_expr ">?" or_expr                                 { Max2' underscoreTy $1 $3 }
-    | min_expr ">?" "@" atom_type or_expr                   { Max2' $4 $1 $5 }
-
 -- Comparisons
 comparison :: { Expr }
-    : min_expr                                              { $1 }
-    | comparison comp_operator min_expr                     { $2 underscoreTy $1 $3 }
-    | comparison comp_operator "@" atom_type min_expr       { $2 $4 $1 $5 }
+    : or_expr                                               { $1 }
+    | comparison comp_operator or_expr                      { $2 underscoreTy $1 $3 }
+    | comparison comp_operator "@" atom_type or_expr        { $2 $4 $1 $5 }
 comp_operator :: { Type -> Expr -> Expr -> Expr }
     : "=="                                                  { Equal' }
     | "/="                                                  { NotEqual' }
@@ -444,20 +447,12 @@
     | ">="                                                  { GreaterEqual' }
 
 -- Boolean operations
-not_test :: { Expr }
-    : comparison                                            { $1 }
-    | "not" not_test                                        { Not' $2 }
 and_test :: { Expr }
-    : not_test                                              { $1 }
-    | and_test "and" not_test                               { And' $1 $3 }
+    : comparison                                            { $1 }
+    | and_test "&&" comparison                              { And' $1 $3 }
 or_test :: { Expr }
     : and_test                                              { $1 }
-    | or_test "or" and_test                                 { Or' $1 $3 }
-
--- Implication operation
-implies_test :: { Expr }
-    : or_test                                               { $1 }
-    | or_test "implies" implies_test                        { Implies' $1 $3 }
+    | or_test "||" and_test                                 { Or' $1 $3 }
 
 -- Conditional expressions
 conditional_expression :: { Expr }
@@ -477,7 +472,7 @@
     : "assert" expression "->" expression                       { Assert $2 $4 }
 
 expression_nolet :: { Expr }
-    : implies_test                                          { $1 }
+    : or_test                                               { $1 }
     | conditional_expression                                { $1 }
     | lambda_expr                                           { $1 }
     | assert_expr                                           { $1 }
@@ -503,8 +498,9 @@
 
 makeProj :: MonadError Error m => Expr -> Integer -> Type -> m Expr
 makeProj e n t = case t of
+    t | t == underscoreTy -> return $ Proj' [] n e -- A projection from the empty tuple is fixed in Jikka.Core.Convert.TypeInfer.
     TupleTy ts -> return $ Proj' ts n e
-    _ -> throwSyntaxError "Jikka.Core.Parse.Happy.makeTuple: wrong type annotation for proj"
+    _ -> throwSyntaxError "Jikka.Core.Parse.Happy.makeTuple: wrong type annotation for a tuple projection"
 
 replaceUnderscoresT :: MonadAlpha m => Type -> m Type
 replaceUnderscoresT = mapSubTypesM go where
@@ -512,10 +508,13 @@
     VarTy (TypeName "_") -> genType
     t -> return t
 
-replaceUnderscoresE :: MonadAlpha m => [(VarName, Type)] -> Expr -> m Expr
-replaceUnderscoresE env = mapExprM go env where
+replaceUnderscoresE :: (MonadAlpha m, MonadError Error m) => [(VarName, Type)] -> Expr -> m Expr
+replaceUnderscoresE env = mapSubExprM go env where
   go _ = \case
     Var (VarName "_") -> Var <$> genVarName'
+    e@(Proj' [] i (Var x)) -> case lookup x env of
+      Just (TupleTy ts) -> return $ Proj' ts i (Var x) -- Fix types of projections if it's easily possible.
+      _ -> return e -- Some cases are impossible. You need to use Jikka.Core.Convert.TypeInfer.
     e -> return e
 
 happyErrorExpList :: MonadError Error m => ([WithLoc L.Token], [String]) -> m a
@@ -555,11 +554,11 @@
 runExpr tokens = wrapError' "Jikka.Core.Parse.Happy.runExpr" $ do
     e <- liftEither $ runExpr_ tokens
     mapTypeExprM replaceUnderscoresT e
-    mapExprM replaceUnderscoresE [] e
+    mapSubExprM replaceUnderscoresE [] e
 
 runProgram :: (MonadAlpha m, MonadError Error m) => [WithLoc L.Token] -> m Program
 runProgram tokens = wrapError' "Jikka.Core.Parse.Happy.runProgram" $ do
     prog <- liftEither $ runProgram_ tokens
     prog <- mapTypeProgramM replaceUnderscoresT prog
-    mapExprProgramM replaceUnderscoresE prog
+    mapExprProgramM (mapSubExprM replaceUnderscoresE) prog
 }
diff --git a/src/Jikka/Core/Parse/Token.hs b/src/Jikka/Core/Parse/Token.hs
--- a/src/Jikka/Core/Parse/Token.hs
+++ b/src/Jikka/Core/Parse/Token.hs
@@ -21,10 +21,8 @@
   | CeilMod
   | Pow
   | -- boolean operators
-    Not
-  | And
+    And
   | Or
-  | Implies
   | -- bit operators
     BitNot
   | BitAnd
@@ -32,9 +30,6 @@
   | BitXor
   | BitLShift
   | BitRShift
-  | -- min max operators
-    Min
-  | Max
   | -- comparators
     DoubleEqual
   | NotEqual
diff --git a/src/Jikka/Main.hs b/src/Jikka/Main.hs
--- a/src/Jikka/Main.hs
+++ b/src/Jikka/Main.hs
@@ -30,6 +30,7 @@
   = Help
   | Verbose
   | Version
+  | Source String
   | Target String
   | BundleRuntimeHeaders Bool
   | EmbedOriginalCode Bool
@@ -37,6 +38,7 @@
 
 data Options = Options
   { verbose :: Bool,
+    source :: Target,
     target :: Maybe Target,
     bundleRuntimeHeaders :: Bool,
     embedOriginalCode :: Bool
@@ -47,6 +49,7 @@
 defaultOptions =
   Options
     { verbose = False,
+      source = PythonTarget,
       target = Nothing,
       bundleRuntimeHeaders = True,
       embedOriginalCode = True
@@ -60,6 +63,7 @@
   [ Option ['h', '?'] ["help"] (NoArg Help) "",
     Option ['v'] ["verbose"] (NoArg Verbose) "",
     Option [] ["version"] (NoArg Version) "",
+    Option [] ["source"] (ReqArg Source "SOURCE") "\"python\" or \"core\"",
     Option [] ["target"] (ReqArg Target "TARGET") "\"python\", \"rpython\", \"core\" or \"cxx\"",
     Option [] ["bundle-runtime-headers"] (NoArg (BundleRuntimeHeaders True)) "bundles C++ runtime headers",
     Option [] ["no-bundle-runtime-headers"] (NoArg (BundleRuntimeHeaders False)) "",
@@ -108,6 +112,9 @@
       Help -> throwCommandLineError "parseFlags is not called when --help is specified"
       Version -> throwCommandLineError "parseFlags is not called when --version is specified"
       Verbose -> go (opts {verbose = True}) flags
+      Source source -> do
+        source <- parseTarget source
+        go (opts {source = source}) flags
       Target target -> do
         target <- parseTarget target
         go (opts {target = Just target}) flags
@@ -119,19 +126,19 @@
   "convert" -> do
     input <- liftIO $ T.readFile path
     let target' = fromMaybe CPlusPlusTarget (target opts)
-    output <- liftEither $ Convert.run target' path input
+    output <- liftEither $ Convert.run (source opts) target' path input
     output <-
       if target' == CPlusPlusTarget && bundleRuntimeHeaders opts
         then BundleRuntime.run output
         else return output
     output <-
       return $
-        if embedOriginalCode opts
+        if target' == CPlusPlusTarget && embedOriginalCode opts
           then
             let headers = ["// This C++ code is transpiled using Jikka transpiler v" <> T.pack (showVersion version) <> " https://github.com/kmyk/Jikka", "// The original Python code:"]
              in T.unlines (headers ++ map ("//     " <>) (T.lines input)) <> output
           else output
     liftIO $ T.putStr output
-  "debug" -> Debug.run path
-  "execute" -> Execute.run (fromMaybe CoreTarget (target opts)) path
+  "debug" -> Debug.run path -- TODO: make this subcommand convenient
+  "execute" -> Execute.run (fromMaybe CoreTarget (target opts)) path -- TODO: use source
   _ -> throwCommandLineError $ "undefined subcommand: " ++ show subcmd
diff --git a/src/Jikka/Main/Subcommand/Convert.hs b/src/Jikka/Main/Subcommand/Convert.hs
--- a/src/Jikka/Main/Subcommand/Convert.hs
+++ b/src/Jikka/Main/Subcommand/Convert.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE LambdaCase #-}
 
 -- |
@@ -13,49 +14,68 @@
 import Data.Text (Text, pack)
 import qualified Jikka.CPlusPlus.Convert as FromCore
 import qualified Jikka.CPlusPlus.Format as FormatCPlusPlus
+import qualified Jikka.CPlusPlus.Language.Expr as CPlusPlus
 import Jikka.Common.Alpha
 import Jikka.Common.Error
 import qualified Jikka.Core.Convert as Convert
 import qualified Jikka.Core.Format as FormatCore
+import qualified Jikka.Core.Language.Expr as Core
+import qualified Jikka.Core.Parse as ParseCore
 import Jikka.Main.Target
 import qualified Jikka.Python.Convert.ToRestrictedPython as ToRestrictedPython
+import qualified Jikka.Python.Language.Expr as Python
 import qualified Jikka.Python.Parse as ParsePython
 import qualified Jikka.RestrictedPython.Convert as ToCore
 import qualified Jikka.RestrictedPython.Format as FormatRestrictedPython
+import qualified Jikka.RestrictedPython.Language.Expr as RestrictedPython
 
-runPython :: FilePath -> Text -> Either Error Text
-runPython path input = flip evalAlphaT 0 $ do
-  prog <- ParsePython.run path input
-  return . pack $ show prog -- TODO
+data Program
+  = PythonProgram Python.Program
+  | RestrictedPythonProgram RestrictedPython.Program
+  | CoreProgram Core.Program
+  | CPlusPlusProgram CPlusPlus.Program
+  deriving (Eq, Ord, Read, Show)
 
-runRestrictedPython :: FilePath -> Text -> Either Error Text
-runRestrictedPython path input = flip evalAlphaT 0 $ do
-  prog <- ParsePython.run path input
-  prog <- ToRestrictedPython.run prog
-  (prog, _) <- ToCore.run' prog
-  FormatRestrictedPython.run prog
+parseProgram :: (MonadAlpha m, MonadError Error m) => Target -> FilePath -> Text -> m Program
+parseProgram source path input = case source of
+  PythonTarget -> PythonProgram <$> ParsePython.run path input
+  RestrictedPythonTarget -> throwCommandLineError "cannot convert from restricted Python"
+  CoreTarget -> CoreProgram <$> ParseCore.run path input
+  CPlusPlusTarget -> throwCommandLineError "cannot convert from C++"
 
-runCore :: FilePath -> Text -> Either Error Text
-runCore path input = flip evalAlphaT 0 $ do
-  prog <- ParsePython.run path input
-  prog <- ToRestrictedPython.run prog
-  (prog, _) <- ToCore.run prog
-  prog <- Convert.run prog
-  FormatCore.run prog
+convertProgram :: (MonadAlpha m, MonadError Error m) => Program -> Target -> m Program
+convertProgram prog target = case (prog, target) of
+  (PythonProgram _, PythonTarget) -> return prog
+  (RestrictedPythonProgram _, RestrictedPythonTarget) -> return prog
+  (CoreProgram prog, CoreTarget) -> CoreProgram <$> Convert.run prog -- optimize
+  (CPlusPlusProgram _, CPlusPlusTarget) -> return prog
+  (RestrictedPythonProgram _, PythonTarget) -> throwCommandLineError "cannot convert from restricted Python to Python"
+  (CoreProgram _, PythonTarget) -> throwCommandLineError "cannot convert from core to Python"
+  (CoreProgram _, RestrictedPythonTarget) -> throwCommandLineError "cannot convert from core to restricted Python"
+  (PythonProgram prog, _) -> do
+    prog <- ToRestrictedPython.run prog
+    convertProgram (RestrictedPythonProgram prog) target
+  (RestrictedPythonProgram prog, CoreTarget) -> do
+    (prog, _) <- ToCore.run prog
+    CoreProgram <$> Convert.run prog
+  (RestrictedPythonProgram prog, CPlusPlusTarget) -> do
+    (prog, format) <- ToCore.run prog
+    prog <- Convert.run prog
+    CPlusPlusProgram <$> FromCore.run prog (Just format)
+  (CoreProgram prog, CPlusPlusTarget) -> do
+    prog <- Convert.run prog
+    CPlusPlusProgram <$> FromCore.run prog Nothing
+  (CPlusPlusProgram _, _) -> throwCommandLineError "cannot convert from C++"
 
-runCPlusPlus :: FilePath -> Text -> Either Error Text
-runCPlusPlus path input = flip evalAlphaT 0 $ do
-  prog <- ParsePython.run path input
-  prog <- ToRestrictedPython.run prog
-  (prog, format) <- ToCore.run prog
-  prog <- Convert.run prog
-  resetAlphaT 0 -- to make generated C++ code cleaner
-  prog <- FromCore.run prog format
-  FormatCPlusPlus.run prog
+formatProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Text
+formatProgram = \case
+  PythonProgram prog -> return . pack $ show prog -- TODO
+  RestrictedPythonProgram prog -> FormatRestrictedPython.run prog
+  CoreProgram prog -> FormatCore.run prog
+  CPlusPlusProgram prog -> FormatCPlusPlus.run prog
 
-run :: Target -> FilePath -> Text -> Either Error Text
-run = \case
-  PythonTarget -> runPython
-  RestrictedPythonTarget -> runRestrictedPython
-  CoreTarget -> runCore
-  CPlusPlusTarget -> runCPlusPlus
+run :: Target -> Target -> FilePath -> Text -> Either Error Text
+run source target path input = flip evalAlphaT 0 $ do
+  prog <- parseProgram source path input
+  prog <- convertProgram prog target
+  formatProgram prog
diff --git a/test/Jikka/CPlusPlus/Convert/MoveSemanticsSpec.hs b/test/Jikka/CPlusPlus/Convert/MoveSemanticsSpec.hs
--- a/test/Jikka/CPlusPlus/Convert/MoveSemanticsSpec.hs
+++ b/test/Jikka/CPlusPlus/Convert/MoveSemanticsSpec.hs
@@ -22,6 +22,34 @@
             [ FunDef
                 TyInt32
                 "func"
+                [(TyInt32, "a")]
+                [ Declare TyInt32 "b" (DeclareCopy (Var "a")),
+                  Assign (AssignExpr AddAssign (LeftVar "b") (Lit (LitInt32 10))),
+                  Declare TyInt32 "c" (DeclareCopy (Var "b")),
+                  Assign (AssignExpr AddAssign (LeftVar "b") (Lit (LitInt32 10))),
+                  Return (BinOp Add (Var "b") (Var "c"))
+                ]
+            ]
+    let expected =
+          Program
+            [ FunDef
+                TyInt32
+                "func"
+                [(TyInt32, "a")]
+                [ Assign (AssignExpr AddAssign (LeftVar "a") (Lit (LitInt32 10))),
+                  Declare TyInt32 "c" (DeclareCopy (Var "a")),
+                  Assign (AssignExpr AddAssign (LeftVar "a") (Lit (LitInt32 10))),
+                  Return (BinOp Add (Var "a") (Var "c"))
+                ]
+            ]
+    run' prog `shouldBe` Right expected
+
+  it "recognizes push_back" $ do
+    let prog =
+          Program
+            [ FunDef
+                TyInt32
+                "func"
                 [(TyVector TyInt32, "a")]
                 [ Declare (TyVector TyInt32) "b" (DeclareCopy (Var "a")),
                   ExprStatement (Call (Method "push_back") [Var "b", Lit (LitInt32 10)]),
@@ -42,7 +70,103 @@
                   Return (BinOp Add (Call MethodSize [Var "a"]) (Call MethodSize [Var "c"]))
                 ]
             ]
-    -- TODO: fix the bug https://github.com/kmyk/Jikka/issues/154 and enable this check
+    run' prog `shouldBe` Right expected
+
+  it "don't move if it is used in the next loop iteration" $ do
+    let prog =
+          Program
+            [ FunDef
+                TyInt32
+                "func"
+                [(TyInt32, "a")]
+                [ For
+                    TyInt32
+                    "i"
+                    (Lit (LitInt32 0))
+                    (BinOp LessThan (Var "i") (Lit (LitInt32 10)))
+                    (AssignIncr (LeftVar "i"))
+                    [ Declare TyInt32 "b" (DeclareCopy (Var "a")),
+                      Assign (AssignExpr AddAssign (LeftVar "b") (Lit (LitInt32 10)))
+                    ],
+                  Return (Var "a")
+                ]
+            ]
+    let expected = prog
+    run' prog `shouldBe` Right expected
+
+  it "allows to write back" $ do
+    let prog =
+          Program
+            [ FunDef
+                TyInt32
+                "func"
+                [(TyInt32, "a")]
+                [ Declare TyInt32 "b" (DeclareCopy (Var "a")),
+                  Assign (AssignExpr AddAssign (LeftVar "b") (Lit (LitInt32 10))),
+                  Assign (AssignExpr SimpleAssign (LeftVar "a") (Var "b")),
+                  Return (Var "a")
+                ]
+            ]
+    let expected =
+          Program
+            [ FunDef
+                TyInt32
+                "func"
+                [(TyInt32, "a")]
+                [ Assign (AssignExpr AddAssign (LeftVar "a") (Lit (LitInt32 10))),
+                  Return (Var "a")
+                ]
+            ]
+    run' prog `shouldBe` Right expected
+
+  it "recognizes set_at" $ do
+    let prog =
+          Program
+            [ FunDef
+                (TyVector TyInt32)
+                "func"
+                [(TyVector TyInt32, "a")]
+                [ Declare (TyVector TyInt32) "b" (DeclareCopy (Var "a")),
+                  Assign (AssignExpr AddAssign (LeftAt (LeftVar "b") (Lit (LitInt32 0))) (Call At [Var "a", Lit (LitInt32 1)])),
+                  Assign (AssignExpr SimpleAssign (LeftVar "a") (Var "b")),
+                  Return (Var "a")
+                ]
+            ]
+    let expected =
+          Program
+            [ FunDef
+                (TyVector TyInt32)
+                "func"
+                [(TyVector TyInt32, "a")]
+                [ Assign (AssignExpr AddAssign (LeftAt (LeftVar "a") (Lit (LitInt32 0))) (Call At [Var "a", Lit (LitInt32 1)])),
+                  Return (Var "a")
+                ]
+            ]
+    run' prog `shouldBe` Right expected
+
+  it "TODO: allows to write back and reads after it" $ do
+    let prog =
+          Program
+            [ FunDef
+                TyInt32
+                "func"
+                [(TyInt32, "a")]
+                [ Declare TyInt32 "b" (DeclareCopy (Var "a")),
+                  Assign (AssignExpr AddAssign (LeftVar "b") (Lit (LitInt32 10))),
+                  Assign (AssignExpr AddAssign (LeftVar "a") (Var "b")),
+                  Return (BinOp Add (Var "a") (Var "b"))
+                ]
+            ]
+    let expected =
+          Program
+            [ FunDef
+                TyInt32
+                "func"
+                [(TyInt32, "a")]
+                [ Assign (AssignExpr AddAssign (LeftVar "a") (Lit (LitInt32 10))),
+                  Return (BinOp Add (Var "a") (Var "a"))
+                ]
+            ]
+    -- TODO: fix this
     -- run' prog `shouldBe` Right expected
-    run' prog `shouldBe` run' prog -- supress warnings
-    expected `shouldBe` expected -- supress warnings
+    run' prog `shouldNotBe` Right expected
diff --git a/test/Jikka/Core/Convert/ConvexHullTrickSpec.hs b/test/Jikka/Core/Convert/ConvexHullTrickSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Jikka/Core/Convert/ConvexHullTrickSpec.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Jikka.Core.Convert.ConvexHullTrickSpec
+  ( spec,
+  )
+where
+
+import Jikka.Common.Alpha
+import Jikka.Common.Error
+import qualified Jikka.Core.Convert.ConstantFolding as ConstantFolding
+import Jikka.Core.Convert.ConvexHullTrick (run)
+import qualified Jikka.Core.Convert.TypeInfer as TypeInfer
+import Jikka.Core.Format (formatProgram)
+import Jikka.Core.Language.Expr
+import Jikka.Core.Parse (parseProgram)
+import Test.Hspec
+
+run' :: Program -> Either Error Program
+run' = flip evalAlphaT 0 . (ConstantFolding.run <=< run)
+
+parseProgram' :: [String] -> Program
+parseProgram' = fromSuccess . flip evalAlphaT 100 . (TypeInfer.run <=< parseProgram . unlines)
+
+spec :: Spec
+spec = describe "run" $ do
+  it "works on morau-style min" $ do
+    let prog =
+          parseProgram'
+            [ "let k: int = 1000",
+              "in let a: int list = range k",
+              "in let b: int list = range k",
+              "in let c: int list = range k",
+              "in let e: int = 1234",
+              "in let xs: int list = range k",
+              "in build (fun ys ->",
+              "    minimum (map (fun j -> a[j] * xs[len ys] + b[j] + c[len ys]) (range (len ys)))",
+              ") (snoc nil e) k"
+            ]
+    let step =
+          unlines
+            [ "fun ($4: convex_hull_trick * int list) ($0: int) ->",
+              "    let ys: int list = $4.1",
+              "    in let ys$6: int list = snoc ys (cht_getmin $4.0 xs[$0 + 1] + c[$0 + 1])",
+              "    in let $5: convex_hull_trick = cht_insert $4.0 a[$0 + 1] b[$0 + 1]",
+              "    in ($5, ys$6)"
+            ]
+    let base =
+          unlines
+            [ "let ys$2: int list = (snoc nil e)",
+              "in (foldl (fun ($1: convex_hull_trick) ($3: int) ->",
+              "    cht_insert $1 a[$3] b[$3]",
+              ") cht_init (range 1), ys$2)"
+            ]
+    let expected =
+          parseProgram'
+            [ "let k: int = 1000",
+              "in let a: int list = range k",
+              "in let b: int list = range k",
+              "in let c: int list = range k",
+              "in let e: int = 1234",
+              "in let xs: int list = range k",
+              "in (foldl (" ++ step ++ ") (" ++ base ++ ") (range k)).1",
+              ""
+            ]
+    (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
+  it "works on morau-style min-snoc" $ do
+    let prog =
+          parseProgram'
+            [ "let k: int = 1000",
+              "in let a: int list = range k",
+              "in let b: int list = range k",
+              "in let c: int list = range k",
+              "in let e: int list -> int = fun f -> len f + 1234",
+              "in let xs: int list = range k",
+              "in build (fun ys ->",
+              "    minimum (snoc (map (fun j -> a[j] * xs[len ys] + b[j] + c[len ys]) (range (len ys))) (e ys))",
+              ") nil k"
+            ]
+    let step =
+          unlines
+            [ "fun ($4: convex_hull_trick * int list) ($0: int) ->",
+              "    let ys: int list = $4.1",
+              "    in let ys$6: int list = snoc ys (min (e ys - c[$0 + 1]) (cht_getmin $4.0 xs[$0 + 1]) + c[$0 + 1])",
+              "    in let $5: convex_hull_trick = cht_insert $4.0 a[$0 + 1] b[$0 + 1]",
+              "    in ($5, ys$6)"
+            ]
+    let base =
+          unlines
+            [ "let ys$2: int list = snoc nil ((let ys: int list = nil in e ys - c[0]) + c[0])",
+              "in (foldl (fun ($1: convex_hull_trick) ($3: int) ->",
+              "    cht_insert $1 a[$3] b[$3]",
+              ") cht_init (range 1), ys$2)"
+            ]
+    let expected =
+          parseProgram'
+            [ "let k: int = 1000",
+              "in let a: int list = range k",
+              "in let b: int list = range k",
+              "in let c: int list = range k",
+              "in let e: int list -> int = fun f -> len f + 1234",
+              "in let xs: int list = range k",
+              "in (foldl (" ++ step ++ ") (" ++ base ++ ") (range (k - 1))).1",
+              ""
+            ]
+    (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
diff --git a/test/Jikka/Core/Convert/MatrixExponentiationSpec.hs b/test/Jikka/Core/Convert/MatrixExponentiationSpec.hs
--- a/test/Jikka/Core/Convert/MatrixExponentiationSpec.hs
+++ b/test/Jikka/Core/Convert/MatrixExponentiationSpec.hs
@@ -8,77 +8,45 @@
 import Jikka.Common.Alpha
 import Jikka.Common.Error
 import Jikka.Core.Convert.MatrixExponentiation (run)
-import Jikka.Core.Language.BuiltinPatterns
+import qualified Jikka.Core.Convert.TypeInfer as TypeInfer
+import Jikka.Core.Format (formatProgram)
 import Jikka.Core.Language.Expr
-import Jikka.Core.Language.Util
+import Jikka.Core.Parse (parseProgram)
 import Test.Hspec
 
 run' :: Program -> Either Error Program
 run' = flip evalAlphaT 0 . run
 
+parseProgram' :: [String] -> Program
+parseProgram' = fromSuccess . flip evalAlphaT 100 . (TypeInfer.run <=< parseProgram . unlines)
+
 spec :: Spec
 spec = describe "run" $ do
   it "works about matrices" $ do
-    let ts2 = [IntTy, IntTy]
-    let ts22 = [TupleTy ts2, TupleTy ts2]
-    let proj i = Proj' ts2 i (Var "xs")
-    let mkTuple ts = uncurryApp (Tuple' ts)
-    let letConst = Let "c" IntTy (LitInt' 10)
-    let k = LitInt' 100
-    let base = mkTuple ts2 [LitInt' 12, LitInt' 34]
     let prog =
-          ResultExpr
-            ( letConst
-                ( Iterate'
-                    (TupleTy ts2)
-                    k
-                    ( Lam
-                        "xs"
-                        (TupleTy ts2)
-                        (mkTuple ts2 [Plus' (proj 0) (Mult' (Var "c") (proj 1)), proj 0])
-                    )
-                    base
-                )
-            )
+          parseProgram'
+            [ "let c: int = 10",
+              "in let k: int = 1000",
+              "in iterate k (fun x -> (x.0 + c * x.1, x.0)) (12, 34)"
+            ]
     let expected =
-          ResultExpr
-            ( letConst
-                ( MatAp'
-                    2
-                    2
-                    ( MatPow'
-                        2
-                        (mkTuple ts22 [mkTuple ts2 [Lit1, Var "c"], mkTuple ts2 [Lit1, Lit0]])
-                        k
-                    )
-                    base
-                )
-            )
-    run' prog `shouldBe` Right expected
+          parseProgram'
+            [ "let c: int = 10",
+              "in let k: int = 1000",
+              "in matap@2@2 (matpow@2 ((1, c), (1, 0)) k) (12, 34)"
+            ]
+    (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
   it "works about integers" $ do
-    let letConst = Let "c" IntTy (LitInt' 10)
-    let k = LitInt' 100
-    let base = LitInt' 1234
     let prog =
-          ResultExpr
-            ( letConst
-                ( Iterate'
-                    IntTy
-                    k
-                    ( Lam
-                        "x"
-                        IntTy
-                        (Plus' (Mult' (Var "c") (Var "x")) (LitInt' 2))
-                    )
-                    base
-                )
-            )
+          parseProgram'
+            [ "let c: int = 10",
+              "in let k: int = 1000",
+              "in iterate k (fun x -> c * x + 2) 1234"
+            ]
     let expected =
-          ResultExpr
-            ( letConst
-                ( Plus'
-                    (Mult' (Pow' (Var "c") k) base)
-                    (Mult' (FloorDiv' (Minus' (Pow' (Var "c") k) (LitInt' 1)) (Minus' (Var "c") (LitInt' 1))) (LitInt' 2))
-                )
-            )
-    run' prog `shouldBe` Right expected
+          parseProgram'
+            [ "let c: int = 10",
+              "in let k: int = 1000",
+              "in c ** k * 1234 + (c ** k - 1) / (c - 1) * 2"
+            ]
+    (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
diff --git a/test/Jikka/Core/FormatSpec.hs b/test/Jikka/Core/FormatSpec.hs
--- a/test/Jikka/Core/FormatSpec.hs
+++ b/test/Jikka/Core/FormatSpec.hs
@@ -37,11 +37,10 @@
     let expected =
           unlines
             [ "let rec solve$0 (n$1: int): int =",
-              "    let xs$2: int list =",
-              "        map((fun (i$3: int) ->",
-              "            i$3 * i$3",
-              "        ), range(n$1))",
-              "    in sum(xs$2)",
+              "    let xs$2: int list = map (fun (i$3: int) ->",
+              "        i$3 * i$3",
+              "    ) (range n$1)",
+              "    in sum xs$2",
               "in",
               "solve$0"
             ]
diff --git a/test/Jikka/Core/Language/ArithmeticExprSpec.hs b/test/Jikka/Core/Language/ArithmeticExprSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Jikka/Core/Language/ArithmeticExprSpec.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Jikka.Core.Language.ArithmeticExprSpec
+  ( spec,
+  )
+where
+
+import qualified Data.Vector as V
+import Jikka.Core.Language.ArithmeticExpr
+import Jikka.Core.Language.BuiltinPatterns
+import Jikka.Core.Language.Expr
+import Test.Hspec
+
+spec :: Spec
+spec = do
+  describe "makeVectorFromArithmeticExpr" $ do
+    it "works" $ do
+      let xs = V.fromList ["x", "y"]
+      let e =
+            parseArithmeticExpr
+              (Plus' (Var "x") (Plus' (Mult' (LitInt' 3) (Var "y")) (Minus' (Var "x") (LitInt' 10))))
+      let f = V.fromList [parseArithmeticExpr (LitInt' 2), parseArithmeticExpr (LitInt' 3)]
+      let c = parseArithmeticExpr (LitInt' (-10))
+      makeVectorFromArithmeticExpr xs e `shouldBe` Just (f, c)
+  describe "normalizeArithmeticExpr" $ do
+    it "works" $ do
+      let e = Plus' (LitInt' 2) (Plus' (Var "a") (LitInt' (-2)))
+      let expected = Var "a"
+      (formatArithmeticExpr . parseArithmeticExpr) e `shouldBe` expected
diff --git a/test/Jikka/Core/Language/ArithmeticalExprSpec.hs b/test/Jikka/Core/Language/ArithmeticalExprSpec.hs
deleted file mode 100644
--- a/test/Jikka/Core/Language/ArithmeticalExprSpec.hs
+++ /dev/null
@@ -1,29 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module Jikka.Core.Language.ArithmeticalExprSpec
-  ( spec,
-  )
-where
-
-import qualified Data.Vector as V
-import Jikka.Core.Language.ArithmeticalExpr
-import Jikka.Core.Language.BuiltinPatterns
-import Jikka.Core.Language.Expr
-import Test.Hspec
-
-spec :: Spec
-spec = do
-  describe "makeVectorFromArithmeticalExpr" $ do
-    it "works" $ do
-      let xs = V.fromList ["x", "y"]
-      let e =
-            parseArithmeticalExpr
-              (Plus' (Var "x") (Plus' (Mult' (LitInt' 3) (Var "y")) (Minus' (Var "x") (LitInt' 10))))
-      let f = V.fromList [parseArithmeticalExpr (LitInt' 2), parseArithmeticalExpr (LitInt' 3)]
-      let c = parseArithmeticalExpr (LitInt' (-10))
-      makeVectorFromArithmeticalExpr xs e `shouldBe` Just (f, c)
-  describe "normalizeArithmeticalExpr" $ do
-    it "works" $ do
-      let e = Plus' (LitInt' 2) (Plus' (Var "a") (LitInt' (-2)))
-      let expected = Var "a"
-      (formatArithmeticalExpr . parseArithmeticalExpr) e `shouldBe` expected
diff --git a/test/Jikka/RestrictedPython/Convert/ToCoreSpec.hs b/test/Jikka/RestrictedPython/Convert/ToCoreSpec.hs
--- a/test/Jikka/RestrictedPython/Convert/ToCoreSpec.hs
+++ b/test/Jikka/RestrictedPython/Convert/ToCoreSpec.hs
@@ -7,6 +7,7 @@
 import qualified Jikka.Core.Format as Y (formatProgram)
 import qualified Jikka.Core.Language.BuiltinPatterns as Y
 import qualified Jikka.Core.Language.Expr as Y
+import qualified Jikka.Core.Parse as Y (parseProgram)
 import Jikka.RestrictedPython.Convert.ToCore (run)
 import qualified Jikka.RestrictedPython.Language.Expr as X
 import qualified Jikka.RestrictedPython.Language.WithoutLoc as X
@@ -15,6 +16,9 @@
 run' :: X.Program -> Either Error Y.Program
 run' = flip evalAlphaT 0 . run
 
+parseProgram :: [String] -> Y.Program
+parseProgram = fromSuccess . flip evalAlphaT 100 . Y.parseProgram . unlines
+
 spec :: Spec
 spec = describe "run" $ do
   it "works" $ do
@@ -66,37 +70,27 @@
               ]
           ]
     let expected =
-          unlines
+          parseProgram
             [ "let rec solve (n: int): int =",
-              "    let a: $0 =",
-              "        0",
-              "    in let b: $1 =",
-              "        1",
+              "    let a: $0 = 0",
+              "    in let b: $1 = 1",
               "    in let $4: $5 * $6 =",
-              "        foldl((fun ($4: $5 * $6) ($3: $2) ->",
-              "            let b: $5 =",
-              "                $4.0",
-              "            in let a: $6 =",
-              "                $4.1",
-              "            in let i: $7 =",
-              "                $3",
-              "            in let c: $8 =",
-              "                a + b",
-              "            in let a: $9 =",
-              "                b",
-              "            in let b: $10 =",
-              "                c",
+              "        foldl (fun ($4: $5 * $6) ($3: $2) ->",
+              "            let b: $5 = $4.0",
+              "            in let a: $6 = $4.1",
+              "            in let i: $7 = $3",
+              "            in let c: $8 = a + b",
+              "            in let a: $9 = b",
+              "            in let b: $10 = c",
               "            in (b, a)",
-              "        ), (b, a), range(n))",
-              "    in let b: $5 =",
-              "        $4.0",
-              "    in let a: $6 =",
-              "        $4.1",
+              "        ) (b, a) (range n)",
+              "    in let b: $5 = $4.0",
+              "    in let a: $6 = $4.1",
               "    in a",
               "in",
               "solve"
             ]
-    (Y.formatProgram <$> run' prog) `shouldBe` Right expected
+    (Y.formatProgram <$> run' prog) `shouldBe` Right (Y.formatProgram expected)
   it "converts if-statements correctly" $ do
     let prog =
           [ X.ToplevelFunctionDef
@@ -113,18 +107,14 @@
               ]
           ]
     let expected =
-          unlines
+          parseProgram
             [ "let rec solve : int =",
-              "    let $2: $1, =",
-              "        if true then let x: $3 =",
-              "            1",
-              "        in (x,) else let x: $5 =",
-              "            0",
-              "        in (x,)",
-              "    in let x: $1 =",
-              "        $2.0",
+              "    let $2: $1 one_tuple = if true",
+              "        then let x: $3 = 1 in (x,)",
+              "        else let x: $5 = 0 in (x,)",
+              "    in let x: $1 = $2.0",
               "    in x",
               "in",
               "solve"
             ]
-    (Y.formatProgram <$> run' prog) `shouldBe` Right expected
+    (Y.formatProgram <$> run' prog) `shouldBe` Right (Y.formatProgram expected)