diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,10 +1,26 @@
# Changelog for Jikka
+## 2021-09-04: v5.5.0.0
+
+Features:
+
+- Now Jikka is available on Web:
+- 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:
- 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
diff --git a/Jikka.cabal b/Jikka.cabal
--- a/Jikka.cabal
+++ b/Jikka.cabal
@@ -5,7 +5,7 @@
-- see: https://github.com/sol/hpack
name: Jikka
-version: 5.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
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
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -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 .
+
## 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:
diff --git a/app/doctests.hs b/app/doctests.hs
new file mode 100644
--- /dev/null
+++ b/app/doctests.hs
@@ -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/"
+ ]
diff --git a/doctests.hs b/doctests.hs
deleted file mode 100644
--- a/doctests.hs
+++ /dev/null
@@ -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/"
- ]
diff --git a/src/Jikka/CPlusPlus/Convert/BundleRuntime.hs b/src/Jikka/CPlusPlus/Convert/BundleRuntime.hs
--- a/src/Jikka/CPlusPlus/Convert/BundleRuntime.hs
+++ b/src/Jikka/CPlusPlus/Convert/BundleRuntime.hs
@@ -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 .
+#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)
diff --git a/src/Jikka/CPlusPlus/Format.hs b/src/Jikka/CPlusPlus/Format.hs
--- a/src/Jikka/CPlusPlus/Format.hs
+++ b/src/Jikka/CPlusPlus/Format.hs
@@ -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
diff --git a/src/Jikka/Common/FileEmbed.hs b/src/Jikka/Common/FileEmbed.hs
--- a/src/Jikka/Common/FileEmbed.hs
+++ b/src/Jikka/Common/FileEmbed.hs
@@ -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)]|]
diff --git a/src/Jikka/Common/IOFormat.hs b/src/Jikka/Common/IOFormat.hs
--- a/src/Jikka/Common/IOFormat.hs
+++ b/src/Jikka/Common/IOFormat.hs
@@ -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
diff --git a/src/Jikka/Core/Convert.hs b/src/Jikka/Core/Convert.hs
--- a/src/Jikka/Core/Convert.hs
+++ b/src/Jikka/Core/Convert.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/ANormal.hs b/src/Jikka/Core/Convert/ANormal.hs
--- a/src/Jikka/Core/Convert/ANormal.hs
+++ b/src/Jikka/Core/Convert/ANormal.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/Alpha.hs b/src/Jikka/Core/Convert/Alpha.hs
--- a/src/Jikka/Core/Convert/Alpha.hs
+++ b/src/Jikka/Core/Convert/Alpha.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/ArithmeticExpr.hs b/src/Jikka/Core/Convert/ArithmeticExpr.hs
--- a/src/Jikka/Core/Convert/ArithmeticExpr.hs
+++ b/src/Jikka/Core/Convert/ArithmeticExpr.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/Beta.hs b/src/Jikka/Core/Convert/Beta.hs
--- a/src/Jikka/Core/Convert/Beta.hs
+++ b/src/Jikka/Core/Convert/Beta.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/BubbleLet.hs b/src/Jikka/Core/Convert/BubbleLet.hs
--- a/src/Jikka/Core/Convert/BubbleLet.hs
+++ b/src/Jikka/Core/Convert/BubbleLet.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/CloseAll.hs b/src/Jikka/Core/Convert/CloseAll.hs
--- a/src/Jikka/Core/Convert/CloseAll.hs
+++ b/src/Jikka/Core/Convert/CloseAll.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/CloseMin.hs b/src/Jikka/Core/Convert/CloseMin.hs
--- a/src/Jikka/Core/Convert/CloseMin.hs
+++ b/src/Jikka/Core/Convert/CloseMin.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/CloseSum.hs b/src/Jikka/Core/Convert/CloseSum.hs
--- a/src/Jikka/Core/Convert/CloseSum.hs
+++ b/src/Jikka/Core/Convert/CloseSum.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/ConstantFolding.hs b/src/Jikka/Core/Convert/ConstantFolding.hs
--- a/src/Jikka/Core/Convert/ConstantFolding.hs
+++ b/src/Jikka/Core/Convert/ConstantFolding.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/ConstantPropagation.hs b/src/Jikka/Core/Convert/ConstantPropagation.hs
--- a/src/Jikka/Core/Convert/ConstantPropagation.hs
+++ b/src/Jikka/Core/Convert/ConstantPropagation.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/ConvexHullTrick.hs b/src/Jikka/Core/Convert/ConvexHullTrick.hs
--- a/src/Jikka/Core/Convert/ConvexHullTrick.hs
+++ b/src/Jikka/Core/Convert/ConvexHullTrick.hs
@@ -28,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
diff --git a/src/Jikka/Core/Convert/CumulativeSum.hs b/src/Jikka/Core/Convert/CumulativeSum.hs
--- a/src/Jikka/Core/Convert/CumulativeSum.hs
+++ b/src/Jikka/Core/Convert/CumulativeSum.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/EqualitySolving.hs b/src/Jikka/Core/Convert/EqualitySolving.hs
--- a/src/Jikka/Core/Convert/EqualitySolving.hs
+++ b/src/Jikka/Core/Convert/EqualitySolving.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/Eta.hs b/src/Jikka/Core/Convert/Eta.hs
--- a/src/Jikka/Core/Convert/Eta.hs
+++ b/src/Jikka/Core/Convert/Eta.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/KubaruToMorau.hs b/src/Jikka/Core/Convert/KubaruToMorau.hs
--- a/src/Jikka/Core/Convert/KubaruToMorau.hs
+++ b/src/Jikka/Core/Convert/KubaruToMorau.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/MakeScanl.hs b/src/Jikka/Core/Convert/MakeScanl.hs
--- a/src/Jikka/Core/Convert/MakeScanl.hs
+++ b/src/Jikka/Core/Convert/MakeScanl.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/MatrixExponentiation.hs b/src/Jikka/Core/Convert/MatrixExponentiation.hs
--- a/src/Jikka/Core/Convert/MatrixExponentiation.hs
+++ b/src/Jikka/Core/Convert/MatrixExponentiation.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/PropagateMod.hs b/src/Jikka/Core/Convert/PropagateMod.hs
--- a/src/Jikka/Core/Convert/PropagateMod.hs
+++ b/src/Jikka/Core/Convert/PropagateMod.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/RemoveUnusedVars.hs b/src/Jikka/Core/Convert/RemoveUnusedVars.hs
--- a/src/Jikka/Core/Convert/RemoveUnusedVars.hs
+++ b/src/Jikka/Core/Convert/RemoveUnusedVars.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/SegmentTree.hs b/src/Jikka/Core/Convert/SegmentTree.hs
--- a/src/Jikka/Core/Convert/SegmentTree.hs
+++ b/src/Jikka/Core/Convert/SegmentTree.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/ShortCutFusion.hs b/src/Jikka/Core/Convert/ShortCutFusion.hs
--- a/src/Jikka/Core/Convert/ShortCutFusion.hs
+++ b/src/Jikka/Core/Convert/ShortCutFusion.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/SortAbs.hs b/src/Jikka/Core/Convert/SortAbs.hs
new file mode 100644
--- /dev/null
+++ b/src/Jikka/Core/Convert/SortAbs.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/SpecializeFoldl.hs b/src/Jikka/Core/Convert/SpecializeFoldl.hs
--- a/src/Jikka/Core/Convert/SpecializeFoldl.hs
+++ b/src/Jikka/Core/Convert/SpecializeFoldl.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/TrivialLetElimination.hs b/src/Jikka/Core/Convert/TrivialLetElimination.hs
--- a/src/Jikka/Core/Convert/TrivialLetElimination.hs
+++ b/src/Jikka/Core/Convert/TrivialLetElimination.hs
@@ -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
diff --git a/src/Jikka/Core/Convert/TypeInfer.hs b/src/Jikka/Core/Convert/TypeInfer.hs
--- a/src/Jikka/Core/Convert/TypeInfer.hs
+++ b/src/Jikka/Core/Convert/TypeInfer.hs
@@ -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)
diff --git a/src/Jikka/Core/Convert/UnpackTuple.hs b/src/Jikka/Core/Convert/UnpackTuple.hs
--- a/src/Jikka/Core/Convert/UnpackTuple.hs
+++ b/src/Jikka/Core/Convert/UnpackTuple.hs
@@ -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
diff --git a/src/Jikka/Core/Language/ArithmeticExpr.hs b/src/Jikka/Core/Language/ArithmeticExpr.hs
--- a/src/Jikka/Core/Language/ArithmeticExpr.hs
+++ b/src/Jikka/Core/Language/ArithmeticExpr.hs
@@ -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
diff --git a/src/Jikka/Core/Language/AssertedHint.hs b/src/Jikka/Core/Language/AssertedHint.hs
new file mode 100644
--- /dev/null
+++ b/src/Jikka/Core/Language/AssertedHint.hs
@@ -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
diff --git a/src/Jikka/Core/Language/Lint.hs b/src/Jikka/Core/Language/Lint.hs
--- a/src/Jikka/Core/Language/Lint.hs
+++ b/src/Jikka/Core/Language/Lint.hs
@@ -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
diff --git a/src/Jikka/Core/Language/NameCheck.hs b/src/Jikka/Core/Language/NameCheck.hs
new file mode 100644
--- /dev/null
+++ b/src/Jikka/Core/Language/NameCheck.hs
@@ -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) []
diff --git a/src/Jikka/Core/Language/QuasiRules.hs b/src/Jikka/Core/Language/QuasiRules.hs
--- a/src/Jikka/Core/Language/QuasiRules.hs
+++ b/src/Jikka/Core/Language/QuasiRules.hs
@@ -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
|]
diff --git a/src/Jikka/Core/Language/RewriteRules.hs b/src/Jikka/Core/Language/RewriteRules.hs
--- a/src/Jikka/Core/Language/RewriteRules.hs
+++ b/src/Jikka/Core/Language/RewriteRules.hs
@@ -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
diff --git a/src/Jikka/Core/Language/TypeCheck.hs b/src/Jikka/Core/Language/TypeCheck.hs
--- a/src/Jikka/Core/Language/TypeCheck.hs
+++ b/src/Jikka/Core/Language/TypeCheck.hs
@@ -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'
diff --git a/src/Jikka/Core/Language/Util.hs b/src/Jikka/Core/Language/Util.hs
--- a/src/Jikka/Core/Language/Util.hs
+++ b/src/Jikka/Core/Language/Util.hs
@@ -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
diff --git a/src/Jikka/Core/Parse/Happy.y b/src/Jikka/Core/Parse/Happy.y
--- a/src/Jikka/Core/Parse/Happy.y
+++ b/src/Jikka/Core/Parse/Happy.y
@@ -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
diff --git a/test/Jikka/CPlusPlus/FormatSpec.hs b/test/Jikka/CPlusPlus/FormatSpec.hs
--- a/test/Jikka/CPlusPlus/FormatSpec.hs
+++ b/test/Jikka/CPlusPlus/FormatSpec.hs
@@ -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 h) {",
- " int64_t x = 0;",
+ " int64_t x = 0ll;",
" for (int32_t i = 2; i < n; ++ i) {",
" x += h[i - 2];",
" }",
diff --git a/test/Jikka/Core/Convert/ANormalSpec.hs b/test/Jikka/Core/Convert/ANormalSpec.hs
--- a/test/Jikka/Core/Convert/ANormalSpec.hs
+++ b/test/Jikka/Core/Convert/ANormalSpec.hs
@@ -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
diff --git a/test/Jikka/Core/Convert/AlphaSpec.hs b/test/Jikka/Core/Convert/AlphaSpec.hs
--- a/test/Jikka/Core/Convert/AlphaSpec.hs
+++ b/test/Jikka/Core/Convert/AlphaSpec.hs
@@ -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
diff --git a/test/Jikka/Core/Convert/BetaSpec.hs b/test/Jikka/Core/Convert/BetaSpec.hs
--- a/test/Jikka/Core/Convert/BetaSpec.hs
+++ b/test/Jikka/Core/Convert/BetaSpec.hs
@@ -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
diff --git a/test/Jikka/Core/Convert/CloseMinSpec.hs b/test/Jikka/Core/Convert/CloseMinSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Jikka/Core/Convert/CloseMinSpec.hs
@@ -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)
diff --git a/test/Jikka/Core/Convert/ConvexHullTrickSpec.hs b/test/Jikka/Core/Convert/ConvexHullTrickSpec.hs
--- a/test/Jikka/Core/Convert/ConvexHullTrickSpec.hs
+++ b/test/Jikka/Core/Convert/ConvexHullTrickSpec.hs
@@ -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)"
diff --git a/test/Jikka/Core/Convert/CumulativeSumSpec.hs b/test/Jikka/Core/Convert/CumulativeSumSpec.hs
--- a/test/Jikka/Core/Convert/CumulativeSumSpec.hs
+++ b/test/Jikka/Core/Convert/CumulativeSumSpec.hs
@@ -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)
diff --git a/test/Jikka/Core/Convert/SegmentTreeSpec.hs b/test/Jikka/Core/Convert/SegmentTreeSpec.hs
--- a/test/Jikka/Core/Convert/SegmentTreeSpec.hs
+++ b/test/Jikka/Core/Convert/SegmentTreeSpec.hs
@@ -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 a2$7.1 0 (i$8 + 100)",
- " in (a2$7.0[i$8 + 10 <- $9], segtree_setpoint a2$7.1 (i$8 + 10) $9)",
- " ) (a2$6, segtree_init 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 a2$0.1 0 (i + 100)",
+ " in (a2$0.0[i + 10 <- $1], segtree_setpoint a2$0.1 (i + 10) $1)",
+ " ) (a2$2, segtree_init a2$2) (range k)).0",
+ "in f 100"
]
(formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
diff --git a/test/Jikka/Core/Convert/ShortCutFusionSpec.hs b/test/Jikka/Core/Convert/ShortCutFusionSpec.hs
--- a/test/Jikka/Core/Convert/ShortCutFusionSpec.hs
+++ b/test/Jikka/Core/Convert/ShortCutFusionSpec.hs
@@ -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 $
diff --git a/test/Jikka/Core/Convert/SortAbsSpec.hs b/test/Jikka/Core/Convert/SortAbsSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Jikka/Core/Convert/SortAbsSpec.hs
@@ -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)
diff --git a/test/Jikka/Core/Convert/TypeInferSpec.hs b/test/Jikka/Core/Convert/TypeInferSpec.hs
--- a/test/Jikka/Core/Convert/TypeInferSpec.hs
+++ b/test/Jikka/Core/Convert/TypeInferSpec.hs
@@ -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
diff --git a/test/Jikka/Core/Convert/UnpackTupleSpec.hs b/test/Jikka/Core/Convert/UnpackTupleSpec.hs
--- a/test/Jikka/Core/Convert/UnpackTupleSpec.hs
+++ b/test/Jikka/Core/Convert/UnpackTupleSpec.hs
@@ -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
diff --git a/test/Jikka/Core/Language/AssertedHintSpec.hs b/test/Jikka/Core/Language/AssertedHintSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Jikka/Core/Language/AssertedHintSpec.hs
@@ -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
diff --git a/test/Jikka/Core/ParseSpec.hs b/test/Jikka/Core/ParseSpec.hs
--- a/test/Jikka/Core/ParseSpec.hs
+++ b/test/Jikka/Core/ParseSpec.hs
@@ -16,45 +16,55 @@
run' :: String -> Either Error Program
run' prog = evalAlphaT (run "" (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