packages feed

Jikka 5.4.0.0 → 5.5.0.0

raw patch · 59 files changed

+1291/−380 lines, 59 filesdep ~template-haskell

Dependency ranges changed: template-haskell

Files

CHANGELOG.md view
@@ -1,10 +1,26 @@ # Changelog for Jikka +## 2021-09-04: v5.5.0.0++Features:++- Now Jikka is available on Web: <https://kmyk.github.io/Jikka/playground/>+- Solve some formulae in the form of `∑ᵢ ∑ⱼ |aᵢ−aⱼ|` [#210](https://github.com/kmyk/Jikka/pull/210) by [@kmyk](https://github.com/kmyk)++Bug Fix:++- Fix a bug about `std::accumulate` ([#205](https://github.com/kmyk/Jikka/pull/205) by [@riantkb](https://github.com/riantkb)+ ## 2021-08-24: v5.4.0.0 -- More and more tests are added and some bugs are removed.+Features:+ - An online judge is published: <https://judge.kimiyuki.net/>   - This judge contains example problems which Jikka can/will be able to solve.++Bug Fix:++- More and more tests are added and some bugs are removed.  ## 2021-08-16: v5.3.0.0
Jikka.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           Jikka-version:        5.4.0.0+version:        5.5.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@@ -84,6 +84,7 @@       Jikka.Core.Convert.RemoveUnusedVars       Jikka.Core.Convert.SegmentTree       Jikka.Core.Convert.ShortCutFusion+      Jikka.Core.Convert.SortAbs       Jikka.Core.Convert.SpecializeFoldl       Jikka.Core.Convert.TrivialLetElimination       Jikka.Core.Convert.TypeInfer@@ -91,6 +92,7 @@       Jikka.Core.Evaluate       Jikka.Core.Format       Jikka.Core.Language.ArithmeticExpr+      Jikka.Core.Language.AssertedHint       Jikka.Core.Language.Beta       Jikka.Core.Language.BuiltinPatterns       Jikka.Core.Language.Expr@@ -98,6 +100,7 @@       Jikka.Core.Language.LambdaPatterns       Jikka.Core.Language.Lint       Jikka.Core.Language.ModuloExpr+      Jikka.Core.Language.NameCheck       Jikka.Core.Language.QuasiRules       Jikka.Core.Language.RewriteRules       Jikka.Core.Language.Runtime@@ -169,7 +172,7 @@     , deepseq >=1.4.4 && <1.5     , directory >=1.3.3 && <1.4     , mtl >=2.2.2 && <2.3-    , template-haskell >=2.16.0 && <2.17+    , template-haskell >=2.15.0 && <2.17     , text >=1.2.3 && <1.3     , transformers >=0.5.6 && <0.6     , vector >=0.12.3 && <0.13@@ -193,7 +196,7 @@     , deepseq >=1.4.4 && <1.5     , directory >=1.3.3 && <1.4     , mtl >=2.2.2 && <2.3-    , template-haskell >=2.16.0 && <2.17+    , template-haskell >=2.15.0 && <2.17     , text >=1.2.3 && <1.3     , transformers >=0.5.6 && <0.6     , vector >=0.12.3 && <0.13@@ -203,9 +206,10 @@   type: exitcode-stdio-1.0   main-is: doctests.hs   other-modules:+      Main       Paths_Jikka   hs-source-dirs:-      ./+      app   ghc-options: -W -threaded -rtsopts -with-rtsopts=-N -optP-Wno-nonportable-include-path   build-depends:       Jikka@@ -217,7 +221,7 @@     , directory >=1.3.3 && <1.4     , doctest     , mtl >=2.2.2 && <2.3-    , template-haskell >=2.16.0 && <2.17+    , template-haskell >=2.15.0 && <2.17     , text >=1.2.3 && <1.3     , transformers >=0.5.6 && <0.6     , vector >=0.12.3 && <0.13@@ -234,6 +238,7 @@       Jikka.Core.Convert.AlphaSpec       Jikka.Core.Convert.ANormalSpec       Jikka.Core.Convert.BetaSpec+      Jikka.Core.Convert.CloseMinSpec       Jikka.Core.Convert.CloseSumSpec       Jikka.Core.Convert.ConstantFoldingSpec       Jikka.Core.Convert.ConstantPropagationSpec@@ -247,6 +252,7 @@       Jikka.Core.Convert.RemoveUnusedVarsSpec       Jikka.Core.Convert.SegmentTreeSpec       Jikka.Core.Convert.ShortCutFusionSpec+      Jikka.Core.Convert.SortAbsSpec       Jikka.Core.Convert.SpecializeFoldlSpec       Jikka.Core.Convert.TrivialLetEliminationSpec       Jikka.Core.Convert.TypeInferSpec@@ -254,6 +260,7 @@       Jikka.Core.EvaluateSpec       Jikka.Core.FormatSpec       Jikka.Core.Language.ArithmeticExprSpec+      Jikka.Core.Language.AssertedHintSpec       Jikka.Core.Language.BetaSpec       Jikka.Core.ParseSpec       Jikka.CPlusPlus.Convert.FromCoreSpec@@ -296,7 +303,7 @@     , hspec     , mtl >=2.2.2 && <2.3     , ormolu-    , template-haskell >=2.16.0 && <2.17+    , template-haskell >=2.15.0 && <2.17     , text >=1.2.3 && <1.3     , transformers >=0.5.6 && <0.6     , vector >=0.12.3 && <0.13
README.md view
@@ -4,14 +4,18 @@  Jikka is an automated solver for problems of competitive programming. -In competitive programming, there are some problems which are solvable only with "repeating formula transformations", "pasting snippets of famous data structures", etc.-Jikka automatically solves such problems.-Jikka takes such problems as input in the form of a program of a very restricted subset of Python, optimizes the code to reduce the computational complexity, and outputs as an implementation in C++.+In competitive programming, there are some problems that can be solved just by _repeating formula transformations_ or by _pasting snippets of famous data structures_.+Jikka solves such problems automatically.+Jikka takes problems as input in the form of programs of a very restricted subset of Python, optimizes the codes to reduce their computational complexity, and converts them to implementations of C++ for output. / 競技プログラミングにおいて「ただ式変形をするだけで解ける」「ただデータ構造のライブラリを貼るだけで解ける」問題は実は少なくありません。-Jikka はそのような問題を自動で解きます。-そのような問題をとても制限された Python のサブセット言語のコードの形で入力として受け取り、計算量を落とすような最適化を行い、C++ の実装に変換して出力します。+Jikka はそのような問題を自動で解いてくれます。+Jikka は問題をとても制限された Python のサブセット言語のコードの形で入力として受け取り、計算量を落とすような最適化を行い、C++ の実装に変換して出力します。 +## Try on Web++Go <https://kmyk.github.io/Jikka/playground>.+ ## Usage  ```console@@ -59,6 +63,7 @@   - A list of optimizations which Jikka does / Jikka が行なってくれる最適化の一覧 - [examples/](https://github.com/kmyk/Jikka/blob/master/examples)   - [gallery](https://kmyk.github.io/Jikka/gallery)+  - [playground](https://kmyk.github.io/Jikka/playground) - [CHANGELOG.md](https://github.com/kmyk/Jikka/blob/master/CHANGELOG.md)  For developpers:
+ app/doctests.hs view
@@ -0,0 +1,14 @@+import Test.DocTest++-- | The modules generated by alex and happy confuse doctest, so we need to avoid some modules which depend on them.+-- TODO: Resolve this issue.+--+-- >   main = doctest ["-isrc", "src/Jikka/Main.hs"]+main :: IO ()+main =+  doctest+    [ "src/Jikka/Common/",+      "src/Jikka/Python/Convert/",+      "src/Jikka/Python/Language/",+      "src/Jikka/RestrictedPython/Language/"+    ]
− doctests.hs 
@@ -1,13 +0,0 @@-import Test.DocTest---- | The modules generated by alex and happy confuse doctest, so we need to avoid some modules which depend on them.--- TODO: Resolve this issue.------ >   main = doctest ["-isrc", "src/Jikka/Main.hs"]-main :: IO ()-main = doctest-    [ "src/Jikka/Common/"-    , "src/Jikka/Python/Convert/"-    , "src/Jikka/Python/Language/"-    , "src/Jikka/RestrictedPython/Language/"-    ]
src/Jikka/CPlusPlus/Convert/BundleRuntime.hs view
@@ -37,18 +37,16 @@ #ifdef JIKKA_EMBED_RUNTIME embeddedRuntimeFiles :: [(FilePath, T.Text)] embeddedRuntimeFiles = $(embedDir "runtime/include")-#endif -{-# ANN readRuntimeFile ("HLint: ignore Redundant return" :: String) #-}-readRuntimeFile :: (MonadIO m, MonadError Error m) => FilePath -> m T.Text-readRuntimeFile path = do-  return () -- Without this, Ormolu fails with "The GHC parser (in Haddock mode) failed: parse error on input `='"--#ifdef JIKKA_EMBED_RUNTIME+readRuntimeFile :: MonadError Error m => FilePath -> m T.Text+readRuntimeFile path =   case lookup ("runtime/include/" ++ path) embeddedRuntimeFiles of     Just file -> return file     Nothing -> throwInternalError $ "failed to open file. It may need recompile the binary?: " ++ path+ #else+readRuntimeFile :: (MonadIO m, MonadError Error m) => FilePath -> m T.Text+readRuntimeFile path = do   resolvedPath <- liftIO $ getDataFileName ("runtime/include/" ++ path)   file <- liftIO $ tryIOError (T.readFile resolvedPath)   case file of@@ -72,11 +70,11 @@ throwInternalErrorAt'' :: MonadError Error m => FilePath -> Integer -> String -> m a throwInternalErrorAt'' path lineno msg = wrapError' (path ++ " (line " ++ show lineno ++ ")") $ throwInternalError msg -runLine :: (MonadIO m, MonadError Error m, MonadState PreprocessorState m) => FilePath -> Integer -> T.Text -> m [T.Text]-runLine path lineno line+runLine :: (MonadError Error m, MonadState PreprocessorState m) => (FilePath -> m T.Text) -> FilePath -> Integer -> T.Text -> m [T.Text]+runLine readRuntimeFile path lineno line   | "#include \"" `T.isPrefixOf` line = case T.splitOn "\"" line of     ["#include ", path', ""] -> do-      lines <- runFile (T.unpack path')+      lines <- runFile readRuntimeFile (T.unpack path')       return (lines ++ [T.pack ("#line " ++ show (lineno + 1) ++ " \"" ++ path ++ "\"")])     _ -> throwInternalErrorAt'' path lineno "invalid #include \"...\""   | otherwise = do@@ -86,11 +84,11 @@       False : _ -> return []       [] -> throwInternalError "there are more #endif than #ifdef and #ifndef" -runLines :: (MonadIO m, MonadError Error m, MonadState PreprocessorState m) => FilePath -> Integer -> [T.Text] -> m [T.Text]-runLines path lineno lines = concat <$> zipWithM (runLine path) [lineno ..] lines+runLines :: (MonadError Error m, MonadState PreprocessorState m) => (FilePath -> m T.Text) -> FilePath -> Integer -> [T.Text] -> m [T.Text]+runLines readRuntimeFile path lineno lines = concat <$> zipWithM (runLine readRuntimeFile path) [lineno ..] lines -runFile :: (MonadIO m, MonadError Error m, MonadState PreprocessorState m) => FilePath -> m [T.Text]-runFile path = do+runFile :: (MonadError Error m, MonadState PreprocessorState m) => (FilePath -> m T.Text) -> FilePath -> m [T.Text]+runFile readRuntimeFile path = do   file <- readRuntimeFile path   let lines = T.lines file   let macro = map (\c -> if isAlphaNum c then toUpper c else '_') path@@ -107,7 +105,7 @@     then return []     else do       modify' (\s -> s {definedMacros = S.insert macro macros})-      (T.pack ("#line 3 \"" ++ path ++ "\"") :) <$> runLines path 3 (drop 2 (init lines))+      (T.pack ("#line 3 \"" ++ path ++ "\"") :) <$> runLines readRuntimeFile path 3 (drop 2 (init lines))  removeConsecutiveLineDirectives :: [T.Text] -> [T.Text] removeConsecutiveLineDirectives = \case@@ -116,7 +114,11 @@   [] -> []  -- | `run` bundles runtime headers to C++ code like <https://github.com/online-judge-tools/verification-helper `oj-bundle` command>.+#ifdef JIKKA_EMBED_RUNTIME+run :: MonadError Error m => T.Text -> m T.Text+#else run :: (MonadIO m, MonadError Error m) => T.Text -> m T.Text+#endif run prog = wrapError' "Jikka.CPlusPlus.Convert.BundleRuntime" $ do-  lines <- evalStateT (runLines "main.cpp" 1 (T.lines prog)) initialPreprocessorState+  lines <- evalStateT (runLines readRuntimeFile "main.cpp" 1 (T.lines prog)) initialPreprocessorState   return $ T.unlines (removeConsecutiveLineDirectives lines)
src/Jikka/CPlusPlus/Format.hs view
@@ -196,9 +196,7 @@ formatLiteral :: Literal -> Code formatLiteral = \case   LitInt32 n -> show n-  LitInt64 n-    | - (2 ^ 31) <= n && n < 2 ^ 31 -> show n-    | otherwise -> show n ++ "ll"+  LitInt64 n -> show n ++ "ll"   LitBool p -> if p then "true" else "false"   LitChar c -> show c   LitString s -> show s
src/Jikka/Common/FileEmbed.hs view
@@ -3,6 +3,7 @@ module Jikka.Common.FileEmbed where  import Control.Monad+import Data.Char import qualified Data.Text as T import qualified Data.Text.IO as T import Language.Haskell.TH@@ -30,4 +31,5 @@   paths <- runIO $ listDirectoryRecursive path   contents <- runIO $ mapM T.readFile paths :: Q [T.Text]   mapM_ addDependentFile paths-  [e|zip paths contents :: [(FilePath, T.Text)]|]+  let contents' = map (map ord . T.unpack) contents -- use [Int] instead of T.Text for scripts/erase_template_haskell.py+  [e|zip paths (map (T.pack . map chr) contents') :: [(FilePath, T.Text)]|]
src/Jikka/Common/IOFormat.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}  module Jikka.Common.IOFormat where @@ -127,17 +128,33 @@   At e i -> second (++ [i]) <$> unpackSubscriptedVar e   e -> throwInternalError $ "not a subscripted variable: " ++ formatFormatExpr e -makeReadValueIO :: (MonadError Error m, MonadIO m) => (value -> m Integer) -> (Integer -> value) -> (value -> m (V.Vector value)) -> (V.Vector value -> value) -> IOFormat -> m ([value], M.Map String value)+makeReadValueIO :: forall m value. (MonadError Error m, MonadIO m) => (value -> m Integer) -> (Integer -> value) -> (value -> m (V.Vector value)) -> (V.Vector value -> value) -> IOFormat -> m ([value], M.Map String value) makeReadValueIO toInt fromInt toList fromList format = wrapError' "Jikka.Common.IOFormat.makeReadValueIO" $ do-  env <- liftIO $ newIORef M.empty-  sizes <- liftIO $ newIORef M.empty-  let lookup x = do+  env <- liftIO $ newIORef M.empty :: m (IORef (M.Map String value))+  sizes <- liftIO $ newIORef M.empty :: m (IORef (M.Map String Integer))+  let lookup :: String -> m value+      lookup x = do         y <- M.lookup x <$> liftIO (readIORef env)         case y of           Nothing -> throwInternalError $ "undefined variable: " ++ x           Just y -> return y-  let go = \case+  let goEmpty :: FormatTree -> m ()+      goEmpty = \case         Exp e -> do+          (x, _) <- unpackSubscriptedVar e+          y <- M.lookup x <$> liftIO (readIORef env)+          case y of+            Just _ -> return ()+            Nothing -> do+              let y = fromList V.empty+              liftIO $ modifyIORef' env (M.insert x y)+        Newline -> return ()+        Seq formats -> mapM_ goEmpty formats+        Loop _ _ body -> do+          goEmpty body+  let go :: FormatTree -> m ()+      go = \case+        Exp e -> do           (x, indices) <- unpackSubscriptedVar e           word <- liftIO $ hGetWord stdin           n <- case readMaybe word of@@ -171,9 +188,11 @@             Len (Var xs) -> toInteger . V.length <$> (toList =<< lookup xs)             _ -> throwInternalError $ "invalid loop size in input tree: " ++ formatFormatExpr n           liftIO $ modifyIORef' sizes (M.insert i n)-          forM_ [0 .. n -1] $ \i' -> do-            liftIO $ modifyIORef' env (M.insert i (fromInt i'))-            go body+          if n == 0+            then goEmpty body+            else forM_ [0 .. n -1] $ \i' -> do+              liftIO $ modifyIORef' env (M.insert i (fromInt i'))+              go body   go (inputTree format)   values <- mapM lookup (inputVariables format)   env <- liftIO $ readIORef env
src/Jikka/Core/Convert.hs view
@@ -37,6 +37,7 @@ import qualified Jikka.Core.Convert.RemoveUnusedVars as RemoveUnusedVars import qualified Jikka.Core.Convert.SegmentTree as SegmentTree import qualified Jikka.Core.Convert.ShortCutFusion as ShortCutFusion+import qualified Jikka.Core.Convert.SortAbs as SortAbs import qualified Jikka.Core.Convert.SpecializeFoldl as SpecializeFoldl import qualified Jikka.Core.Convert.TrivialLetElimination as TrivialLetElimination import qualified Jikka.Core.Convert.TypeInfer as TypeInfer@@ -49,6 +50,7 @@   prog <- UnpackTuple.run prog   prog <- MatrixExponentiation.run prog   prog <- SpecializeFoldl.run prog+  prog <- SortAbs.run prog   prog <- MakeScanl.run prog   prog <- PropagateMod.run prog   prog <- ConstantPropagation.run prog
src/Jikka/Core/Convert/ANormal.hs view
@@ -16,7 +16,6 @@  import Jikka.Common.Alpha (MonadAlpha) import Jikka.Common.Error-import qualified Jikka.Core.Convert.Alpha as Alpha (runProgram) import Jikka.Core.Language.Expr import Jikka.Core.Language.Lint import Jikka.Core.Language.TypeCheck@@ -107,7 +106,9 @@ -- > in z run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.ANormal" $ do-  prog <- Alpha.runProgram prog+  precondition $ do+    lint prog   prog <- runProgram prog-  ensureWellTyped prog+  postcondition $ do+    lint prog   return prog
src/Jikka/Core/Convert/Alpha.hs view
@@ -10,43 +10,66 @@ -- Maintainer  : kimiyuki95@gmail.com -- Stability   : experimental -- Portability : portable-module Jikka.Core.Convert.Alpha where+module Jikka.Core.Convert.Alpha+  ( run,+    runProgram,+    runToplevelExpr,+    runExpr,+  )+where +import Control.Monad.State.Strict import Jikka.Common.Alpha import Jikka.Common.Error import Jikka.Core.Language.Expr+import Jikka.Core.Language.Lint -rename :: MonadAlpha m => VarName -> m VarName+type UsedVars = [VarName]++type RenameMapping = [(VarName, VarName)]++rename :: (MonadState UsedVars m, MonadAlpha m) => VarName -> m VarName rename x = do-  let base = takeWhile (/= '$') (unVarName x)-  i <- nextCounter-  return $ VarName (base ++ "$" ++ show i)+  used <- get+  y <-+    if x `notElem` used+      then return x+      else do+        let base = takeWhile (/= '$') (unVarName x)+        i <- nextCounter+        return $ VarName (base ++ "$" ++ show i)+  put $ y : used+  return y -runExpr :: (MonadAlpha m, MonadError Error m) => [(VarName, VarName)] -> Expr -> m Expr-runExpr env = \case+runExpr' :: (MonadState UsedVars m, MonadAlpha m, MonadError Error m) => RenameMapping -> Expr -> m Expr+runExpr' env = \case   Var x -> case lookup x env of     Nothing -> throwInternalError $ "undefined variable: " ++ unVarName x     Just y -> return $ Var y   Lit lit -> return $ Lit lit-  App f e -> App <$> runExpr env f <*> runExpr env e+  App f e -> App <$> runExpr' env f <*> runExpr' env e   Lam x t body -> do     y <- rename x-    body <- runExpr ((x, y) : env) body+    body <- runExpr' ((x, y) : env) body     return $ Lam y t body   Let x t e1 e2 -> do-    e1 <- runExpr env e1+    e1 <- runExpr' env e1     y <- rename x-    e2 <- runExpr ((x, y) : env) e2+    e2 <- runExpr' ((x, y) : env) e2     return $ Let y t e1 e2-  Assert e1 e2 -> Assert <$> runExpr env e1 <*> runExpr env e2+  Assert e1 e2 -> Assert <$> runExpr' env e1 <*> runExpr' env e2 -runToplevelExpr :: (MonadAlpha m, MonadError Error m) => [(VarName, VarName)] -> ToplevelExpr -> m ToplevelExpr-runToplevelExpr env = \case-  ResultExpr e -> ResultExpr <$> runExpr env e+runExpr :: (MonadAlpha m, MonadError Error m) => [(VarName, Type)] -> Expr -> m Expr+runExpr env e = wrapError' "Jikka.Core.Convert.Alpha.runExpr" $ do+  evalStateT (runExpr' (map (\(x, _) -> (x, x)) env) e) (map fst env)++runToplevelExpr' :: (MonadState UsedVars m, MonadAlpha m, MonadError Error m) => RenameMapping -> ToplevelExpr -> m ToplevelExpr+runToplevelExpr' env = \case+  ResultExpr e -> ResultExpr <$> runExpr' env e   ToplevelLet x t e cont -> do     y <- rename x-    e <- runExpr env e-    cont <- runToplevelExpr ((x, y) : env) cont+    e <- runExpr' env e+    cont <- runToplevelExpr' ((x, y) : env) cont     return $ ToplevelLet y t e cont   ToplevelLetRec f args ret body cont -> do     g <- rename f@@ -55,13 +78,21 @@       return (x, y, t)     let args1 = map (\(x, y, _) -> (x, y)) args     let args2 = map (\(_, y, t) -> (y, t)) args-    body <- runExpr (args1 ++ (f, g) : env) body-    cont <- runToplevelExpr ((f, g) : env) cont+    body <- runExpr' (args1 ++ (f, g) : env) body+    cont <- runToplevelExpr' ((f, g) : env) cont     return $ ToplevelLetRec g args2 ret body cont-  ToplevelAssert e1 e2 -> ToplevelAssert <$> runExpr env e1 <*> runToplevelExpr env e2+  ToplevelAssert e1 e2 -> ToplevelAssert <$> runExpr' env e1 <*> runToplevelExpr' env e2 +runToplevelExpr :: (MonadAlpha m, MonadError Error m) => [(VarName, Type)] -> ToplevelExpr -> m ToplevelExpr+runToplevelExpr env e = wrapError' "Jikka.Core.Convert.Alpha.runToplevelExpr" $ do+  evalStateT (runToplevelExpr' (map (\(x, _) -> (x, x)) env) e) (map fst env)+ runProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Program-runProgram = runToplevelExpr []+runProgram prog = wrapError' "Jikka.Core.Convert.Alpha.runProgram" $ do+  prog <- evalStateT (runToplevelExpr' [] prog) []+  postcondition $ do+    ensureAlphaConverted prog+  return prog  -- | `run` renames variables in exprs to avoid name conflictions, even if the scopes of two variables are distinct. --@@ -81,5 +112,4 @@ -- > in x2 = x0 + y1 -- > x2 + y1 run :: (MonadAlpha m, MonadError Error m) => Program -> m Program-run prog = wrapError' "Jikka.Core.Convert.Alpha" $ do-  runToplevelExpr [] prog+run = runProgram
src/Jikka/Core/Convert/ArithmeticExpr.hs view
@@ -10,6 +10,7 @@ -- Portability : portable module Jikka.Core.Convert.ArithmeticExpr   ( run,+    runExpr,   ) where @@ -20,15 +21,18 @@ import Jikka.Core.Language.TypeCheck import Jikka.Core.Language.Util -runExpr :: MonadError Error m => [(VarName, Type)] -> Expr -> m Expr-runExpr env e = do+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 +runExpr :: MonadError Error m => [(VarName, Type)] -> Expr -> m Expr+runExpr = mapSubExprM runExpr'+ runProgram :: MonadError Error m => Program -> m Program-runProgram = mapExprProgramM (mapSubExprM runExpr) -- Doesn't use RewriteRules because the rewriting may not terminate.+runProgram = mapExprProgramM (mapSubExprM runExpr') -- Doesn't use RewriteRules because the rewriting may not terminate.  -- | `run` sorts arithmetical exprs. --@@ -44,8 +48,8 @@ run :: MonadError Error m => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.ArithmeticExpr" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/Beta.hs view
@@ -19,7 +19,6 @@  import Jikka.Common.Alpha import Jikka.Common.Error-import qualified Jikka.Core.Convert.Alpha as Alpha import Jikka.Core.Language.Beta import Jikka.Core.Language.Expr import Jikka.Core.Language.Lint@@ -47,9 +46,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.Beta" $ do   precondition $ do-    ensureWellTyped prog-  prog <- Alpha.run prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/BubbleLet.hs view
@@ -55,8 +55,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.BubbleLet" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/CloseAll.hs view
@@ -28,7 +28,7 @@ import Jikka.Core.Language.QuasiRules import Jikka.Core.Language.RewriteRules -reduceAll :: MonadAlpha m => RewriteRule m+reduceAll :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceAll =   mconcat     [ -- list build functions@@ -42,7 +42,7 @@       [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+reduceAny :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceAny =   mconcat     [ -- list build functions@@ -57,7 +57,7 @@       [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+rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m rule =   mconcat     [ reduceAll,@@ -113,8 +113,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.CloseAll" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/CloseMin.hs view
@@ -25,7 +25,7 @@  import Jikka.Common.Alpha import Jikka.Common.Error-import qualified Jikka.Core.Convert.Alpha as Alpha+import Jikka.Core.Language.AssertedHint import Jikka.Core.Language.BuiltinPatterns import Jikka.Core.Language.Expr import Jikka.Core.Language.FreeVars@@ -34,10 +34,14 @@ import Jikka.Core.Language.QuasiRules import Jikka.Core.Language.RewriteRules -reduceMin :: MonadAlpha m => RewriteRule m+reduceMin :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceMin =   mconcat-    [ -- list build functions+    [ -- reduce minimum-cons if non-nil+      pureRewriteRule "minimum/cons" $ \env -> \case+        Min1' t (Cons' _ x xs) | nullWithHints (assertedHints env) xs == Just False -> Just $ Min2' t x (Min1' t xs)+        _ -> Nothing,+      -- list build functions       [r| "minimum/nil" minimum nil = bottom<"no minimum in empty list"> |],       [r| "minimum/cons/cons" forall x y zs. minimum (cons x (cons y zs)) = min x (minimum (cons y zs)) |],       [r| "minimum/range" forall n. minimum (range n) = 0 |],@@ -82,10 +86,14 @@         _ -> return Nothing     ] -reduceMax :: MonadAlpha m => RewriteRule m+reduceMax :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceMax =   mconcat-    [ -- list build functions+    [ -- reduce maximum-cons if non-nil+      pureRewriteRule "maximum/cons" $ \env -> \case+        Max1' t (Cons' _ x xs) | nullWithHints (assertedHints env) xs == Just False -> Just $ Max2' t x (Max1' t xs)+        _ -> Nothing,+      -- list build functions       [r| "maximum/nil" maximum nil = bottom<"no maximum in empty list"> |],       [r| "maximum/cons/cons" forall x y zs. maximum (cons x (cons y zs)) = max x (maximum (cons y zs)) |],       [r| "maximum/range" forall n. maximum (range n) = n - 1 |],@@ -131,7 +139,7 @@     ]  -- | TODO: implement this-reduceArgMin :: Monad m => RewriteRule m+reduceArgMin :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceArgMin = simpleRewriteRule "reduceArgMin" $ \case   -- list map functions   ArgMin' t (Reversed' _ xs) -> Just $ Minus' (Minus' (Len' t xs) (ArgMin' t xs)) Lit1@@ -141,7 +149,7 @@   _ -> Nothing  -- | TODO: implement this-reduceArgMax :: Monad m => RewriteRule m+reduceArgMax :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceArgMax = simpleRewriteRule "reduceArgMax" $ \case   -- list map functions   ArgMax' t (Reversed' _ xs) -> Just $ Minus' (Minus' (Len' t xs) (ArgMax' t xs)) Lit1@@ -150,7 +158,7 @@   ArgMax' _ (Map' t1 t2 (Lam x t (Plus' e1 e2)) xs) | x `isUnusedVar` e2 -> Just $ ArgMax' t2 (Map' t1 t2 (Lam x t e1) xs)   _ -> Nothing -rule :: MonadAlpha m => RewriteRule m+rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m rule =   mconcat     [ reduceMin,@@ -209,9 +217,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.CloseMin" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog-  prog <- Alpha.run prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/CloseSum.hs view
@@ -39,7 +39,7 @@ import Jikka.Core.Language.QuasiRules import Jikka.Core.Language.RewriteRules -reduceSum :: MonadAlpha m => RewriteRule m+reduceSum :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceSum =   mconcat     [ -- reduce list build functions@@ -87,7 +87,7 @@  -- | -- * This assumes that `ModFloor` is already propagated.-reduceModSum :: MonadAlpha m => RewriteRule m+reduceModSum :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceModSum =   mconcat     [ -- the corner case@@ -138,7 +138,7 @@     _ -> Nothing   _ -> Nothing -rule :: MonadAlpha m => RewriteRule m+rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m rule =   mconcat     [ reduceSum,@@ -204,8 +204,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.CloseSum" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/ConstantFolding.hs view
@@ -36,6 +36,7 @@  import Data.Bits import Data.Either+import Jikka.Common.Alpha import Jikka.Common.Error import Jikka.Core.Language.BuiltinPatterns import Jikka.Core.Language.Expr@@ -64,7 +65,7 @@ -- * `Abs` \(: \int \to \int\) -- * `Gcd` \(: \int \to \int \to \int\) -- * `Lcm` \(: \int \to \int \to \int\)-reduceConstArithmeticExpr :: Monad m => RewriteRule m+reduceConstArithmeticExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceConstArithmeticExpr =   let return' = Just . LitInt'    in simpleRewriteRule "reduceConstArithmeticExpr" $ \case@@ -111,7 +112,7 @@ -- -- * `Min2` \(: \forall \alpha. \alpha \to \alpha \to \alpha\) (specialized to \(\alpha = \lbrace \bool, \int \rbrace\)) -- * `Max2` \(: \forall \alpha. \alpha \to \alpha \to \alpha\) (specialized to \(\alpha = \lbrace \bool, \int \rbrace\))-reduceConstMaxExpr :: Monad m => RewriteRule m+reduceConstMaxExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceConstMaxExpr = simpleRewriteRule "reduceConstMaxExpr" $ \case   Min2' _ (LitInt' a) (LitInt' b) -> Just . LitInt' $ min a b   Min2' _ (LitBool' a) (LitBool' b) -> Just . LitBool' $ min a b@@ -127,7 +128,7 @@ -- * `And` \(: \bool \to \bool \to \bool\) -- * `Or` \(: \bool \to \bool \to \bool\) -- * `Implies` \(: \bool \to \bool \to \bool\)-reduceIdempotentBooleanExpr :: Monad m => RewriteRule m+reduceIdempotentBooleanExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceIdempotentBooleanExpr =   mconcat     [ [r| "join/and" forall x. x && x = x|],@@ -145,7 +146,7 @@ -- * `And` \(: \bool \to \bool \to \bool\) -- * `Or` \(: \bool \to \bool \to \bool\) -- * `Implies` \(: \bool \to \bool \to \bool\)-reduceUnitBooleanExpr :: Monad m => RewriteRule m+reduceUnitBooleanExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceUnitBooleanExpr =   mconcat     [ [r| "not/true" not true = false|],@@ -170,7 +171,7 @@ -- === Boolean functions -- -- * `If` \(: \forall \alpha. \bool \to \alpha \to \alpha \to \alpha\)-reduceConstBooleanExpr :: Monad m => RewriteRule m+reduceConstBooleanExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceConstBooleanExpr =   mconcat     [ [r| "if/true" forall e1 e2. if true then e1 else e2 = e1|],@@ -188,7 +189,7 @@ -- * `BitXor` \(: \int \to \int \to \int\) -- * `BitLeftShift` \(: \int \to \int \to \int\) -- * `BitRightShift` \(: \int \to \int \to \int\)-reduceUnitBitExpr :: Monad m => RewriteRule m+reduceUnitBitExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceUnitBitExpr =   mconcat     [ [r| "bitand/0" forall x. 0 & x = 0 |],@@ -220,7 +221,7 @@ -- * `BitXor` \(: \int \to \int \to \int\) -- * `BitLeftShift` \(: \int \to \int \to \int\) -- * `BitRightShift` \(: \int \to \int \to \int\)-reduceConstBitExpr :: Monad m => RewriteRule m+reduceConstBitExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceConstBitExpr =   let return' = Just . LitInt'    in simpleRewriteRule "reduceConstBitExpr" $ \case@@ -243,7 +244,7 @@ -- * `GreaterEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\)) -- * `Equal` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\)) -- * `NotEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))-reduceConstIntComparison :: Monad m => RewriteRule m+reduceConstIntComparison :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceConstIntComparison =   simpleRewriteRule "comparison/const/int" $     (LitBool' <$>) . \case@@ -266,7 +267,7 @@ -- * `GreaterEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\)) -- * `Equal` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\)) -- * `NotEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))-reduceUnitBooleanComparison :: Monad m => RewriteRule m+reduceUnitBooleanComparison :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceUnitBooleanComparison =   mconcat     [ -- TODO: implement lessthan and lessequal@@ -281,7 +282,7 @@       [r| "notequal/false'" forall x. x /= false = x |]     ] -rule :: MonadError Error m => RewriteRule m+rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m rule =   mconcat     [ reduceConstArithmeticExpr,@@ -295,7 +296,7 @@       reduceUnitBooleanComparison     ] -runProgram :: MonadError Error m => Program -> m Program+runProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Program runProgram = applyRewriteRuleProgram' rule  -- | `run` folds constants in given programs.@@ -306,11 +307,11 @@ -- to the follwoing: -- -- > 3 x + 3-run :: MonadError Error m => Program -> m Program+run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.ConstantFolding" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/ConstantPropagation.hs view
@@ -70,8 +70,8 @@ run :: MonadError Error m => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.ConstantPropagation" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- return $ run' prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/ConvexHullTrick.hs view
@@ -28,6 +28,7 @@ import Control.Monad.Trans.Maybe import Jikka.Common.Alpha import Jikka.Common.Error+import qualified Jikka.Core.Convert.Alpha as Alpha import Jikka.Core.Language.ArithmeticExpr import Jikka.Core.Language.Beta import Jikka.Core.Language.BuiltinPatterns@@ -161,7 +162,7 @@   _ -> Nothing  rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m-rule = makeRewriteRule "Jikka.Core.Convert.ConvexHullTrick" $ \_ -> \case+rule = makeRewriteRule "Jikka.Core.Convert.ConvexHullTrick" $ \env -> \case   -- build (fun f -> step(f)) base n   Build' IntTy (Lam f _ step) base n -> runMaybeT $ do     let ts = [ConvexHullTrickTy, ListTy IntTy]@@ -217,7 +218,8 @@               Let y ConvexHullTrickTy (ConvexHullTrickInsert' (Proj' ts 0 (Var x)) a b) $                 uncurryApp (Tuple' ts) [Var y, Var f']     -- proj 1 (foldl step' base' (range (n - 1)))-    return $ Proj' ts 1 (Foldl' IntTy (TupleTy ts) step' base' (Range1' n))+    let e = Proj' ts 1 (Foldl' IntTy (TupleTy ts) step' base' (Range1' n))+    lift $ Alpha.runExpr (typeEnv env) e   _ -> return Nothing  runProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Program@@ -230,8 +232,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.ConvexHullTrick" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/CumulativeSum.hs view
@@ -20,7 +20,6 @@ import Data.Maybe import Jikka.Common.Alpha import Jikka.Common.Error-import qualified Jikka.Core.Convert.Alpha as Alpha import Jikka.Core.Language.ArithmeticExpr import Jikka.Core.Language.BuiltinPatterns import Jikka.Core.Language.Expr@@ -86,9 +85,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.CumulativeSum" $ do   precondition $ do-    ensureWellTyped prog-  prog <- Alpha.run prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/EqualitySolving.hs view
@@ -33,6 +33,7 @@   ) where +import Jikka.Common.Alpha import Jikka.Common.Error import Jikka.Core.Language.BuiltinPatterns import Jikka.Core.Language.Expr@@ -42,7 +43,7 @@ import Jikka.Core.Language.Util  -- | `moveLiteralToRight` moves literals to lhs of `(==)` or `(/=)`, using symmetricity.-moveLiteralToRight :: Monad m => RewriteRule m+moveLiteralToRight :: (MonadAlpha m, MonadError Error m) => RewriteRule m moveLiteralToRight =   mconcat     [ simpleRewriteRule "equal/symmetricity/literal" $ \case@@ -54,7 +55,7 @@     ]  -- | `convertGreaterToLess` erases `(>)` and `(>=)`.-convertGreaterToLess :: Monad m => RewriteRule m+convertGreaterToLess :: (MonadAlpha m, MonadError Error m) => RewriteRule m convertGreaterToLess =   mconcat     [ [r| "greaterthan->lessthan" forall x y. x > y = y < x |],@@ -62,7 +63,7 @@     ]  -- | `reduceReflexivity` uses reflexivity.-reduceReflexivity :: Monad m => RewriteRule m+reduceReflexivity :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceReflexivity =   mconcat     [ [r| "lessthan/reflexivity" forall x. x == x = false |],@@ -72,7 +73,7 @@     ]  -- | `makeRightZero` makes RHS of integer equality/inequality zero with subtracting RHS from both sides.-makeRightZero :: Monad m => RewriteRule m+makeRightZero :: (MonadAlpha m, MonadError Error m) => RewriteRule m makeRightZero =   mconcat     [ simpleRewriteRule "lessthan/right-zero" $ \case@@ -90,7 +91,7 @@     ]  -- | `reduceIntInjective` removes injective functions from equalities of integers.-reduceIntInjective :: Monad m => RewriteRule m+reduceIntInjective :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceIntInjective =   mconcat     [ [r| "equal/negate" forall x y k. - x == 0 = x == 0  |],@@ -98,7 +99,7 @@       [r| "equal/fact'" forall x y. - fact x + fact y == 0 = x == y  |]     ] -reduceNot :: Monad m => RewriteRule m+reduceNot :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceNot =   mconcat     [ [r| "equal/not" forall x y. not x == y = x /= y |],@@ -107,7 +108,7 @@       [r| "notequal/not'" forall x y. x /= not y = x == y |]     ] -reduceListCtor :: Monad m => RewriteRule m+reduceListCtor :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceListCtor =   mconcat     [ [r| "equal/nil/nil" forall x xs. nil == nil = true |],@@ -116,13 +117,13 @@       [r| "equal/cons/cons" forall x xs y ys. cons x xs == cons y ys = x == y && xs == ys |]     ] -reduceListInjective :: Monad m => RewriteRule m+reduceListInjective :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceListInjective =   mconcat     [ [r| "equal/range/range" forall n1 n2. range n1 == range n2 = n1 == n2 |]     ] -rule :: Monad m => RewriteRule m+rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m rule =   mconcat     [ moveLiteralToRight,@@ -135,14 +136,14 @@       reduceListInjective     ] -runProgram :: MonadError Error m => Program -> m Program+runProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Program runProgram = applyRewriteRuleProgram' rule -run :: MonadError Error m => Program -> m Program+run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.EqualitySolving" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/Eta.hs view
@@ -76,8 +76,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.Eta" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/KubaruToMorau.hs view
@@ -107,8 +107,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.KubaruToMorau" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/MakeScanl.hs view
@@ -275,8 +275,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.MakeScanl" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/MatrixExponentiation.hs view
@@ -96,7 +96,7 @@   Iterate' (TupleTy ts) k (Lam x _ step) base | isVectorTy' ts -> do     let n = genericLength ts     let go n step base = MatAp' n n (MatPow' n step k) base-    step <- toMatrix env x n step+    step <- toMatrix (typeEnv env) x n step     case step of       Nothing -> return Nothing       Just (a, Nothing) -> return . Just $ go n (fromMatrix a) base@@ -134,8 +134,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.MatrixExponentiation" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/PropagateMod.hs view
@@ -135,10 +135,10 @@         e@(ModMult' _ _ _) -> return $ go0 e         e@(ModInv' _ _) -> return $ go0 e         e@(ModPow' _ _ _) -> return $ go0 e-        ModMatAp' h w e1 e2 m | not (e1 `isModulo'` m) || not (e2 `isModulo'` m) -> go2 m (ModMatAp' h w) (putMatFloorMod env, e1) (putVecFloorMod env, e2)-        ModMatAdd' h w e1 e2 m | not (e1 `isModulo'` m) || not (e2 `isModulo'` m) -> go2 m (ModMatAdd' h w) (putMatFloorMod env, e1) (putMatFloorMod env, e2)-        ModMatMul' h n w e1 e2 m | not (e1 `isModulo'` m) || not (e2 `isModulo'` m) -> go2 m (ModMatMul' h n w) (putMatFloorMod env, e1) (putMatFloorMod env, e2)-        ModMatPow' n e1 e2 m | not (e1 `isModulo'` m) -> go2 m (ModMatPow' n) (putMatFloorMod env, e1) (\_ e -> return e, e2)+        ModMatAp' h w e1 e2 m | not (e1 `isModulo'` m) || not (e2 `isModulo'` m) -> go2 m (ModMatAp' h w) (putMatFloorMod (typeEnv env), e1) (putVecFloorMod (typeEnv env), e2)+        ModMatAdd' h w e1 e2 m | not (e1 `isModulo'` m) || not (e2 `isModulo'` m) -> go2 m (ModMatAdd' h w) (putMatFloorMod (typeEnv env), e1) (putMatFloorMod (typeEnv env), e2)+        ModMatMul' h n w e1 e2 m | not (e1 `isModulo'` m) || not (e2 `isModulo'` m) -> go2 m (ModMatMul' h n w) (putMatFloorMod (typeEnv env), e1) (putMatFloorMod (typeEnv env), e2)+        ModMatPow' n e1 e2 m | not (e1 `isModulo'` m) -> go2 m (ModMatPow' n) (putMatFloorMod (typeEnv env), e1) (\_ e -> return e, e2)         ModSum' e m | not (e `isModulo'` m) -> go1 m ModSum' (putMapFloorMod, e)         ModProduct' e m | not (e `isModulo'` m) -> go1 m ModProduct' (putMapFloorMod, e)         FloorMod' e m ->@@ -169,8 +169,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.PropagateMod" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/RemoveUnusedVars.hs view
@@ -62,8 +62,8 @@ run :: MonadError Error m => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.RemoveUnusedVars" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- return $ run' prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/SegmentTree.hs view
@@ -177,9 +177,9 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.SegmentTree" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   prog <- Alpha.run prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/ShortCutFusion.hs view
@@ -47,14 +47,14 @@ -- * `Range2` is removed. -- * `Range3` is removed. -- * `Nil` and `Cons` are kept as is.-reduceBuild :: MonadAlpha m => RewriteRule m+reduceBuild :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceBuild =   mconcat     [ [r| "range2" forall l r. range2 l r = map (fun i -> l + i) (range (r - l)) |],       [r| "range3" forall l r step. range3 l r step = map (fun i -> l + i * step) (range ((r - l) /^ step)) |]     ] -reduceMapBuild :: MonadAlpha m => RewriteRule m+reduceMapBuild :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceMapBuild =   mconcat     [ [r| "sorted/nil" sorted nil = nil |],@@ -66,7 +66,7 @@       [r| "map/cons" forall f x xs. map f (cons x xs) = cons (f x) (map f xs) |]     ] -reduceMap :: Monad m => RewriteRule m+reduceMap :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceMap =   mconcat     [ [r| "map/id" forall xs. map (fun x -> x) xs = xs |],@@ -79,7 +79,7 @@ --   * `Sort` and `Reversed` (functions to reorder) are lastly applied to lists --   * `Map` (functions to modify lists) --   * `Filter` (funcitons to reduce lengths) is firstly applied to lists-reduceMapMap :: MonadAlpha m => RewriteRule m+reduceMapMap :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceMapMap =   mconcat     [ [r| "map/map" forall f g xs. map g (map f xs) = map (fun x -> g (f x)) xs |],@@ -92,7 +92,7 @@       [r| "sorted/sorted" forall xs. sorted (sorted xs) = sorted xs |]     ] -reduceFoldMap :: MonadAlpha m => RewriteRule m+reduceFoldMap :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceFoldMap =   mconcat     [ -- reduce `Reversed`@@ -117,7 +117,7 @@   Foldl' t1 t2 (Lam2 x2 _ x1 _ body) init xs | x1 `isUnusedVar` body -> Just $ Iterate' t2 (Len' t1 xs) (Lam x2 t2 body) init   _ -> Nothing -reduceFoldBuild :: MonadAlpha m => RewriteRule m+reduceFoldBuild :: (MonadAlpha m, MonadError Error m) => RewriteRule m reduceFoldBuild =   mconcat     [ -- reduce `Foldl`@@ -141,7 +141,7 @@       [r| "len/build" forall f base n. len (build f base n) = len base + n |]     ] -rule :: MonadAlpha m => RewriteRule m+rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m rule =   mconcat     [ reduceFoldMap,@@ -197,8 +197,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.ShortCutFusion" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
+ src/Jikka/Core/Convert/SortAbs.hs view
@@ -0,0 +1,135 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-}++-- |+-- Module      : Jikka.Core.Convert.SortAbs+-- Description : remove abs with sorting. / sort によって abs を除去します。+-- Copyright   : (c) Kimiyuki Onaka, 2021+-- License     : Apache License 2.0+-- Maintainer  : kimiyuki95@gmail.com+-- Stability   : experimental+-- Portability : portable+--+-- \[+--     \newcommand\int{\mathbf{int}}+--     \newcommand\bool{\mathbf{bool}}+--     \newcommand\list{\mathbf{list}}+-- \]+module Jikka.Core.Convert.SortAbs+  ( run,++    -- * internal rules+    rule,+  )+where++import Control.Monad.Trans.Maybe+import Jikka.Common.Alpha+import Jikka.Common.Error+import qualified Jikka.Core.Convert.Alpha as Alpha+import Jikka.Core.Language.ArithmeticExpr+import Jikka.Core.Language.Beta+import Jikka.Core.Language.BuiltinPatterns+import Jikka.Core.Language.Expr+import Jikka.Core.Language.Lint+import Jikka.Core.Language.QuasiRules+import Jikka.Core.Language.RewriteRules+import Jikka.Core.Language.Util++-- | @replaceAbsDelta x y z e@ replaces \(\levert x - y \rvert\) in \(e\) with \(z\).+replaceAbsDelta :: VarName -> VarName -> VarName -> Expr -> Expr+replaceAbsDelta x y z e = mapSubExpr go [] e+  where+    go _ = \case+      Abs' e | isZeroArithmeticExpr (parseArithmeticExpr (Minus' e (Minus' (Var x) (Var y)))) -> Var z+      Abs' e | isZeroArithmeticExpr (parseArithmeticExpr (Minus' e (Minus' (Var y) (Var x)))) -> Var z+      e -> e++swapTwoVars :: MonadAlpha m => VarName -> VarName -> Expr -> m Expr+swapTwoVars x y e = do+  x' <- genVarName x+  y' <- genVarName y+  e <- substitute x (Var x') e+  e <- substitute y (Var y') e+  e <- substitute x' (Var y) e+  substitute y' (Var x) e++-- | TODO: accept more functions+isSymmetric :: MonadAlpha m => VarName -> VarName -> Expr -> m Bool+isSymmetric x y f = do+  g <- swapTwoVars x y f+  return $ parseArithmeticExpr g == parseArithmeticExpr f++rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m+rule = makeRewriteRule "sum/sum/abs/symmetric" $ \env -> \case+  Sum' (Map' IntTy _ (Lam x _ (Sum' (Map' _ _ (Lam y _ f) xs'))) xs) | xs' == xs -> runMaybeT $ do+    delta <- lift genVarName'+    let f' = replaceAbsDelta x y delta f+    guard $ f' /= f -- f has |x - y|+    guard =<< lift (isSymmetric x y f') -- symmetric+    ys <- lift $ genVarName'' xs+    i <- lift genVarName'+    j <- lift genVarName'+    lt <- lift $ substitute delta (Minus' (Var x) (Var y)) f'+    eq <- lift $ substitute delta (LitInt' 0) f'+    gt <- lift $ substitute delta (Minus' (Var y) (Var x)) f'+    let ctx = Let y IntTy (At' IntTy (Var ys) (Var j))+    let lt' = Sum' (Map' IntTy IntTy (Lam j IntTy (ctx lt)) (Range1' (Var i)))+    let eq' = Let j IntTy (Var i) (ctx eq)+    let gt' = Sum' (Map' IntTy IntTy (Lam j IntTy (ctx gt)) (Range2' (Plus' (Var i) (LitInt' 1)) (Len' IntTy (Var ys))))+    let e =+          Let ys (ListTy IntTy) (Sorted' IntTy xs) $+            Sum'+              ( Map'+                  IntTy+                  IntTy+                  ( Lam+                      i+                      IntTy+                      ( Let+                          x+                          IntTy+                          (At' IntTy (Var ys) (Var i))+                          (Plus' (Plus' lt' eq') gt')+                      )+                  )+                  (Range1' (Len' IntTy (Var ys)))+              )+    lift $ Alpha.runExpr (typeEnv env) e+  _ -> return Nothing++runProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Program+runProgram = applyRewriteRuleProgram' rule++-- | `run` reduces \(\lvert \sum _ {a_i \in a} \sum _ {a_j \in a} f(a, a_i, a_j) \rvert\) to \(\mathbf{let}~ b = \mathrm{sort}(a) ~\mathbf{in}~ \sum \sum f'(a, a_i, a_j)\) when \(f\) contains \(\lvert a_i - a_j \rvert\) and \(f(a, a_i, a_j) = f(a, a_j, a_i)\) holds.+--+-- == Example+--+-- Before:+--+-- > sum (map (fun (a_i: int) ->+-- >     sum (map (fun (a_j: int) ->+-- >         abs (a_i - a_j)+-- >     ) a)+-- > ) a)+--+-- After:+--+-- > let b = sort a+-- > in sum (map (fun (i: int) ->+-- >     (sum (map (fun (b_j: int) ->+-- >         b_i - b_j+-- >     ) b[:i])+-- >     + 0+-- >     + sum (map (fun (b_j: int) ->+-- >         b_j - b_i+-- >     ) b[i + 1:]))+-- > ) (range (length b)))+run :: (MonadAlpha m, MonadError Error m) => Program -> m Program+run prog = wrapError' "Jikka.Core.Convert.SortAbs" $ do+  precondition $ do+    lint prog+  prog <- runProgram prog+  postcondition $ do+    lint prog+  return prog
src/Jikka/Core/Convert/SpecializeFoldl.hs view
@@ -131,8 +131,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.SpecializeFoldl" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/TrivialLetElimination.hs view
@@ -91,8 +91,8 @@ run :: MonadError Error m => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.ConstantPropagation" $ do   precondition $ do-    ensureWellTyped prog+    lint prog   prog <- return $ run' prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Convert/TypeInfer.hs view
@@ -39,7 +39,8 @@ import Jikka.Core.Language.Expr import Jikka.Core.Language.FreeVars import Jikka.Core.Language.Lint-import Jikka.Core.Language.TypeCheck (literalToType, typecheckExpr, typecheckProgram)+import Jikka.Core.Language.NameCheck (namecheckExpr)+import Jikka.Core.Language.TypeCheck (literalToType, typecheckExpr) import Jikka.Core.Language.Util  data Hint@@ -151,6 +152,7 @@  -- | `Subst` is type substituion. It's a mapping from type variables to their actual types. newtype Subst = Subst {unSubst :: M.Map TypeName Type}+  deriving (Eq, Ord, Show, Read)  subst :: Subst -> Type -> Type subst sigma = \case@@ -247,7 +249,9 @@ -- > in let x: int = 1 -- > in f(x + x) run :: (MonadAlpha m, MonadError Error m) => Program -> m Program-run prog = wrapError' "Jikka.Core.Convert.TypeInfer" $ do+run prog = wrapError' "Jikka.Core.Convert.TypeInfer.run" $ do+  precondition $ do+    ensureAlphaConverted prog   eqns <- formularizeProgram prog   let (eqns', assertions) = sortEquations eqns   let eqns'' = mergeAssertions assertions@@ -255,24 +259,31 @@   let t0 = Just UnitTy   prog <- substProgram t0 sigma prog   postcondition $ do-    typecheckProgram prog+    ensureAlphaConverted prog+    ensureWellTyped prog   return prog  runExpr :: (MonadAlpha m, MonadError Error m) => [(VarName, Type)] -> Expr -> m Expr-runExpr env e = wrapError' "Jikka.Core.Convert.TypeInfer" $ do+runExpr env e = wrapError' "Jikka.Core.Convert.TypeInfer.runExpr" $ do+  precondition $ do+    namecheckExpr env e   eqns <- getDual <$> execWriterT (formularizeExpr e)   let (eqns', assertions) = sortEquations eqns-  let eqns'' = mergeAssertions assertions+  let eqns'' = mergeAssertions (env ++ assertions)   sigma <- solveEquations (eqns' ++ eqns'')   let t0 = Nothing -- don't use substDefault   env <- return $ map (second (subst' t0 sigma)) env   e <- substExpr t0 sigma env e   postcondition $ do+    namecheckExpr env e     typecheckExpr env e   return e  runRule :: (MonadAlpha m, MonadError Error m) => [(VarName, Type)] -> Expr -> Expr -> m ([(VarName, Type)], Expr, Expr)-runRule args e1 e2 = wrapError' "Jikka.Core.Convert.TypeInfer" $ do+runRule args e1 e2 = wrapError' "Jikka.Core.Convert.TypeInfer.runRule" $ do+  precondition $ do+    -- Underscores are allowed for names, so we don't use namecheckExpr here.+    return ()   eqns <- (getDual <$>) . execWriterT $ do     t <- formularizeExpr e1     formularizeExpr' e2 t@@ -282,4 +293,8 @@   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+  postcondition $ do+    -- Underscores are allowed for names, so we don't use namecheckExpr here.+    -- Type variables can remain, so we don't use typecheckExpr here.+    return ()   return (args, e1, e2)
src/Jikka/Core/Convert/UnpackTuple.hs view
@@ -19,7 +19,6 @@  import Jikka.Common.Alpha import Jikka.Common.Error-import qualified Jikka.Core.Convert.Alpha as Alpha import Jikka.Core.Language.Beta import Jikka.Core.Language.BuiltinPatterns import Jikka.Core.Language.Expr@@ -83,9 +82,8 @@ run :: (MonadAlpha m, MonadError Error m) => Program -> m Program run prog = wrapError' "Jikka.Core.Convert.UnpackTuple" $ do   precondition $ do-    ensureWellTyped prog-  prog <- Alpha.run prog+    lint prog   prog <- runProgram prog   postcondition $ do-    ensureWellTyped prog+    lint prog   return prog
src/Jikka/Core/Language/ArithmeticExpr.hs view
@@ -12,14 +12,20 @@     plusArithmeticExpr,     minusArithmeticExpr,     multArithmeticExpr,+    incrArithmeticExpr,+    decrArithmeticExpr,+    sumArithmeticExpr,     isZeroArithmeticExpr,     isOneArithmeticExpr,+    isIntegerArithmeticExpr,+    integerFromArithmeticExpr,      -- * Advanced functions     unNPlusKPattern,     makeVectorFromArithmeticExpr,     makeAffineFunctionFromArithmeticExpr,     splitConstantFactorArithmeticExpr,+    splitToSumArithmeticExpr,   ) where @@ -143,6 +149,15 @@ multArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr -> ArithmeticExpr multArithmeticExpr (ArithmeticExpr e1) (ArithmeticExpr e2) = ArithmeticExpr $ multSumExpr e1 e2 +incrArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr+incrArithmeticExpr = plusArithmeticExpr (integerArithmeticExpr 1)++decrArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr+decrArithmeticExpr = plusArithmeticExpr (integerArithmeticExpr (-1))++sumArithmeticExpr :: [ArithmeticExpr] -> ArithmeticExpr+sumArithmeticExpr = foldl plusArithmeticExpr (integerArithmeticExpr 0)+ parseSumExpr :: Expr -> SumExpr parseSumExpr = \case   LitInt' n -> SumExpr {sumExprList = [], sumExprConst = n}@@ -242,6 +257,14 @@ isOneArithmeticExpr :: ArithmeticExpr -> Bool isOneArithmeticExpr e = normalizeArithmeticExpr e == integerArithmeticExpr 1 +isIntegerArithmeticExpr :: ArithmeticExpr -> Bool+isIntegerArithmeticExpr e = normalizeArithmeticExpr e == integerArithmeticExpr (sumExprConst (unArithmeticExpr e))++integerFromArithmeticExpr :: ArithmeticExpr -> Maybe Integer+integerFromArithmeticExpr e+  | isIntegerArithmeticExpr e = Just (sumExprConst (unArithmeticExpr e))+  | otherwise = Nothing+ -- | `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@@ -283,3 +306,10 @@  splitConstantFactorProductExpr :: ProductExpr -> (Integer, ProductExpr) splitConstantFactorProductExpr e = (productExprConst e, e {productExprConst = 1})++splitToSumArithmeticExpr :: ArithmeticExpr -> [ArithmeticExpr]+splitToSumArithmeticExpr e =+  let e' = unArithmeticExpr $ normalizeArithmeticExpr e+      es = map arithmeticalExprFromProductExpr (sumExprList e')+      k = if sumExprConst e' == 0 then [] else [integerArithmeticExpr (sumExprConst e')]+   in es ++ k
+ src/Jikka/Core/Language/AssertedHint.hs view
@@ -0,0 +1,274 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-}++module Jikka.Core.Language.AssertedHint+  ( AssertedHint (..),+    pattern EqualHint,+    parseHints,++    -- * Functions using hints+    lowerBoundWithHints,+    upperBoundWithHints,+    isZeroWithHints,+    nullWithHints,+    lengthWithHints,+  )+where++import Control.Monad+import Data.Semigroup+import Jikka.Core.Language.ArithmeticExpr+import Jikka.Core.Language.BuiltinPatterns+import Jikka.Core.Language.Expr++data AssertedHint+  = -- | @NotEqualHint n@ for a integer variable @x@ means @x /= n@+    NotEqualHint ArithmeticExpr+  | -- | @BoundHint l r@ for a integer variable @x@ means @l <= x < r@+    BoundHint (Maybe ArithmeticExpr) (Maybe ArithmeticExpr)+  | -- | @LengthHint t hint@ for a list variable @xs@ means @length xs@ satisfies @hint@+    LengthHint Type AssertedHint+  | -- | @AllHint t hint@ for a list variable @xs@ means that @x@ satisfies @hint@ for all @x@ in @xs@+    AllHint Type AssertedHint+  deriving (Eq, Ord, Show)++pattern EqualHint :: ArithmeticExpr -> AssertedHint+pattern EqualHint l <-+  (\case BoundHint (Just l) (Just r) | incrArithmeticExpr l == r -> Just l; _ -> Nothing -> Just l)+  where+    EqualHint l = BoundHint (Just l) (Just (incrArithmeticExpr l))++parseNilHint :: Expr -> [(VarName, AssertedHint)]+parseNilHint = \case+  -- Jikka.Core.Language.EqualitiySolving makes rhs nil+  Equal' _ (Var xs) (Nil' t) -> [(xs, LengthHint t (BoundHint (Just (integerArithmeticExpr 0)) (Just (integerArithmeticExpr 1))))]+  NotEqual' _ (Var xs) (Nil' t) -> [(xs, LengthHint t (BoundHint (Just (integerArithmeticExpr 1)) Nothing))]+  _ -> []++data Term+  = VarTerm VarName+  | LenTerm Type VarName+  | NegatedTerm Term+  deriving (Eq, Ord, Show, Read)++-- `decomposeArithmeticExpr` makes @a + b + c@ to @[(a, b + c), (b, a + c), (c, a + b)]@ in a convenient way, because Jikka.Core.Language.EqualitiySolving makes @a == b@ to @a - b == 0@.+decomposeArithmeticExpr :: Expr -> [(Term, ArithmeticExpr)]+decomposeArithmeticExpr e =+  let es = splitToSumArithmeticExpr $ parseArithmeticExpr e+   in (`concatMap` [0 .. length es - 1]) $ \i ->+        let e = es !! i+            e' = sumArithmeticExpr $ take i es ++ drop (i + 1) es+         in case formatArithmeticExpr e of+              Var x -> [(VarTerm x, e')]+              Negate' (Var x) -> [(NegatedTerm (VarTerm x), e')]+              Len' t (Var x) -> [(LenTerm t x, e')]+              Negate' (Len' t (Var x)) -> [(NegatedTerm (LenTerm t x), e')]+              _ -> []++parseBoundHint :: Expr -> [(VarName, AssertedHint)]+parseBoundHint = \case+  Equal' IntTy e (LitInt' 0) -> do+    (x, e) <- decomposeArithmeticExpr e+    case x of+      VarTerm x -> return (x, EqualHint (negateArithmeticExpr e))+      NegatedTerm (VarTerm x) -> return (x, EqualHint e)+      LenTerm t x -> return (x, LengthHint t (EqualHint (negateArithmeticExpr e)))+      NegatedTerm (LenTerm t x) -> return (x, LengthHint t (EqualHint e))+      _ -> []+  NotEqual' IntTy e (LitInt' 0) -> do+    (x, e) <- decomposeArithmeticExpr e+    case x of+      VarTerm x -> return (x, NotEqualHint (negateArithmeticExpr e))+      NegatedTerm (VarTerm x) -> return (x, NotEqualHint e)+      LenTerm t x | isZeroArithmeticExpr e -> return (x, LengthHint t (BoundHint (Just (integerArithmeticExpr 1)) Nothing))+      NegatedTerm (LenTerm t x) | isZeroArithmeticExpr e -> return (x, LengthHint t (BoundHint (Just (integerArithmeticExpr 1)) Nothing))+      _ -> []+  LessEqual' IntTy e (LitInt' 0) -> do+    (x, e) <- decomposeArithmeticExpr e+    case x of+      VarTerm x -> return (x, BoundHint Nothing (Just (incrArithmeticExpr (negateArithmeticExpr e))))+      NegatedTerm (VarTerm x) -> return (x, BoundHint (Just e) Nothing)+      LenTerm t x -> return (x, LengthHint t (BoundHint Nothing (Just (incrArithmeticExpr (negateArithmeticExpr e)))))+      NegatedTerm (LenTerm t x) -> return (x, LengthHint t (BoundHint (Just e) Nothing))+      _ -> []+  LessThan' IntTy e (LitInt' 0) -> do+    (x, e) <- decomposeArithmeticExpr e+    case x of+      VarTerm x -> return (x, BoundHint Nothing (Just (negateArithmeticExpr e)))+      NegatedTerm (VarTerm x) -> return (x, BoundHint (Just (incrArithmeticExpr e)) Nothing)+      LenTerm t x -> return (x, LengthHint t (BoundHint Nothing (Just (negateArithmeticExpr e))))+      NegatedTerm (LenTerm t x) -> return (x, LengthHint t (BoundHint (Just (incrArithmeticExpr e)) Nothing))+      _ -> []+  -- Jikka.Core.Language.EqualitiySolving makes rhs 0 and removes GreaterEqual and GreaterThan+  _ -> []++parseAndHint :: Expr -> [(VarName, AssertedHint)]+parseAndHint = \case+  And' e e' -> parseHints e ++ parseHints e'+  _ -> []++parseAllHint :: Expr -> [(VarName, AssertedHint)]+parseAllHint = \case+  All' (Map' t _ (Lam x _ pred) (Var xs)) -> do+    (x', hint) <- parseHints pred+    guard $ x' == x+    return (xs, AllHint t hint)+  _ -> []++parseHints :: Expr -> [(VarName, AssertedHint)]+parseHints e =+  concat+    [ parseNilHint e,+      parseBoundHint e,+      parseAndHint e,+      parseAllHint e+    ]++selectHints :: [(VarName, AssertedHint)] -> VarName -> [AssertedHint]+selectHints hints x = map snd (filter (\hint -> fst hint == x) hints)++maximum' :: Ord a => [Maybe a] -> Maybe a+maximum' = (getMax <$>) . mconcat . map (Max <$>)++minimum' :: Ord a => [Maybe a] -> Maybe a+minimum' = (getMin <$>) . mconcat . map (Min <$>)++lowerBoundWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer+lowerBoundWithHints hints = \case+  LitInt' n -> Just n+  Negate' e -> do+    e <- upperBoundWithHints hints e+    return $ - (e - 1)+  Plus' e1 e2 -> do+    e1 <- lowerBoundWithHints hints e1+    e2 <- lowerBoundWithHints hints e2+    return $ e1 + e2+  Minus' e1 e2 -> do+    e1 <- lowerBoundWithHints hints e1+    e2 <- upperBoundWithHints hints e2+    return $ e1 - (e2 - 1)+  Mult' e1 e2 -> do+    e1 <- lowerBoundWithHints hints e1+    e2 <- lowerBoundWithHints hints e2+    guard $ e1 >= 0 && e2 >= 0+    return $ e1 * e2+  Var x ->+    let go :: AssertedHint -> Maybe Integer+        go = \case+          BoundHint (Just l) _ -> lowerBoundWithHints hints (formatArithmeticExpr l)+          _ -> Nothing+     in maximum' (map go (selectHints hints x))+  _ -> Nothing++upperBoundWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer+upperBoundWithHints hints = \case+  LitInt' n -> Just (n + 1)+  Negate' e -> do+    e <- lowerBoundWithHints hints e+    return $ - e + 1+  Plus' e1 e2 -> do+    e1 <- upperBoundWithHints hints e1+    e2 <- upperBoundWithHints hints e2+    return $ e1 + e2 - 1+  Minus' e1 e2 -> do+    e1 <- upperBoundWithHints hints e1+    e2 <- lowerBoundWithHints hints e2+    return $ e1 - e2+  Mult' e1 e2 -> do+    l1 <- lowerBoundWithHints hints e1+    l2 <- lowerBoundWithHints hints e2+    r1 <- upperBoundWithHints hints e1+    r2 <- upperBoundWithHints hints e2+    guard $ l1 >= 0 && l2 >= 0+    return $ (r1 - 1) * (r2 - 1) + 1+  Var x ->+    let go :: AssertedHint -> Maybe Integer+        go = \case+          BoundHint _ (Just r) -> pred <$> upperBoundWithHints hints (formatArithmeticExpr r)+          _ -> Nothing+     in minimum' (map go (selectHints hints x))+  _ -> Nothing++isZeroWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Bool+isZeroWithHints hints e =+  case (lowerBoundWithHints hints e, upperBoundWithHints hints e) of+    (Just 0, Just 1) -> Just True+    (Just l, _) | l >= 1 -> Just False+    (_, Just r) | r <= 0 -> Just False+    _ -> Nothing++integerWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer+integerWithHints hints = \case+  LitInt' n -> Just n+  Negate' e -> do+    e <- integerWithHints hints e+    return $ - e+  Plus' e1 e2 -> do+    e1 <- integerWithHints hints e1+    e2 <- integerWithHints hints e2+    return $ e1 + e2+  Minus' e1 e2 -> do+    e1 <- integerWithHints hints e1+    e2 <- integerWithHints hints e2+    return $ e1 - e2+  Mult' e1 e2 -> do+    e1 <- integerWithHints hints e1+    e2 <- integerWithHints hints e2+    return $ e1 * e2+  e@(Var _) ->+    case (lowerBoundWithHints hints e, upperBoundWithHints hints e) of+      (Just l, Just r) | l + 1 == r -> Just l+      _ -> Nothing+  _ -> Nothing++nullWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Bool+nullWithHints hints = \case+  Nil' _ -> Just True+  Cons' _ _ _ -> Just False+  Range1' n -> isZeroWithHints hints n+  Var xs -> do+    let go :: AssertedHint -> Maybe Integer+        go = \case+          LengthHint _ (BoundHint (Just l) _) -> lowerBoundWithHints hints (formatArithmeticExpr l)+          _ -> Nothing+    l <- maximum' (map go (selectHints hints xs))+    if l >= 1+      then Just False+      else do+        let go :: AssertedHint -> Maybe Integer+            go = \case+              LengthHint _ (NotEqualHint n) -> integerWithHints hints (formatArithmeticExpr n)+              _ -> Nothing+        let ns = map go (selectHints hints xs)+        if Just 0 `elem` ns+          then Just False+          else do+            let go :: AssertedHint -> Maybe Integer+                go = \case+                  LengthHint _ (BoundHint _ (Just r)) -> pred <$> upperBoundWithHints hints (formatArithmeticExpr r)+                  _ -> Nothing+            r <- minimum' (map go (selectHints hints xs))+            if r <= 1+              then Just True+              else Nothing+  _ -> Nothing++lengthWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer+lengthWithHints hints = \case+  Nil' _ -> Just 0+  Cons' _ _ xs -> do+    n <- lengthWithHints hints xs+    return $ n + 1+  Range1' e -> case (lowerBoundWithHints hints e, upperBoundWithHints hints e) of+    (Just l, Just r) | l + 1 == r -> Just l+    _ -> Nothing+  Var xs -> do+    let go :: AssertedHint -> Maybe Integer+        go = \case+          LengthHint _ (BoundHint (Just l) _) -> lowerBoundWithHints hints (formatArithmeticExpr l)+          _ -> Nothing+    let minimum' :: Ord a => [Maybe a] -> Maybe a+        minimum' = (getMin <$>) . mconcat . map (Min <$>)+    minimum' (map go (selectHints hints xs))+  _ -> Nothing
src/Jikka/Core/Language/Lint.hs view
@@ -14,6 +14,7 @@  import Jikka.Common.Error import Jikka.Core.Language.Expr+import Jikka.Core.Language.NameCheck import Jikka.Core.Language.TypeCheck  precondition :: MonadError Error m => m a -> m a@@ -31,3 +32,12 @@ ensureWellTyped prog = wrapError' "Jikka.Core.Language.Lint.ensureWellTyped" $ do   _ <- typecheckProgram prog   return ()++ensureAlphaConverted :: MonadError Error m => Program -> m ()+ensureAlphaConverted prog = wrapError' "Jikka.Core.Language.Lint.ensureAlphaConverted" $ do+  namecheckProgram prog++lint :: MonadError Error m => Program -> m ()+lint prog = do+  ensureAlphaConverted prog+  ensureWellTyped prog
+ src/Jikka/Core/Language/NameCheck.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-}++-- |+-- Module      : Jikka.Core.Language.RewriteRules+-- Description : checks that there are no name conflicts. / 名前衝突がないか検査します。+-- Copyright   : (c) Kimiyuki Onaka, 2021+-- License     : Apache License 2.0+-- Maintainer  : kimiyuki95@gmail.com+-- Stability   : experimental+-- Portability : portable+module Jikka.Core.Language.NameCheck+  ( namecheckProgram,+    namecheckToplevelExpr,+    namecheckExpr,+  )+where++import Control.Monad.State.Strict+import Jikka.Common.Error+import Jikka.Core.Format (formatType)+import Jikka.Core.Language.Expr+import Jikka.Core.Language.Util++define :: (MonadState [(VarName, Type)] m, MonadError Error m) => VarName -> Type -> m ()+define x t = do+  env <- get+  case lookup x env of+    Just t' -> throwInternalError $ "name conflict: " ++ unVarName x ++ ": " ++ formatType t ++ " and " ++ unVarName x ++ ": " ++ formatType t'+    Nothing -> put $ (x, t) : env++namecheckExpr' :: (MonadState [(VarName, Type)] m, MonadError Error m) => Expr -> m ()+namecheckExpr' = \case+  Var x -> do+    env <- get+    case lookup x env of+      Nothing -> throwInternalError $ "undefined variable: " ++ unVarName x+      Just _ -> return ()+  Lit _ -> return ()+  App f e -> do+    namecheckExpr' f+    namecheckExpr' e+  Lam x t e -> do+    define x t+    namecheckExpr' e+  Let x t e1 e2 -> do+    namecheckExpr' e1+    define x t+    namecheckExpr' e2+  Assert e1 e2 -> do+    namecheckExpr' e1+    namecheckExpr' e2++namecheckExpr :: MonadError Error m => [(VarName, Type)] -> Expr -> m ()+namecheckExpr env e = wrapError' "Jikka.Core.Language.NameCheck.namecheckExpr" $ do+  evalStateT (namecheckExpr' e) env++namecheckToplevelExpr' :: (MonadState [(VarName, Type)] m, MonadError Error m) => ToplevelExpr -> m ()+namecheckToplevelExpr' = \case+  ResultExpr e -> namecheckExpr' e+  ToplevelLet x t e cont -> do+    namecheckExpr' e+    define x t+    namecheckToplevelExpr' cont+  ToplevelLetRec f args ret body cont -> do+    let t = curryFunTy (map snd args) ret+    define f t+    forM_ args $ \(x, t) -> do+      define x t+    namecheckExpr' body+    namecheckToplevelExpr' cont+  ToplevelAssert e1 e2 -> do+    namecheckExpr' e1+    namecheckToplevelExpr' e2++namecheckToplevelExpr :: MonadError Error m => [(VarName, Type)] -> ToplevelExpr -> m ()+namecheckToplevelExpr env e = wrapError' "Jikka.Core.Language.NameCheck.namecheckToplevelExpr" $ do+  evalStateT (namecheckToplevelExpr' e) env++namecheckProgram :: MonadError Error m => Program -> m ()+namecheckProgram prog = wrapError' "Jikka.Core.Language.NameCheck.namecheckProgram" $ do+  evalStateT (namecheckToplevelExpr' prog) []
src/Jikka/Core/Language/QuasiRules.hs view
@@ -9,6 +9,7 @@      -- * Things which `r` uses.     module Jikka.Core.Language.Expr,+    alphaExpr,     makeRewriteRule,     genVarName',   )@@ -17,8 +18,10 @@ import Control.Arrow import Control.Monad.State.Strict import Data.Data+import Jikka.Common.Alpha import Jikka.Common.Error import Jikka.Common.Format.Error+import qualified Jikka.Core.Convert.Alpha as Alpha import qualified Jikka.Core.Convert.TypeInfer as TypeInfer import Jikka.Core.Language.Expr import Jikka.Core.Language.RewriteRules@@ -255,6 +258,9 @@       e <- lift [e|Assert $(pure e1) $(pure e2)|]       return (stmts1 ++ stmts2, e) +alphaExpr :: (MonadAlpha m, MonadError Error m) => [(VarName, Type)] -> Expr -> m Expr+alphaExpr = Alpha.runExpr+ ruleExp :: String -> Q Exp ruleExp s = do   (name, args, e1, e2) <- liftError $ parseRule s@@ -274,11 +280,15 @@   supressUnusedMatchesWarnings' <- forM (typeVars env) $ \(_, y) -> do     NoBindS <$> [e|return $(pure (VarE y))|]   ((stmts, exp), _) <- runStateT (toExpE e2) env-  exp' <- [e|return (Just $(pure exp))|]-  let stmts' = supressUnusedMatchesWarnings ++ supressUnusedMatchesWarnings' ++ stmts ++ [NoBindS exp']+  nop <- [e|return ()|]+  exp' <- [e|return $(pure exp)|]   [e|-    makeRewriteRule $(pure (LitE (StringL name))) $ \_ e -> case e of-      $(pure pat) -> $(pure (DoE stmts'))+    makeRewriteRule $(pure (LitE (StringL name))) $ \env e -> case e of+      $(pure pat) -> do+        $(pure (DoE (supressUnusedMatchesWarnings ++ [NoBindS nop])))+        $(pure (DoE (supressUnusedMatchesWarnings' ++ [NoBindS nop])))+        e <- $(pure (DoE (stmts ++ [NoBindS exp'])))+        Just <$> alphaExpr (typeEnv env) e       _ -> return Nothing     |]
src/Jikka/Core/Language/RewriteRules.hs view
@@ -12,6 +12,7 @@ -- Portability : portable module Jikka.Core.Language.RewriteRules   ( RewriteRule,+    RewriteEnvironment (..),      -- * Construct Rules     makeRewriteRule,@@ -20,6 +21,8 @@     traceRewriteRule,      -- * Apply Rules+    emptyRewriteEnvironment,+    makeRewriteEnvironmentFromTypeEnv,     applyRewriteRule,     applyRewriteRuleToplevelExpr,     applyRewriteRuleProgram,@@ -32,11 +35,21 @@ import Debug.Trace import Jikka.Common.Error import Jikka.Core.Format (formatExpr)+import Jikka.Core.Language.AssertedHint import Jikka.Core.Language.Expr import Jikka.Core.Language.Util (curryFunTy) +data RewriteEnvironment = RewriteEnvironment+  { typeEnv :: [(VarName, Type)],+    assertedHints :: [(VarName, AssertedHint)]+  }+  deriving (Eq, Ord, Show)++putTypeEnv :: (VarName, Type) -> RewriteEnvironment -> RewriteEnvironment+putTypeEnv (x, t) env = env {typeEnv = (x, t) : typeEnv env}+ data RewriteRule m-  = RewriteRule ([(VarName, Type)] -> Expr -> m (Maybe Expr))+  = RewriteRule (RewriteEnvironment -> Expr -> m (Maybe Expr))   | NamedRule String (RewriteRule m)   | EmptyRule   | AltRule (RewriteRule m) (RewriteRule m)@@ -48,7 +61,7 @@ instance Monad m => Monoid (RewriteRule m) where   mempty = EmptyRule -applyRewriteRuleToRootExpr :: MonadError Error m => RewriteRule m -> [(VarName, Type)] -> Expr -> StateT Integer m (Maybe Expr)+applyRewriteRuleToRootExpr :: MonadError Error m => RewriteRule m -> RewriteEnvironment -> Expr -> StateT Integer m (Maybe Expr) applyRewriteRuleToRootExpr f env e = go "(anonymous)" False f   where     go :: MonadError Error m => String -> Bool -> RewriteRule m -> StateT Integer m (Maybe Expr)@@ -75,10 +88,10 @@           Nothing -> go ruleName dumpTrace g       TraceRule f -> go ruleName True f -makeRewriteRule :: Monad m => String -> ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m+makeRewriteRule :: Monad m => String -> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m makeRewriteRule name f = NamedRule name (RewriteRule f) -pureRewriteRule :: Monad m => String -> ([(VarName, Type)] -> Expr -> Maybe Expr) -> RewriteRule m+pureRewriteRule :: Monad m => String -> (RewriteEnvironment -> Expr -> Maybe Expr) -> RewriteRule m pureRewriteRule name f = NamedRule name (RewriteRule (\env e -> return (f env e)))  simpleRewriteRule :: Monad m => String -> (Expr -> Maybe Expr) -> RewriteRule m@@ -93,10 +106,10 @@ -- -- * This function is idempotent. -- * This function doesn't terminate when a given rewrite rule doesn't terminate.-applyRewriteRule :: MonadError Error m => RewriteRule m -> [(VarName, Type)] -> Expr -> m (Maybe Expr)+applyRewriteRule :: MonadError Error m => RewriteRule m -> RewriteEnvironment -> Expr -> m (Maybe Expr) applyRewriteRule f env e = evalStateT (applyRewriteRule' f env e) 0 -applyRewriteRule' :: (MonadError Error m) => RewriteRule m -> [(VarName, Type)] -> Expr -> StateT Integer m (Maybe Expr)+applyRewriteRule' :: (MonadError Error m) => RewriteRule m -> RewriteEnvironment -> Expr -> StateT Integer m (Maybe Expr) applyRewriteRule' = applyRewriteRulePreOrder  coalesceMaybes :: a -> Maybe a -> b -> Maybe b -> Maybe (a, b)@@ -105,7 +118,7 @@ coalesceMaybes _ (Just a) b Nothing = Just (a, b) coalesceMaybes _ (Just a) _ (Just b) = Just (a, b) -applyRewriteRuleToImmediateSubExprs :: MonadError Error m => RewriteRule m -> [(VarName, Type)] -> Expr -> StateT Integer m (Maybe Expr)+applyRewriteRuleToImmediateSubExprs :: MonadError Error m => RewriteRule m -> RewriteEnvironment -> Expr -> StateT Integer m (Maybe Expr) applyRewriteRuleToImmediateSubExprs f env = \case   Var _ -> return Nothing   Lit _ -> return Nothing@@ -113,13 +126,14 @@     e1' <- applyRewriteRuleToRootExpr f env e1     e2' <- applyRewriteRuleToRootExpr f env e2     return $ fmap (uncurry App) (coalesceMaybes e1 e1' e2 e2')-  Lam x t body -> (Lam x t <$>) <$> applyRewriteRuleToRootExpr f ((x, t) : env) body+  Lam x t body -> (Lam x t <$>) <$> applyRewriteRuleToRootExpr f (putTypeEnv (x, t) env) body   Let x t e1 e2 -> do     e1' <- applyRewriteRuleToRootExpr f env e1-    e2' <- applyRewriteRuleToRootExpr f ((x, t) : env) e2+    e2' <- applyRewriteRuleToRootExpr f (putTypeEnv (x, t) env) e2     return $ fmap (uncurry (Let x t)) (coalesceMaybes e1 e1' e2 e2')   Assert e1 e2 -> do     e1' <- applyRewriteRuleToRootExpr f env e1+    env <- return $ env {assertedHints = parseHints (fromMaybe e1 e1') ++ assertedHints env}     e2' <- applyRewriteRuleToRootExpr f env e2     return $ fmap (uncurry Assert) (coalesceMaybes e1 e1' e2 e2') @@ -130,7 +144,7 @@   put s   return a -applyRewriteRulePreOrder :: forall m. MonadError Error m => RewriteRule m -> [(VarName, Type)] -> Expr -> StateT Integer m (Maybe Expr)+applyRewriteRulePreOrder :: forall m. MonadError Error m => RewriteRule m -> RewriteEnvironment -> Expr -> StateT Integer m (Maybe Expr) applyRewriteRulePreOrder f env e = do   e' <- applyRewriteRuleToRootExpr f env e   case e' of@@ -150,25 +164,32 @@       e'' <- applyRewriteRulePreOrder f env e'       return . Just $ fromMaybe e' e'' -applyRewriteRuleToplevelExpr :: MonadError Error m => RewriteRule m -> [(VarName, Type)] -> ToplevelExpr -> StateT Integer m (Maybe ToplevelExpr)+applyRewriteRuleToplevelExpr :: MonadError Error m => RewriteRule m -> RewriteEnvironment -> ToplevelExpr -> StateT Integer m (Maybe ToplevelExpr) applyRewriteRuleToplevelExpr f env = \case   ResultExpr e -> (ResultExpr <$>) <$> applyRewriteRule' f env e   ToplevelLet y t e cont -> do     e' <- applyRewriteRule' f env e-    cont' <- applyRewriteRuleToplevelExpr f ((y, t) : env) cont+    cont' <- applyRewriteRuleToplevelExpr f (putTypeEnv (y, t) env) cont     return $ fmap (uncurry (ToplevelLet y t)) (coalesceMaybes e e' cont cont')   ToplevelLetRec g args ret body cont -> do-    let env' = (g, curryFunTy (map snd args) ret) : env-    body' <- applyRewriteRule' f (reverse args ++ env') body+    let env' = putTypeEnv (g, curryFunTy (map snd args) ret) env+    body' <- applyRewriteRule' f (foldr putTypeEnv env' args) body     cont' <- applyRewriteRuleToplevelExpr f env' cont     return $ fmap (uncurry (ToplevelLetRec g args ret)) (coalesceMaybes body body' cont cont')   ToplevelAssert e1 e2 -> do     e1' <- applyRewriteRule' f env e1+    env <- return $ env {assertedHints = parseHints (fromMaybe e1 e1') ++ assertedHints env}     e2' <- applyRewriteRuleToplevelExpr f env e2     return $ fmap (uncurry ToplevelAssert) (coalesceMaybes e1 e1' e2 e2') +emptyRewriteEnvironment :: RewriteEnvironment+emptyRewriteEnvironment = RewriteEnvironment {typeEnv = [], assertedHints = []}++makeRewriteEnvironmentFromTypeEnv :: [(VarName, Type)] -> RewriteEnvironment+makeRewriteEnvironmentFromTypeEnv env = RewriteEnvironment {typeEnv = env, assertedHints = []}+ applyRewriteRuleProgram :: MonadError Error m => RewriteRule m -> Program -> m (Maybe Program)-applyRewriteRuleProgram f prog = evalStateT (applyRewriteRuleToplevelExpr f [] prog) 0+applyRewriteRuleProgram f prog = evalStateT (applyRewriteRuleToplevelExpr f emptyRewriteEnvironment prog) 0  applyRewriteRuleProgram' :: MonadError Error m => RewriteRule m -> Program -> m Program applyRewriteRuleProgram' f prog = fromMaybe prog <$> applyRewriteRuleProgram f prog
src/Jikka/Core/Language/TypeCheck.hs view
@@ -199,9 +199,7 @@       throwInternalError $ "assigned type is not correct: context = (let " ++ unVarName x ++ ": " ++ formatType t ++ " = " ++ formatExpr e ++ " in ...), expected type = " ++ formatType t ++ ", actual type = " ++ formatType t'     typecheckToplevelExpr ((x, t) : env) cont   ToplevelLetRec f args ret body cont -> do-    let t = case args of-          [] -> ret-          _ -> curryFunTy (map snd args) ret+    let t = curryFunTy (map snd args) ret     ret' <- typecheckExpr (reverse args ++ (f, t) : env) body     when (ret' /= ret) $ do       throwInternalError $ "returned type is not correct: context = (let rec " ++ unVarName f ++ " " ++ unwords (map (\(x, t) -> unVarName x ++ ": " ++ formatType t) args) ++ ": " ++ formatType ret ++ " = " ++ formatExpr body ++ " in ...), expected type = " ++ formatType ret ++ ", actual type = " ++ formatType ret'
src/Jikka/Core/Language/Util.hs view
@@ -30,6 +30,11 @@ genVarName' :: MonadAlpha m => m VarName genVarName' = genVarName (VarName "_") +genVarName'' :: MonadAlpha m => Expr -> m VarName+genVarName'' = \case+  Var x -> genVarName x+  _ -> genVarName'+ mapSubTypesM :: Monad m => (Type -> m Type) -> Type -> m Type mapSubTypesM f = go   where
src/Jikka/Core/Parse/Happy.y view
@@ -592,7 +592,7 @@ runExpr :: (MonadAlpha m, MonadError Error m) => [WithLoc L.Token] -> m Expr runExpr tokens = wrapError' "Jikka.Core.Parse.Happy.runExpr" $ do     e <- liftEither $ runExpr_ tokens-    mapTypeExprM replaceUnderscoresT e+    e <- mapTypeExprM replaceUnderscoresT e     mapSubExprM replaceUnderscoresE [] e  runProgram :: (MonadAlpha m, MonadError Error m) => [WithLoc L.Token] -> m Program
test/Jikka/CPlusPlus/FormatSpec.hs view
@@ -35,7 +35,7 @@               ]       let formatted =             [ "int64_t solve(int32_t n) {",-              "    int64_t x = 0;",+              "    int64_t x = 0ll;",               "    for (int32_t i = 0; i < n; ++ i) {",               "        x += int64_t(i);",               "    }",@@ -65,7 +65,7 @@               ]       let formatted =             [ "int64_t solve(int32_t n, std::vector<int64_t> h) {",-              "    int64_t x = 0;",+              "    int64_t x = 0ll;",               "    for (int32_t i = 2; i < n; ++ i) {",               "        x += h[i - 2];",               "    }",
test/Jikka/Core/Convert/ANormalSpec.hs view
@@ -22,12 +22,12 @@           ResultExpr $             Plus'               (Let "x" IntTy Lit1 (Var "x"))-              (App (Lam "x" IntTy (Var "x")) Lit1)+              (App (Lam "y" IntTy (Var "y")) Lit1)     let expected =           ResultExpr $-            Let "x$0" IntTy Lit1 $-              Let "$3" (Fun1STy IntTy) (Lam "x$1" IntTy (Var "x$1")) $-                Let "$2" (Fun1STy IntTy) (Var "$3") $-                  Let "$4" IntTy (App (Var "$2") Lit1) $-                    Plus' (Var "x$0") (Var "$4")+            Let "x" IntTy Lit1 $+              Let "$1" (Fun1STy IntTy) (Lam "y" IntTy (Var "y")) $+                Let "$0" (Fun1STy IntTy) (Var "$1") $+                  Let "$2" IntTy (App (Var "$0") Lit1) $+                    Plus' (Var "x") (Var "$2")     run' prog `shouldBe` Right expected
test/Jikka/Core/Convert/AlphaSpec.hs view
@@ -34,14 +34,14 @@     let expected =           ResultExpr             ( Let-                "x$0"+                "x"                 IntTy                 Lit0                 ( Let-                    "x$1"+                    "x$0"                     IntTy-                    (Plus' (Var "x$0") Lit1)-                    (Var "x$1")+                    (Plus' (Var "x") Lit1)+                    (Var "x$0")                 )             )     run' prog `shouldBe` Right expected
test/Jikka/Core/Convert/BetaSpec.hs view
@@ -31,8 +31,8 @@     let expected =           ResultExpr             ( Lam-                "a$0"+                "a"                 IntTy-                (Plus' (Var "a$0") (Var "a$0"))+                (Plus' (Var "a") (Var "a"))             )     run' prog `shouldBe` Right expected
+ test/Jikka/Core/Convert/CloseMinSpec.hs view
@@ -0,0 +1,74 @@+{-# LANGUAGE OverloadedStrings #-}++module Jikka.Core.Convert.CloseMinSpec (spec) where++import Jikka.Common.Alpha+import Jikka.Common.Error+import Jikka.Core.Convert.CloseMin (rule)+import qualified Jikka.Core.Convert.TypeInfer as TypeInfer+import Jikka.Core.Format (formatProgram)+import Jikka.Core.Language.Expr+import Jikka.Core.Language.RewriteRules+import Jikka.Core.Parse (parseProgram)+import Test.Hspec++run' :: Program -> Either Error Program+run' = flip evalAlphaT 0 . applyRewriteRuleProgram' rule++parseProgram' :: [String] -> Program+parseProgram' = fromSuccess . flip evalAlphaT 100 . (TypeInfer.run <=< parseProgram . unlines)++spec :: Spec+spec = describe "run" $ do+  it "works" $ do+    let prog =+          parseProgram'+            [ "fun xs ->",+              "    minimum (map (fun x -> 3 + x) xs)"+            ]+    let expected =+          parseProgram'+            [ "fun xs ->",+              "    3 + minimum (map (fun x -> x) xs)"+            ]+    (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)+  it "reduces minimum-cons if non-nil" $ do+    let prog =+          parseProgram'+            [ "fun xs ->",+              "    assert xs /= nil",+              "    in minimum (cons 0 xs)"+            ]+    let expected =+          parseProgram'+            [ "fun xs ->",+              "    assert xs /= nil",+              "    in min 0 (minimum xs)"+            ]+    (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)+  it "reduces maximum-cons if non-nil" $ do+    let prog =+          parseProgram'+            [ "fun xs ->",+              "    assert 3 - len xs <= 0", -- Jikka.Core.Language.AssertedHint assumes exprs are converted with Jikka.Core.Convert.EqualitySolving.+              "    in maximum (cons 0 xs)"+            ]+    let expected =+          parseProgram'+            [ "fun xs ->",+              "    assert 3 - len xs <= 0",+              "    in max 0 (maximum xs)"+            ]+    (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)+  it "doesn't reduce minimum-cons if it may be nil" $ do+    let prog =+          parseProgram'+            [ "fun xs ->",+              "    minimum (cons 0 xs)"+            ]+    let expected =+          parseProgram'+            [ "fun xs ->",+              "    minimum (cons 0 xs)"+            ]+    (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
test/Jikka/Core/Convert/ConvexHullTrickSpec.hs view
@@ -86,7 +86,7 @@             ]     let base =           unlines-            [ "let ys$2: int list = snoc nil ((let ys: int list = nil in e ys - c[0]) + c[0])",+            [ "let ys$2: int list = snoc nil ((let ys$7: int list = nil in e ys$7 - 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)"
test/Jikka/Core/Convert/CumulativeSumSpec.hs view
@@ -33,11 +33,11 @@             ]     let expected =           parseProgram'-            [ "let rec f$0: int =",-              "    let a$1: int list = range 1000",-              "    in let n$2: int = 500",-              "    in let $4 = scanl (+) 0 a$1",-              "    in $4[n$2]",-              "in f$0"+            [ "let rec f: int =",+              "    let a: int list = range 1000",+              "    in let n: int = 500",+              "    in let $0 = scanl (+) 0 a",+              "    in $0[n]",+              "in f"             ]     (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
test/Jikka/Core/Convert/SegmentTreeSpec.hs view
@@ -34,13 +34,13 @@             ]     let expected =           parseProgram'-            [ "let a1$3: int list = range 1000",-              "in let rec f$4 (k$5: int): int list =",-              "    let a2$6 = a1$3",-              "    in (foldl (fun a2$7 i$8 ->",-              "        let $9 = 0 + segtree_getrange<int_plus> a2$7.1 0 (i$8 + 100)",-              "        in (a2$7.0[i$8 + 10 <- $9], segtree_setpoint<int_plus> a2$7.1 (i$8 + 10) $9)",-              "    ) (a2$6, segtree_init<int_plus> a2$6) (range k$5)).0",-              "in f$4 100"+            [ "let a1: int list = range 1000",+              "in let rec f (k: int): int list =",+              "    let a2$2 = a1",+              "    in (foldl (fun a2$0 i ->",+              "        let $1 = 0 + segtree_getrange<int_plus> a2$0.1 0 (i + 100)",+              "        in (a2$0.0[i + 10 <- $1], segtree_setpoint<int_plus> a2$0.1 (i + 10) $1)",+              "    ) (a2$2, segtree_init<int_plus> a2$2) (range k)).0",+              "in f 100"             ]     (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
test/Jikka/Core/Convert/ShortCutFusionSpec.hs view
@@ -23,8 +23,8 @@             LitInt' 100     run' prog `shouldBe` Right expected   it "squashes foldl-map combination" $ do-    let g = Lam2 "a" IntTy "i" IntTy (Plus' (Var "a") (Var "i"))-    let f = Lam "j" IntTy (Plus' (Var "j") Lit1)+    let g = Lam2 "a$4" IntTy "i$5" IntTy (Plus' (Var "a$4") (Var "i$5"))+    let f = Lam "j$6" IntTy (Plus' (Var "j$6") Lit1)     let prog =           ResultExpr $             Foldl' IntTy IntTy g Lit0 $
+ test/Jikka/Core/Convert/SortAbsSpec.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE OverloadedStrings #-}++module Jikka.Core.Convert.SortAbsSpec (spec) where++import Jikka.Common.Alpha+import Jikka.Common.Error+import Jikka.Core.Convert.SortAbs (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 . run++parseProgram' :: [String] -> Program+parseProgram' = fromSuccess . flip evalAlphaT 100 . (TypeInfer.run <=< parseProgram . unlines)++spec :: Spec+spec = describe "run" $ do+  it "works about sum" $ do+    let prog =+          parseProgram'+            [ "fun (a: int list) ->",+              "    sum (map (fun (a_i: int) ->",+              "        sum (map (fun (a_j: int) ->",+              "            abs (a_i - a_j)",+              "        ) a)",+              "    ) a)"+            ]+    let expected =+          parseProgram'+            [ "fun (a: int list) ->",+              "    let a$3 = sorted a",+              "    in sum (map (fun ($4: int) ->",+              "        let a_i = a$3[$4] in",+              "        sum (map (fun ($5: int) ->",+              "            let a_j = a$3[$5]",+              "            in a_i - a_j",+              "        ) (range $4))",+              "        + (let $6 = $4",+              "           in let a_j$7 = a$3[$6]",+              "           in 0)",+              "        + sum (map (fun ($8: int) ->",+              "            let a_j$9 = a$3[$8]",+              "            in a_j$9 - a_i",+              "        ) (range2 ($4 + 1) (len a$3)))",+              "    ) (range (len a$3)))"+            ]+    (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
test/Jikka/Core/Convert/TypeInferSpec.hs view
@@ -7,7 +7,7 @@  import Jikka.Common.Alpha import Jikka.Common.Error-import Jikka.Core.Convert.TypeInfer (run)+import Jikka.Core.Convert.TypeInfer (run, runExpr) import Jikka.Core.Language.BuiltinPatterns import Jikka.Core.Language.Expr import Test.Hspec@@ -15,97 +15,108 @@ run' :: Program -> Either Error Program run' = flip evalAlphaT 0 . run +runExpr' :: [(VarName, Type)] -> Expr -> Either Error Expr+runExpr' env = flip evalAlphaT 0 . runExpr env+ spec :: Spec-spec = describe "run" $ do-  it "works" $ do-    let prog =-          ResultExpr-            ( Let-                "x"-                (VarTy "t1")-                Lit0-                ( Let-                    "y"-                    (VarTy "t2")-                    (Plus' (Var "x") Lit1)-                    (Var "y")-                )-            )-    let expected =-          ResultExpr-            ( Let-                "x"-                IntTy-                Lit0-                ( Let-                    "y"-                    IntTy-                    (Plus' (Var "x") Lit1)-                    (Var "y")-                )-            )-    run' prog `shouldBe` Right expected-  it "works on let-rec" $ do-    let prog =-          ToplevelLetRec-            "f"-            [("x", VarTy "t1")]-            (VarTy "t2")-            (Var "x")-            (ResultExpr (App (Var "f") Lit0))-    let expected =-          ToplevelLetRec-            "f"-            [("x", IntTy)]-            IntTy-            (Var "x")-            (ResultExpr (App (Var "f") Lit0))-    run' prog `shouldBe` Right expected-  it "replaces undetermined types with 0-tuples" $ do-    let prog =-          ToplevelLetRec-            "f"-            [("x", VarTy "t1")]-            (VarTy "t2")-            (Var "x")-            (ResultExpr Lit0)-    let expected =-          ToplevelLetRec-            "f"-            [("x", TupleTy [])]-            (TupleTy [])-            (Var "x")-            (ResultExpr Lit0)-    run' prog `shouldBe` Right expected-  it "works on builtin functions" $ do-    let prog =-          ToplevelLetRec-            "solve"-            [("n", IntTy)]-            IntTy-            ( If'-                (VarTy "$0")-                (Equal' IntTy (Var "n") Lit0)-                Lit1-                ( Mult'-                    (Var "n")-                    (App (Var "solve") (Minus' (Var "n") Lit1))-                )-            )-            (ResultExpr (Var "solve"))-    let expected =-          ToplevelLetRec-            "solve"-            [("n", IntTy)]-            IntTy-            ( If'-                IntTy-                (Equal' IntTy (Var "n") Lit0)-                Lit1-                ( Mult'-                    (Var "n")-                    (App (Var "solve") (Minus' (Var "n") Lit1))-                )-            )-            (ResultExpr (Var "solve"))-    run' prog `shouldBe` Right expected+spec = do+  describe "run" $ do+    it "works" $ do+      let prog =+            ResultExpr+              ( Let+                  "x"+                  (VarTy "t1")+                  Lit0+                  ( Let+                      "y"+                      (VarTy "t2")+                      (Plus' (Var "x") Lit1)+                      (Var "y")+                  )+              )+      let expected =+            ResultExpr+              ( Let+                  "x"+                  IntTy+                  Lit0+                  ( Let+                      "y"+                      IntTy+                      (Plus' (Var "x") Lit1)+                      (Var "y")+                  )+              )+      run' prog `shouldBe` Right expected+    it "works on let-rec" $ do+      let prog =+            ToplevelLetRec+              "f"+              [("x", VarTy "t1")]+              (VarTy "t2")+              (Var "x")+              (ResultExpr (App (Var "f") Lit0))+      let expected =+            ToplevelLetRec+              "f"+              [("x", IntTy)]+              IntTy+              (Var "x")+              (ResultExpr (App (Var "f") Lit0))+      run' prog `shouldBe` Right expected+    it "replaces undetermined types with 0-tuples" $ do+      let prog =+            ToplevelLetRec+              "f"+              [("x", VarTy "t1")]+              (VarTy "t2")+              (Var "x")+              (ResultExpr Lit0)+      let expected =+            ToplevelLetRec+              "f"+              [("x", TupleTy [])]+              (TupleTy [])+              (Var "x")+              (ResultExpr Lit0)+      run' prog `shouldBe` Right expected+    it "works on builtin functions" $ do+      let prog =+            ToplevelLetRec+              "solve"+              [("n", IntTy)]+              IntTy+              ( If'+                  (VarTy "$0")+                  (Equal' IntTy (Var "n") Lit0)+                  Lit1+                  ( Mult'+                      (Var "n")+                      (App (Var "solve") (Minus' (Var "n") Lit1))+                  )+              )+              (ResultExpr (Var "solve"))+      let expected =+            ToplevelLetRec+              "solve"+              [("n", IntTy)]+              IntTy+              ( If'+                  IntTy+                  (Equal' IntTy (Var "n") Lit0)+                  Lit1+                  ( Mult'+                      (Var "n")+                      (App (Var "solve") (Minus' (Var "n") Lit1))+                  )+              )+              (ResultExpr (Var "solve"))+      run' prog `shouldBe` Right expected++  describe "runExpr" $ do+    it "works" $ do+      let e = Equal' (VarTy "t1") (Var "xs") (Nil' (VarTy "t2"))+      let env = [("xs", ListTy IntTy)]+      let expected = Equal' (ListTy IntTy) (Var "xs") (Nil' IntTy)+      runExpr' env e `shouldBe` Right expected
test/Jikka/Core/Convert/UnpackTupleSpec.hs view
@@ -25,7 +25,7 @@             App (Lam "x" (TupleTy ts) (Plus' (Proj' ts 0 (Var "x")) (Proj' ts 1 (Var "x")))) (uncurryApp (Tuple' ts) [LitInt' 0, LitInt' 1])     let expected =           ResultExpr $-            App2 (Lam2 "x$1" IntTy "x$2" IntTy (Plus' (Var "x$1") (Var "x$2"))) (LitInt' 0) (LitInt' 1)+            App2 (Lam2 "x$0" IntTy "x$1" IntTy (Plus' (Var "x$0") (Var "x$1"))) (LitInt' 0) (LitInt' 1)     run' prog `shouldBe` Right expected   it "works on foldl" $ do     let prog =@@ -33,5 +33,5 @@             Foldl' IntTy (TupleTy [IntTy]) (Lam2 "x" (TupleTy [IntTy]) "y" IntTy (uncurryApp (Tuple' [IntTy]) [Plus' (Proj' [IntTy] 0 (Var "x")) (Var "y")])) (uncurryApp (Tuple' [IntTy]) [LitInt' 0]) (Range1' (LitInt' 10))     let expected =           ResultExpr $-            uncurryApp (Tuple' [IntTy]) [Foldl' IntTy IntTy (Lam2 "x$0" IntTy "y$1" IntTy (Plus' (Var "x$0") (Var "y$1"))) (LitInt' 0) (Range1' (LitInt' 10))]+            uncurryApp (Tuple' [IntTy]) [Foldl' IntTy IntTy (Lam2 "x" IntTy "y" IntTy (Plus' (Var "x") (Var "y"))) (LitInt' 0) (Range1' (LitInt' 10))]     run' prog `shouldBe` Right expected
+ test/Jikka/Core/Language/AssertedHintSpec.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE OverloadedStrings #-}++module Jikka.Core.Language.AssertedHintSpec (spec) where++import Data.Maybe+import Jikka.Common.Alpha+import Jikka.Common.Error+import qualified Jikka.Core.Convert.ArithmeticExpr as ArithmeticExpr+import qualified Jikka.Core.Convert.EqualitySolving as EqualitySolving+import qualified Jikka.Core.Convert.TypeInfer as TypeInfer+import Jikka.Core.Language.ArithmeticExpr+import Jikka.Core.Language.AssertedHint+import Jikka.Core.Language.Expr+import Jikka.Core.Language.RewriteRules+import Jikka.Core.Parse (parseExpr)+import Test.Hspec++parseExpr' :: [(VarName, Type)] -> String -> Expr+parseExpr' env e = fromSuccess . flip evalAlphaT 100 $ do+  e <- parseExpr e+  e <- TypeInfer.runExpr env e+  e <- fromMaybe e <$> applyRewriteRule EqualitySolving.rule (makeRewriteEnvironmentFromTypeEnv env) e+  ArithmeticExpr.runExpr env e++spec :: Spec+spec = do+  describe "parseHints" $ do+    it "works on n == 3" $ do+      let e = parseExpr' [("n", IntTy)] "n == 3"+      let expected =+            [ ("n", EqualHint (integerArithmeticExpr 3))+            ]+      parseHints e `shouldBe` expected+    it "works on length xs == 3" $ do+      let e = parseExpr' [("xs", ListTy IntTy)] "len xs == 3"+      let expected =+            [ ("xs", LengthHint IntTy (EqualHint (integerArithmeticExpr 3)))+            ]+      parseHints e `shouldBe` expected+    it "works on length xs >= 3" $ do+      let e = parseExpr' [("xs", ListTy IntTy)] "len xs >= 3"+      let expected =+            [ ("xs", LengthHint IntTy (BoundHint (Just (integerArithmeticExpr 3)) Nothing))+            ]+      parseHints e `shouldBe` expected+    it "works on xs /= nil" $ do+      let e = parseExpr' [("xs", ListTy IntTy)] "xs /= nil"+      let expected =+            [ ("xs", LengthHint IntTy (BoundHint (Just (integerArithmeticExpr 1)) Nothing))+            ]+      parseHints e `shouldBe` expected+    it "works on length 0 <= xs - 3" $ do+      let e = parseExpr' [("xs", ListTy IntTy)] "0 <= len xs - 3"+      let expected =+            [ ("xs", LengthHint IntTy (BoundHint (Just (integerArithmeticExpr 3)) Nothing))+            ]+      parseHints e `shouldBe` expected++  describe "lowerBoundWithHints" $ do+    it "works on length n == 3" $ do+      let hints = [("n", EqualHint (integerArithmeticExpr 3))]+      let e = Var "n"+      let expected = Just 3+      lowerBoundWithHints hints e `shouldBe` expected++  describe "upperBoundWithHints" $ do+    it "works on length n == 3" $ do+      let hints = [("n", EqualHint (integerArithmeticExpr 3))]+      let e = Var "n"+      let expected = Just 4+      upperBoundWithHints hints e `shouldBe` expected++  describe "nullWithHints" $ do+    it "works on length xs >= 3" $ do+      let hints = [("xs", LengthHint IntTy (BoundHint (Just (integerArithmeticExpr 3)) Nothing))]+      let e = Var "xs"+      let expected = Just False+      nullWithHints hints e `shouldBe` expected+    it "works on length xs == 0" $ do+      let hints = [("xs", LengthHint IntTy (EqualHint (integerArithmeticExpr 0)))]+      let e = Var "xs"+      let expected = Just True+      nullWithHints hints e `shouldBe` expected+    it "works on length xs == 1" $ do+      let hints = [("xs", LengthHint IntTy (EqualHint (integerArithmeticExpr 1)))]+      let e = Var "xs"+      let expected = Just False+      nullWithHints hints e `shouldBe` expected+    it "works on length xs < 3" $ do+      let hints = [("xs", LengthHint IntTy (BoundHint Nothing (Just (integerArithmeticExpr 3))))]+      let e = Var "xs"+      let expected = Nothing+      nullWithHints hints e `shouldBe` expected
test/Jikka/Core/ParseSpec.hs view
@@ -16,45 +16,55 @@ run' :: String -> Either Error Program run' prog = evalAlphaT (run "<data>" (T.pack prog)) 100 +parseExpr' :: String -> Either Error Expr+parseExpr' e = evalAlphaT (parseExpr e) 100+ spec :: Spec-spec = describe "run" $ do-  it "works" $ do-    let prog =-          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",-              "in",+spec = do+  describe "run" $ do+    it "works" $ do+      let prog =+            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",+                "in",+                "solve$0"+              ]+      let expected =+            ToplevelLetRec               "solve$0"-            ]-    let expected =-          ToplevelLetRec-            "solve$0"-            [("n$1", IntTy)]-            IntTy-            ( Let-                "xs$2"-                (ListTy IntTy)-                ( Map'-                    (VarTy "$100")-                    (VarTy "$101")-                    ( Lam-                        "i$3"-                        IntTy-                        (Mult' (Var "i$3") (Var "i$3"))-                    )-                    (Range1' (Var "n$1"))-                )-                (Sum' (Var "xs$2"))-            )-            (ResultExpr (Var "solve$0"))-    run' prog `shouldBe` Right expected-  it "inserts new type variables" $ do-    let prog = "a[0 <- b][0]"-    let expected =-          ResultExpr-            (At' (VarTy "$100") (SetAt' (VarTy "$101") (Var "a") (LitInt' 0) (Var "b")) (LitInt' 0))-    run' prog `shouldBe` Right expected+              [("n$1", IntTy)]+              IntTy+              ( Let+                  "xs$2"+                  (ListTy IntTy)+                  ( Map'+                      (VarTy "$100")+                      (VarTy "$101")+                      ( Lam+                          "i$3"+                          IntTy+                          (Mult' (Var "i$3") (Var "i$3"))+                      )+                      (Range1' (Var "n$1"))+                  )+                  (Sum' (Var "xs$2"))+              )+              (ResultExpr (Var "solve$0"))+      run' prog `shouldBe` Right expected+    it "inserts new type variables" $ do+      let prog = "a[0 <- b][0]"+      let expected =+            ResultExpr+              (At' (VarTy "$100") (SetAt' (VarTy "$101") (Var "a") (LitInt' 0) (Var "b")) (LitInt' 0))+      run' prog `shouldBe` Right expected++  describe "parseExpr" $ do+    it "works" $ do+      let e = "n == 3"+      let expected = Equal' (VarTy "$100") (Var "n") (LitInt' 3)+      parseExpr' e `shouldBe` Right expected