diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,11 @@
# Changelog for Jikka
+## 2021-08-24: v5.4.0.0
+
+- More and more tests are added and some bugs are removed.
+- An online judge is published:
+ - This judge contains example problems which Jikka can/will be able to solve.
+
## 2021-08-16: v5.3.0.0
Many bugs are removed.
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.3.0.0
+version: 5.4.0.0
synopsis: A transpiler from Python to C++ for competitive programming
description: Please see the README on GitHub at
category: Compilers/Interpreters
@@ -85,7 +85,6 @@
Jikka.Core.Convert.SegmentTree
Jikka.Core.Convert.ShortCutFusion
Jikka.Core.Convert.SpecializeFoldl
- Jikka.Core.Convert.StrengthReduction
Jikka.Core.Convert.TrivialLetElimination
Jikka.Core.Convert.TypeInfer
Jikka.Core.Convert.UnpackTuple
@@ -98,6 +97,7 @@
Jikka.Core.Language.FreeVars
Jikka.Core.Language.LambdaPatterns
Jikka.Core.Language.Lint
+ Jikka.Core.Language.ModuloExpr
Jikka.Core.Language.QuasiRules
Jikka.Core.Language.RewriteRules
Jikka.Core.Language.Runtime
@@ -238,11 +238,14 @@
Jikka.Core.Convert.ConstantFoldingSpec
Jikka.Core.Convert.ConstantPropagationSpec
Jikka.Core.Convert.ConvexHullTrickSpec
+ Jikka.Core.Convert.CumulativeSumSpec
Jikka.Core.Convert.EtaSpec
+ Jikka.Core.Convert.KubaruToMorauSpec
Jikka.Core.Convert.MakeScanlSpec
Jikka.Core.Convert.MatrixExponentiationSpec
Jikka.Core.Convert.PropagateModSpec
Jikka.Core.Convert.RemoveUnusedVarsSpec
+ Jikka.Core.Convert.SegmentTreeSpec
Jikka.Core.Convert.ShortCutFusionSpec
Jikka.Core.Convert.SpecializeFoldlSpec
Jikka.Core.Convert.TrivialLetEliminationSpec
diff --git a/runtime/include/jikka/divmod.hpp b/runtime/include/jikka/divmod.hpp
--- a/runtime/include/jikka/divmod.hpp
+++ b/runtime/include/jikka/divmod.hpp
@@ -31,6 +31,12 @@
return n - ceildiv(n, d) * d;
}
+inline int64_t justdiv(int64_t n, int64_t d) {
+ assert(d != 0);
+ assert(n % d == 0);
+ return n / d;
+}
+
} // namespace jikka
#endif // JIKKA_DIVMOD_HPP
diff --git a/src/Jikka/CPlusPlus/Convert/FromCore.hs b/src/Jikka/CPlusPlus/Convert/FromCore.hs
--- a/src/Jikka/CPlusPlus/Convert/FromCore.hs
+++ b/src/Jikka/CPlusPlus/Convert/FromCore.hs
@@ -268,6 +268,7 @@
X.FloorMod -> go02 $ \e1 e2 -> Y.Call (Y.Function "jikka::floormod" []) [e1, e2]
X.CeilDiv -> go02 $ \e1 e2 -> Y.Call (Y.Function "jikka::ceildiv" []) [e1, e2]
X.CeilMod -> go02 $ \e1 e2 -> Y.Call (Y.Function "jikka::ceilmod" []) [e1, e2]
+ X.JustDiv -> go02 $ \e1 e2 -> Y.Call (Y.Function "jikka::justdiv" []) [e1, e2]
X.Pow -> go02 $ \e1 e2 -> Y.Call (Y.Function "jikka::notmod::pow" []) [e1, e2]
-- advanced arithmetical functions
X.Abs -> go01 $ \e -> Y.Call (Y.Function "std::abs" []) [e]
diff --git a/src/Jikka/Common/Parse/JoinLines.hs b/src/Jikka/Common/Parse/JoinLines.hs
--- a/src/Jikka/Common/Parse/JoinLines.hs
+++ b/src/Jikka/Common/Parse/JoinLines.hs
@@ -4,11 +4,18 @@
module Jikka.Common.Parse.JoinLines
( joinLinesWithParens,
removeEmptyLines,
+ putTrailingNewline,
)
where
import Jikka.Common.Error
import Jikka.Common.Location
+
+putTrailingNewline :: Eq a => a -> [a] -> [a]
+putTrailingNewline newline tokens =
+ if not (null tokens) && last tokens /= newline
+ then tokens ++ [newline]
+ else tokens
joinLinesWithParens :: forall m a. (MonadError Error m, Show a) => (a -> Bool) -> (a -> Bool) -> (a -> Bool) -> [WithLoc a] -> m [WithLoc a]
joinLinesWithParens isOpen isClose isNewline = go []
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
@@ -38,7 +38,6 @@
import qualified Jikka.Core.Convert.SegmentTree as SegmentTree
import qualified Jikka.Core.Convert.ShortCutFusion as ShortCutFusion
import qualified Jikka.Core.Convert.SpecializeFoldl as SpecializeFoldl
-import qualified Jikka.Core.Convert.StrengthReduction as StrengthReduction
import qualified Jikka.Core.Convert.TrivialLetElimination as TrivialLetElimination
import qualified Jikka.Core.Convert.TypeInfer as TypeInfer
import qualified Jikka.Core.Convert.UnpackTuple as UnpackTuple
@@ -65,7 +64,6 @@
prog <- BubbleLet.run prog
prog <- ArithmeticExpr.run prog
prog <- ConvexHullTrick.run prog
- prog <- StrengthReduction.run prog
Eta.run prog
run' :: (MonadAlpha m, MonadError Error m) => Program -> m Program
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
@@ -27,7 +27,6 @@
import Jikka.Core.Language.Lint
import Jikka.Core.Language.QuasiRules
import Jikka.Core.Language.RewriteRules
-import Jikka.Core.Language.Util
reduceAll :: MonadAlpha m => RewriteRule m
reduceAll =
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
@@ -1,5 +1,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ViewPatterns #-}
-- |
-- Module : Jikka.Core.Convert.CloseMin
@@ -27,62 +29,106 @@
import Jikka.Core.Language.BuiltinPatterns
import Jikka.Core.Language.Expr
import Jikka.Core.Language.FreeVars
+import Jikka.Core.Language.LambdaPatterns
import Jikka.Core.Language.Lint
+import Jikka.Core.Language.QuasiRules
import Jikka.Core.Language.RewriteRules
-reduceMin :: Monad m => RewriteRule m
-reduceMin = simpleRewriteRule "reduceMin" $ \case
- -- list build functions
- Min1' t (Nil' _) -> Just $ Bottom' t "no minimum in empty list"
- Min1' _ (Cons' _ e (Nil' _)) -> Just e
- Min1' t (Cons' _ e (Cons' _ e' es)) -> Just $ Min2' t e (Min1' t (Cons' t e' es))
- -- list map functions
- Min1' t (Reversed' _ es) -> Just $ Min1' t es
- Min1' t (Cons' _ e (Reversed' _ es)) -> Just $ Min1' t (Cons' t e es)
- Min1' t (Sorted' _ es) -> Just $ Min1' t es
- Min1' t (Cons' _ e (Sorted' _ es)) -> Just $ Min1' t (Cons' t e es)
- Min1' t (Map' t1 t2 f es) -> case f of
- Lam x _ e | x `isUnusedVar` e -> Just e
- Lam x _ (Min2' _ e1 e2) -> Just $ Min2' t (Min1' t (Map' t1 t2 (Lam x t e1) es)) (Min1' t (Map' t1 t2 (Lam x t e2) es))
- Lam x _ (Negate' e) -> Just $ Negate' (Max1' t (Map' t1 t2 (Lam x IntTy e) es))
- Lam x _ (Plus' e1 e2) | x `isUnusedVar` e1 -> Just $ Plus' e1 (Min1' t (Map' t1 t2 (Lam x IntTy e2) es))
- Lam x _ (Plus' e1 e2) | x `isUnusedVar` e2 -> Just $ Plus' (Min1' t (Map' t1 t2 (Lam x IntTy e1) es)) e2
- _ -> Nothing
- Min1' t (Cons' _ e0 (Map' t1 t2 f xs)) -> case f of
- Lam x _ e | x `isUnusedVar` e -> Just $ If' t (Equal' IntTy (Len' t xs) Lit0) e0 (Min2' t e0 e)
- Lam x _ (Min2' _ e1 e2) -> Just $ Min2' t (Min1' t (Cons' t e0 (Map' t1 t2 (Lam x t e1) xs))) (Min1' t (Cons' t e0 (Map' t1 t2 (Lam x t e2) xs)))
- Lam x _ (Negate' e) -> Just $ Negate' (Max1' t (Cons' t (Negate' e0) (Map' t1 t2 (Lam x IntTy e) xs)))
- Lam x _ (Plus' e1 e2) | x `isUnusedVar` e1 -> Just $ Plus' e1 (Min1' t (Cons' t (Minus' e0 e1) (Map' t1 t2 (Lam x IntTy e2) xs)))
- Lam x _ (Plus' e1 e2) | x `isUnusedVar` e2 -> Just $ Plus' (Min1' t (Cons' t (Minus' e0 e2) (Map' t1 t2 (Lam x IntTy e1) xs))) e2
- _ -> Nothing
- _ -> Nothing
+reduceMin :: MonadAlpha m => RewriteRule m
+reduceMin =
+ mconcat
+ [ -- 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 |],
+ -- list map functions
+ [r| "minimum/reversed" forall xs. minimum (reversed xs) = minimum xs |],
+ [r| "minimum/cons/reversed" forall x xs. minimum (cons x (reversed xs)) = minimum (cons x xs) |],
+ [r| "minimum/sorted" forall xs. minimum (sorted xs) = minimum xs |],
+ [r| "minimum/cons/sorted" forall x xs. minimum (cons x (sorted xs)) = minimum (cons x xs) |],
+ makeRewriteRule "minimum/map/const" $ \_ -> \case
+ Min1' _ (Map' _ _ (LamConst _ e) _) -> return $ Just e
+ _ -> return Nothing,
+ [r| "minimum/map/min" forall e1 e2 xs. minimum (map (fun x -> min e1 e2) xs) = min (minimum (map (fun x -> e1) xs)) (minimum (map (fun x -> e2) xs)) |],
+ [r| "minimum/map/negate" forall e xs. minimum (map (fun x -> - e) xs) = - (maximum (map (fun x -> e) xs)) |],
+ makeRewriteRule "minimum/map/plus" $ \_ -> \case
+ Min1' _ (Map' t1 _ (Lam x _ (Plus' k e)) xs) | x `isUnusedVar` k -> return . Just $ Plus' k (Min1' IntTy (Map' t1 IntTy (Lam x t1 e) xs))
+ _ -> return Nothing,
+ makeRewriteRule "minimum/map/plus'" $ \_ -> \case
+ Min1' _ (Map' t1 _ (Lam x _ (Plus' e k)) xs) | x `isUnusedVar` k -> return . Just $ Plus' k (Min1' IntTy (Map' t1 IntTy (Lam x t1 e) xs))
+ _ -> return Nothing,
+ makeRewriteRule "minimum/map/minus" $ \_ -> \case
+ Min1' _ (Map' t1 _ (Lam x _ (Minus' k e)) xs) | x `isUnusedVar` k -> return . Just $ Minus' k (Max1' IntTy (Map' t1 IntTy (Lam x t1 e) xs))
+ _ -> return Nothing,
+ makeRewriteRule "minimum/map/minus'" $ \_ -> \case
+ Min1' _ (Map' t1 _ (Lam x _ (Minus' e k)) xs) | x `isUnusedVar` k -> return . Just $ Minus' k (Min1' IntTy (Map' t1 IntTy (Lam x t1 e) xs))
+ _ -> return Nothing,
+ makeRewriteRule "minimum/cons/map/const" $ \_ -> \case
+ Min1' t (Cons' _ x (Map' _ _ (LamConst _ e) _)) -> return . Just $ Min2' t x e
+ _ -> return Nothing,
+ [r| "minimum/cons/map/min" forall e0 e1 e2 xs. minimum (cons e0 (map (fun x -> min e1 e2) xs)) = min (minimum (cons e0 (map (fun x -> e1) xs))) (minimum (cons x (map (fun x -> e2) xs))) |],
+ [r| "minimum/cons/map/negate" forall e0 e xs. minimum (cons e0 (map (fun x -> - e) xs)) = - (maximum (cons (- e0) (map (fun x -> e) xs))) |],
+ makeRewriteRule "minimum/cons/map/plus" $ \_ -> \case
+ Min1' _ (Cons' _ e0 (Map' t1 _ (Lam x _ (Plus' k e)) xs)) | x `isUnusedVar` k -> return . Just $ Plus' k (Min1' IntTy (Cons' IntTy (Minus' e0 k) (Map' t1 IntTy (Lam x t1 e) xs)))
+ _ -> return Nothing,
+ makeRewriteRule "minimum/cons/map/plus'" $ \_ -> \case
+ Min1' _ (Cons' _ e0 (Map' t1 _ (Lam x _ (Plus' e k)) xs)) | x `isUnusedVar` k -> return . Just $ Plus' k (Min1' IntTy (Cons' IntTy (Minus' e0 k) (Map' t1 IntTy (Lam x t1 e) xs)))
+ _ -> return Nothing,
+ makeRewriteRule "minimum/cons/map/minus" $ \_ -> \case
+ Min1' _ (Cons' _ e0 (Map' t1 _ (Lam x _ (Minus' k e)) xs)) | x `isUnusedVar` k -> return . Just $ Minus' k (Max1' IntTy (Cons' IntTy (Minus' k e0) (Map' t1 IntTy (Lam x t1 e) xs)))
+ _ -> return Nothing,
+ makeRewriteRule "minimum/cons/map/minus'" $ \_ -> \case
+ Min1' _ (Cons' _ e0 (Map' t1 _ (Lam x _ (Minus' e k)) xs)) | x `isUnusedVar` k -> return . Just $ Minus' (Min1' IntTy (Cons' IntTy (Plus' e0 k) (Map' t1 IntTy (Lam x t1 e) xs))) k
+ _ -> return Nothing
+ ]
-reduceMax :: Monad m => RewriteRule m
-reduceMax = simpleRewriteRule "reduceMax" $ \case
- -- list build functions
- Max1' t (Nil' _) -> Just $ Bottom' t "no maximum in empty list"
- Max1' _ (Cons' _ e (Nil' _)) -> Just e
- Max1' t (Cons' _ e (Cons' _ e' es)) -> Just $ Max2' t e (Max1' t (Cons' t e' es))
- -- list map functions
- Max1' t (Reversed' _ es) -> Just $ Max1' t es
- Max1' t (Cons' _ e (Reversed' _ es)) -> Just $ Max1' t (Cons' t e es)
- Max1' t (Sorted' _ es) -> Just $ Max1' t es
- Max1' t (Cons' _ e (Sorted' _ es)) -> Just $ Max1' t (Cons' t e es)
- Max1' t (Map' t1 t2 f es) -> case f of
- Lam x _ e | x `isUnusedVar` e -> Just e
- Lam x _ (Max2' _ e1 e2) -> Just $ Max2' t (Map' t1 t2 (Lam x t e1) es) (Map' t1 t2 (Lam x t e2) es)
- Lam x _ (Negate' e) -> Just $ Negate' (Min1' t2 (Map' t1 t2 (Lam x IntTy e) es))
- Lam x _ (Plus' e1 e2) | x `isUnusedVar` e1 -> Just $ Plus' e1 (Max1' t2 (Map' t1 t2 (Lam x IntTy e2) es))
- Lam x _ (Plus' e1 e2) | x `isUnusedVar` e2 -> Just $ Plus' (Max1' t2 (Map' t1 t2 (Lam x IntTy e1) es)) e2
- _ -> Nothing
- Max1' t (Cons' _ e0 (Map' t1 t2 f xs)) -> case f of
- Lam x _ e | x `isUnusedVar` e -> Just $ If' t (Equal' IntTy (Len' t xs) Lit0) e0 (Max2' t e0 e)
- Lam x _ (Max2' _ e1 e2) -> Just $ Max2' t (Max1' t (Cons' t e0 (Map' t1 t2 (Lam x t e1) xs))) (Max1' t (Cons' t e0 (Map' t1 t2 (Lam x t e2) xs)))
- Lam x _ (Negate' e) -> Just $ Negate' (Min1' t (Cons' t (Negate' e0) (Map' t1 t2 (Lam x IntTy e) xs)))
- Lam x _ (Plus' e1 e2) | x `isUnusedVar` e1 -> Just $ Plus' e1 (Max1' t (Cons' t (Minus' e0 e1) (Map' t1 t2 (Lam x IntTy e2) xs)))
- Lam x _ (Plus' e1 e2) | x `isUnusedVar` e2 -> Just $ Plus' (Max1' t (Cons' t (Minus' e0 e2) (Map' t1 t2 (Lam x IntTy e1) xs))) e2
- _ -> Nothing
- _ -> Nothing
+reduceMax :: MonadAlpha m => RewriteRule m
+reduceMax =
+ mconcat
+ [ -- 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 |],
+ -- list map functions
+ [r| "maximum/reversed" forall xs. maximum (reversed xs) = maximum xs |],
+ [r| "maximum/cons/reversed" forall x xs. maximum (cons x (reversed xs)) = maximum (cons x xs) |],
+ [r| "maximum/sorted" forall xs. maximum (sorted xs) = maximum xs |],
+ [r| "maximum/cons/sorted" forall x xs. maximum (cons x (sorted xs)) = maximum (cons x xs) |],
+ makeRewriteRule "maximum/map/const" $ \_ -> \case
+ Max1' _ (Map' _ _ (LamConst _ e) _) -> return $ Just e
+ _ -> return Nothing,
+ [r| "maximum/map/max" forall e1 e2 xs. maximum (map (fun x -> max e1 e2) xs) = max (maximum (map (fun x -> e1) xs)) (maximum (map (fun x -> e2) xs)) |],
+ [r| "maximum/map/negate" forall e xs. maximum (map (fun x -> - e) xs) = - (maximum (map (fun x -> e) xs)) |],
+ makeRewriteRule "maximum/map/plus" $ \_ -> \case
+ Max1' _ (Map' t1 _ (Lam x _ (Plus' k e)) xs) | x `isUnusedVar` k -> return . Just $ Plus' k (Max1' IntTy (Map' t1 IntTy (Lam x t1 e) xs))
+ _ -> return Nothing,
+ makeRewriteRule "maximum/map/plus'" $ \_ -> \case
+ Max1' _ (Map' t1 _ (Lam x _ (Plus' e k)) xs) | x `isUnusedVar` k -> return . Just $ Plus' k (Max1' IntTy (Map' t1 IntTy (Lam x t1 e) xs))
+ _ -> return Nothing,
+ makeRewriteRule "maximum/map/minus" $ \_ -> \case
+ Max1' _ (Map' t1 _ (Lam x _ (Minus' k e)) xs) | x `isUnusedVar` k -> return . Just $ Minus' k (Min1' IntTy (Map' t1 IntTy (Lam x t1 e) xs))
+ _ -> return Nothing,
+ makeRewriteRule "maximum/map/minus'" $ \_ -> \case
+ Max1' _ (Map' t1 _ (Lam x _ (Minus' e k)) xs) | x `isUnusedVar` k -> return . Just $ Minus' k (Max1' IntTy (Map' t1 IntTy (Lam x t1 e) xs))
+ _ -> return Nothing,
+ makeRewriteRule "maximum/cons/map/const" $ \_ -> \case
+ Max1' t (Cons' _ x (Map' _ _ (LamConst _ e) _)) -> return . Just $ Max2' t x e
+ _ -> return Nothing,
+ [r| "maximum/cons/map/max" forall e0 e1 e2 xs. maximum (cons e0 (map (fun x -> max e1 e2) xs)) = max (maximum (cons e0 (map (fun x -> e1) xs))) (maximum (cons e0 (map (fun x -> e2) xs))) |],
+ [r| "maximum/cons/map/negate" forall e0 e xs. maximum (cons e0 (map (fun x -> - e) xs)) = - (minimum (cons e0 (map (fun x -> e) xs))) |],
+ makeRewriteRule "maximum/cons/map/plus" $ \_ -> \case
+ Max1' _ (Cons' _ e0 (Map' t1 _ (Lam x _ (Plus' k e)) xs)) | x `isUnusedVar` k -> return . Just $ Plus' k (Max1' IntTy (Cons' IntTy (Minus' e0 k) (Map' t1 IntTy (Lam x t1 e) xs)))
+ _ -> return Nothing,
+ makeRewriteRule "maximum/cons/map/plus'" $ \_ -> \case
+ Max1' _ (Cons' _ e0 (Map' t1 _ (Lam x _ (Plus' e k)) xs)) | x `isUnusedVar` k -> return . Just $ Plus' k (Max1' IntTy (Cons' IntTy (Minus' e0 k) (Map' t1 IntTy (Lam x t1 e) xs)))
+ _ -> return Nothing,
+ makeRewriteRule "maximum/cons/map/minus" $ \_ -> \case
+ Max1' _ (Cons' _ e0 (Map' t1 _ (Lam x _ (Minus' k e)) xs)) | x `isUnusedVar` k -> return . Just $ Minus' k (Min1' IntTy (Cons' IntTy (Minus' k e0) (Map' t1 IntTy (Lam x t1 e) xs)))
+ _ -> return Nothing,
+ makeRewriteRule "maximum/cons/map/minus'" $ \_ -> \case
+ Max1' _ (Cons' _ e0 (Map' t1 _ (Lam x _ (Minus' e k)) xs)) | x `isUnusedVar` k -> return . Just $ Minus' (Max1' IntTy (Cons' IntTy (Plus' e0 k) (Map' t1 IntTy (Lam x t1 e) xs))) k
+ _ -> return Nothing
+ ]
-- | TODO: implement this
reduceArgMin :: Monad m => RewriteRule m
@@ -104,7 +150,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 :: Monad m => RewriteRule m
+rule :: MonadAlpha m => RewriteRule m
rule =
mconcat
[ reduceMin,
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
@@ -1,5 +1,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ViewPatterns #-}
-- |
-- Module : Jikka.Core.Convert.CloseSum
@@ -32,39 +34,38 @@
import Jikka.Core.Language.BuiltinPatterns
import Jikka.Core.Language.Expr
import Jikka.Core.Language.FreeVars
+import Jikka.Core.Language.LambdaPatterns
import Jikka.Core.Language.Lint
+import Jikka.Core.Language.QuasiRules
import Jikka.Core.Language.RewriteRules
-import Jikka.Core.Language.Util
reduceSum :: MonadAlpha m => RewriteRule m
reduceSum =
- let return' = return . Just
- in makeRewriteRule "reduceSum" $ \_ -> \case
- Sum' xs -> case xs of
- -- reduce list build functions
- Nil' _ -> return' Lit0
- Cons' _ x xs -> return' $ Plus' x (Sum' xs)
- Range1' n -> return' $ FloorDiv' (Mult' n (Minus' n Lit1)) Lit2
- -- reduce list map functions
- Reversed' _ xs -> return' $ Sum' xs
- Sorted' _ xs -> return' $ Sum' xs
- Filter' _ g (Map' t1 _ f xs) -> do
- x <- genVarName'
- let h = Lam x t1 (If' IntTy (App g (App f (Var x))) (App f (Var x)) Lit0)
- return' $ Sum' (Map' t1 IntTy h xs)
- Map' t1 IntTy (Lam x _ body) xs -> case (body, xs) of
- (e, xs) | x `isUnusedVar` e -> return' $ Mult' (Len' t1 xs) e
- (body, Range1' n) | body == Var x -> return' $ FloorDiv' (Mult' n (Minus' n Lit1)) Lit2
- (body, Range1' n) | body == Mult' (Var x) (Var x) || body == Pow' (Var x) (LitInt' 2) -> return' $ FloorDiv' (Mult' n (Mult' (Minus' n Lit1) (Minus' (Mult' Lit2 (Var x)) Lit1))) (LitInt' 6)
- (Negate' e, xs) -> return' $ Negate' (Sum' (Map' t1 IntTy (Lam x t1 e) xs))
- (Plus' e1 e2, xs) -> return' $ Plus' (Sum' (Map' t1 IntTy (Lam x t1 e1) xs)) (Sum' (Map' t1 IntTy (Lam x t1 e2) xs))
- (Minus' e1 e2, xs) -> return' $ Minus' (Sum' (Map' t1 IntTy (Lam x t1 e1) xs)) (Sum' (Map' t1 IntTy (Lam x t1 e2) xs))
- (Mult' e1 e2, xs) | x `isUnusedVar` e1 -> return' $ Mult' e1 (Sum' (Map' t1 IntTy (Lam x t1 e2) xs))
- (Mult' e1 e2, xs) | x `isUnusedVar` e2 -> return' $ Mult' e2 (Sum' (Map' t1 IntTy (Lam x t1 e1) xs))
- _ -> return Nothing
- -- others
- _ -> return Nothing
+ mconcat
+ [ -- reduce list build functions
+ [r| "sum/nil" sum nil = 0 |],
+ [r| "sum/cons" forall x xs. sum (cons x xs) = x + sum xs |],
+ [r| "sum/range" forall n. sum (range n) = n * (n - 1) /! 2 |],
+ -- reduce list map functions
+ [r| "sum/reversed" forall xs. sum (reversed xs) = sum xs |],
+ [r| "sum/sorted" forall xs. sum (sorted xs) = sum xs |],
+ [r| "sum/filter/map" forall g f xs. sum (filter g (map f xs)) = sum (map (fun x -> if g (f x) then f x else 0) xs) |],
+ makeRewriteRule "sum/map/const" $ \_ -> \case
+ Sum' (Map' _ _ (LamConst t e) xs) -> return . Just $ Mult' (Len' t xs) e
+ _ -> return Nothing,
+ [r| "sum/map/id" forall n. sum (map (fun x -> x) (range n)) = n * (n - 1) /! 2 |],
+ [r| "sum/map/pow/2" forall n. sum (map (fun x -> x ** 2) (range n)) = n * (n - 1) * (2 * n - 1) /! 6 |],
+ [r| "sum/map/pow/2'" forall n. sum (map (fun x -> x * x) (range n)) = n * (n - 1) * (2 * n - 1) /! 6 |],
+ [r| "sum/map/negate" forall e xs. sum (map (fun x -> - e) xs) = - sum (map (fun x -> e) xs) |],
+ [r| "sum/map/plus" forall e1 e2 xs. sum (map (fun x -> e1 + e2) xs) = sum (map (fun x -> e1) xs) + sum (map (fun x -> e2) xs) |],
+ [r| "sum/map/minus" forall e1 e2 xs. sum (map (fun x -> e1 - e2) xs) = sum (map (fun x -> e1) xs) - sum (map (fun x -> e2) xs) |],
+ makeRewriteRule "sum/map/mult" $ \_ -> \case
+ Sum' (Map' t1 t2 (Lam x t (Mult' k e)) xs) | x `isUnusedVar` k -> return . Just $ Mult' k (Sum' (Map' t1 t2 (Lam x t e) xs))
+ _ -> return Nothing,
+ makeRewriteRule "sum/map/mult'" $ \_ -> \case
+ Sum' (Map' t1 t2 (Lam x t (Mult' e k)) xs) | x `isUnusedVar` k -> return . Just $ Mult' k (Sum' (Map' t1 t2 (Lam x t e) xs))
_ -> return Nothing
+ ]
-- | TODO: implement this.
reduceProduct :: Monad m => RewriteRule m
@@ -88,39 +89,37 @@
-- * This assumes that `ModFloor` is already propagated.
reduceModSum :: MonadAlpha m => RewriteRule m
reduceModSum =
- let return' = return . Just
- in makeRewriteRule "reduceModSum" $ \_ -> \case
- ModSum' xs m -> case xs of
- -- the corner case
- _ | m == Lit1 -> return' Lit0
- -- reduce list build functions
- Nil' _ -> return' Lit0
- Cons' _ x xs -> return' $ ModPlus' x (ModSum' xs m) m
- Range1' n -> return' $ ModMult' (ModMult' n (ModPlus' n Lit1 m) m) (ModInv' Lit2 m) m
- -- reduce list map functions
- Reversed' _ xs -> return' $ ModSum' xs m
- Sorted' _ xs -> return' $ ModSum' xs m
- Filter' _ g (Map' t1 _ f xs) -> do
- x <- genVarName'
- let h = Lam x t1 (If' IntTy (App g (App f (Var x))) (App f (Var x)) Lit0)
- return' $ ModSum' (Map' t1 IntTy h xs) m
- Map' t1 IntTy (Lam x _ body) xs -> do
- let go body = case (body, xs) of
- (e, xs) | x `isUnusedVar` e -> return' $ ModMult' (Len' t1 xs) e m
- (body, Range1' n) | body == Var x -> return' $ ModMult' (ModMult' n (ModMinus' n Lit1 m) m) (ModInv' Lit2 m) m
- (body, Range1' n) | body == ModMult' (Var x) (Var x) m || body == ModPow' (Var x) (LitInt' 2) m -> return' $ ModMult' (ModMult' n (ModMult' (ModMinus' n Lit1 m) (ModMinus' (ModMult' Lit2 n m) Lit1 m) m) m) (ModInv' (LitInt' 6) m) m
- (ModNegate' e m', xs) | m' == m -> return' $ ModNegate' (ModSum' (Map' t1 IntTy (Lam x t1 e) xs) m) m
- (ModPlus' e1 e2 m', xs) | m' == m -> return' $ ModPlus' (ModSum' (Map' t1 IntTy (Lam x t1 e1) xs) m) (ModSum' (Map' t1 IntTy (Lam x t1 e2) xs) m) m
- (ModMinus' e1 e2 m', xs) | m' == m -> return' $ ModMinus' (ModSum' (Map' t1 IntTy (Lam x t1 e1) xs) m) (ModSum' (Map' t1 IntTy (Lam x t1 e2) xs) m) m
- (ModMult' e1 e2 m', xs) | x `isUnusedVar` e1 && m' == m -> return' $ ModMult' e1 (ModSum' (Map' t1 IntTy (Lam x t1 e2) xs) m) m
- (ModMult' e1 e2 m', xs) | x `isUnusedVar` e2 && m' == m -> return' $ ModMult' e2 (ModSum' (Map' t1 IntTy (Lam x t1 e1) xs) m) m
- _ -> return Nothing
- case body of
- FloorMod' body m' | m' == m -> go body -- We shouldn't remove FloorMod not to introduce loops of rewrite rules between Jikka.Core.Convert.PropagateMod.
- _ -> go body
- -- others
- _ -> return Nothing
+ mconcat
+ [ -- the corner case
+ [r| "modsum/1" forall xs. modsum xs 1 = 0 |],
+ -- reduce list build functions
+ [r| "modsum/nil" forall m. modsum nil m = 0 |],
+ [r| "modsum/cons" forall m x xs. modsum (cons x xs) m = modplus x (sum xs) m |],
+ [r| "modsum/range" forall m n. modsum (range n) m = (n * (n - 1) /! 2) % m |],
+ -- reduce list map functions
+ [r| "modsum/reversed" forall m xs. modsum (reversed xs) m = modsum xs m |],
+ [r| "modsum/sorted" forall m xs. modsum (sorted xs) m = modsum xs m |],
+ [r| "modsum/filter/map" forall m g f xs. modsum (filter g (map f xs)) m = modsum (map (fun x -> if g (f x) then f x else 0) xs) m |],
+ makeRewriteRule "modsum/map/const" $ \_ -> \case
+ ModSum' (Map' _ _ (LamConst t e) xs) m -> return . Just $ ModMult' (Len' t xs) e m
+ _ -> return Nothing,
+ makeRewriteRule "modsum/map/floormod/const" $ \_ -> \case
+ ModSum' (Map' _ _ (LamConst t (FloorMod' e m')) xs) m | m' == m -> return . Just $ ModMult' (Len' t xs) e m
+ _ -> return Nothing,
+ [r| "modsum/map/id" forall m n. modsum (map (fun x -> x) (range n)) m = n * (n - 1) /! 2 % m |],
+ [r| "modsum/map/floormod/id" forall m n. modsum (map (fun x -> x % m) (range n)) m = n * (n - 1) /! 2 % m |],
+ [r| "modsum/map/modpow/2" forall m n. modsum (map (fun x -> modpow x 2 m) (range n)) m = n * (n - 1) * (2 * n - 1) /! 6 % m |],
+ [r| "modsum/map/modpow/2'" forall m n. modsum (map (fun x -> modmult x x m) (range n)) m = n * (n - 1) * (2 * n - 1) /! 6 % m |],
+ [r| "modsum/map/modnegate" forall m e xs. modsum (map (fun x -> modnegate e m) xs) m = modnegate (modsum (map (fun x -> e) xs) m) m |],
+ [r| "modsum/map/modplus" forall m e1 e2 xs. modsum (map (fun x -> modplus e1 e2 m) xs) m = modplus (modsum (map (fun x -> e1) xs) m) (modsum (map (fun x -> e2) xs) m) m |],
+ [r| "modsum/map/modminus" forall m e1 e2 xs. modsum (map (fun x -> modminus e1 e2 m) xs) m = modminus (modsum (map (fun x -> e1) xs) m) (modsum (map (fun x -> e2) xs) m) m |],
+ makeRewriteRule "modsum/map/modmult" $ \_ -> \case
+ ModSum' (Map' t1 t2 (Lam x t (ModMult' k e m')) xs) m | x `isUnusedVar` k && m' == m -> return . Just $ ModMult' k (ModSum' (Map' t1 t2 (Lam x t e) xs) m) m
+ _ -> return Nothing,
+ makeRewriteRule "modsum/map/modmult'" $ \_ -> \case
+ ModSum' (Map' t1 t2 (Lam x t (ModMult' e k m')) xs) m | x `isUnusedVar` k && m' == m -> return . Just $ ModMult' k (ModSum' (Map' t1 t2 (Lam x t e) xs) m) m
_ -> return Nothing
+ ]
-- | TODO: implement this.
reduceModProduct :: Monad m => RewriteRule m
diff --git a/src/Jikka/Core/Convert/ConstantFolding.hs b/src/Jikka/Core/Convert/ConstantFolding.hs
--- a/src/Jikka/Core/Convert/ConstantFolding.hs
+++ b/src/Jikka/Core/Convert/ConstantFolding.hs
@@ -1,5 +1,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ViewPatterns #-}
-- |
-- Module : Jikka.Core.Convert.ConstantFolding
@@ -22,9 +24,13 @@
rule,
reduceConstArithmeticExpr,
reduceConstMaxExpr,
+ reduceIdempotentBooleanExpr,
+ reduceUnitBooleanExpr,
reduceConstBooleanExpr,
+ reduceUnitBitExpr,
reduceConstBitExpr,
- reduceConstComparison,
+ reduceConstIntComparison,
+ reduceUnitBooleanComparison,
)
where
@@ -34,6 +40,7 @@
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.Runtime
@@ -117,28 +124,58 @@
--
-- === Boolean functions
--
+-- * `And` \(: \bool \to \bool \to \bool\)
+-- * `Or` \(: \bool \to \bool \to \bool\)
+-- * `Implies` \(: \bool \to \bool \to \bool\)
+reduceIdempotentBooleanExpr :: Monad m => RewriteRule m
+reduceIdempotentBooleanExpr =
+ mconcat
+ [ [r| "join/and" forall x. x && x = x|],
+ [r| "join/or" forall x. x || x = x|],
+ [r| "join/implies" forall x. implies (not x) x = x|],
+ [r| "join/implies'" forall x. implies x (not x) = not x|]
+ ]
+
+-- |
+-- == List of functions which are reduced
+--
+-- === Boolean functions
+--
-- * `Not` \(: \bool \to \bool\)
-- * `And` \(: \bool \to \bool \to \bool\)
-- * `Or` \(: \bool \to \bool \to \bool\)
-- * `Implies` \(: \bool \to \bool \to \bool\)
+reduceUnitBooleanExpr :: Monad m => RewriteRule m
+reduceUnitBooleanExpr =
+ mconcat
+ [ [r| "not/true" not true = false|],
+ [r| "not/false" not false = false|],
+ [r| "and/false" forall x. false && x = false|],
+ [r| "and/false'" forall x. x && false = false|],
+ [r| "and/true" forall x. true && x = x|],
+ [r| "and/true'" forall x. x && true = x|],
+ [r| "or/false" forall x. false || x = x|],
+ [r| "or/false'" forall x. x || false = x|],
+ [r| "or/true" forall x. true || x = true|],
+ [r| "or/true'" forall x. x || true = true|],
+ [r| "implies/false" forall x. implies false x = true|],
+ [r| "implies/false'" forall x. implies x false = not x|],
+ [r| "implies/true" forall x. implies true x = x|],
+ [r| "implies/true'" forall x. implies x true = true|]
+ ]
+
+-- |
+-- == List of functions which are reduced
+--
+-- === Boolean functions
+--
-- * `If` \(: \forall \alpha. \bool \to \alpha \to \alpha \to \alpha\)
reduceConstBooleanExpr :: Monad m => RewriteRule m
-reduceConstBooleanExpr = simpleRewriteRule "reduceConstBooleanExpr" $ \case
- Not' (LitBool' a) -> Just $ LitBool' (not a)
- And' _ LitFalse -> Just LitFalse
- And' a LitTrue -> Just a
- And' LitFalse _ -> Just LitFalse
- And' LitTrue b -> Just b
- Or' a LitFalse -> Just a
- Or' _ LitTrue -> Just LitTrue
- Or' LitFalse b -> Just b
- Or' LitTrue _ -> Just LitTrue
- Implies' a LitFalse -> Just $ Not' a
- Implies' _ LitTrue -> Just LitTrue
- Implies' LitFalse _ -> Just LitTrue
- Implies' LitTrue a -> Just a
- If' _ (LitBool' a) e1 e2 -> Just $ if a then e1 else e2
- _ -> Nothing
+reduceConstBooleanExpr =
+ mconcat
+ [ [r| "if/true" forall e1 e2. if true then e1 else e2 = e1|],
+ [r| "if/false" forall e1 e2. if false then e1 else e2 = e2|]
+ ]
-- |
-- == List of functions which are reduced
@@ -151,31 +188,47 @@
-- * `BitXor` \(: \int \to \int \to \int\)
-- * `BitLeftShift` \(: \int \to \int \to \int\)
-- * `BitRightShift` \(: \int \to \int \to \int\)
+reduceUnitBitExpr :: Monad m => RewriteRule m
+reduceUnitBitExpr =
+ mconcat
+ [ [r| "bitand/0" forall x. 0 & x = 0 |],
+ [r| "bitand/0'" forall x. x & 0 = 0 |],
+ [r| "bitand/-1" forall x. (-1) & x = x |],
+ [r| "bitand/-1'" forall x. x & (-1) = x |],
+ [r| "bitor/0" forall x. 0 | x = x |],
+ [r| "bitor/0'" forall x. x | 0 = x |],
+ [r| "bitor/-1" forall x. (-1) | x = -1 |],
+ [r| "bitor/-1'" forall x. x | (-1) = -1 |],
+ [r| "bitxor/0" forall x. 0 ^ x = x |],
+ [r| "bitxor/0'" forall x. x ^ 0 = x |],
+ [r| "bitxor/-1" forall x. (-1) ^ x = ~ x |],
+ [r| "bitxor/-1'" forall x. x ^ (-1) = ~ x |],
+ [r| "bitleftshift/0" forall x. 0 << x = 0 |],
+ [r| "bitleftshift/0'" forall x. x << 0 = x |],
+ [r| "bitrightshift/0" forall x. 0 >> x = 0 |],
+ [r| "bitrightshift/0'" forall x. x >> 0 = x |]
+ ]
+
+-- |
+-- == List of functions which are reduced
+--
+-- === Bitwise boolean functions
+--
+-- * `BitNot` \(: \int \to \int\)
+-- * `BitAnd` \(: \int \to \int \to \int\)
+-- * `BitOr` \(: \int \to \int \to \int\)
+-- * `BitXor` \(: \int \to \int \to \int\)
+-- * `BitLeftShift` \(: \int \to \int \to \int\)
+-- * `BitRightShift` \(: \int \to \int \to \int\)
reduceConstBitExpr :: Monad m => RewriteRule m
reduceConstBitExpr =
let return' = Just . LitInt'
in simpleRewriteRule "reduceConstBitExpr" $ \case
BitNot' (LitInt' a) -> return' $ complement a
- BitAnd' _ (LitInt' 0) -> return' 0
- BitAnd' a (LitInt' (-1)) -> Just a
- BitAnd' (LitInt' 0) _ -> return' 0
- BitAnd' (LitInt' (-1)) b -> Just b
BitAnd' (LitInt' a) (LitInt' b) -> return' $ a .&. b
- BitOr' a (LitInt' 0) -> Just a
- BitOr' _ (LitInt' (-1)) -> return' $ -1
- BitOr' (LitInt' 0) b -> Just b
- BitOr' (LitInt' (-1)) _ -> return' $ -1
BitOr' (LitInt' a) (LitInt' b) -> return' $ a .|. b
- BitXor' a (LitInt' 0) -> Just a
- BitXor' a (LitInt' (-1)) -> Just $ BitNot' a
- BitXor' (LitInt' 0) b -> Just b
- BitXor' (LitInt' (-1)) b -> Just $ BitNot' b
BitXor' (LitInt' a) (LitInt' b) -> return' $ a `xor` b
- BitLeftShift' a (LitInt' 0) -> Just a
- BitLeftShift' (LitInt' 0) _ -> return' 0
BitLeftShift' (LitInt' a) (LitInt' b) | - 100 < b && b < 100 -> return' $ a `shift` fromInteger b
- BitRightShift' a (LitInt' 0) -> Just a
- BitRightShift' (LitInt' 0) _ -> return' 0
BitRightShift' (LitInt' a) (LitInt' b) | - 100 < b && b < 100 -> return' $ a `shift` fromInteger (- b)
_ -> Nothing
@@ -190,30 +243,56 @@
-- * `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\))
-reduceConstComparison :: Monad m => RewriteRule m
-reduceConstComparison =
- simpleRewriteRule "reduceConstComparison" $
+reduceConstIntComparison :: Monad m => RewriteRule m
+reduceConstIntComparison =
+ simpleRewriteRule "comparison/const/int" $
(LitBool' <$>) . \case
LessThan' _ (LitInt' a) (LitInt' b) -> Just $ a < b
- LessEqual' _ (LitBool' a) (LitBool' b) -> Just $ a <= b
LessEqual' _ (LitInt' a) (LitInt' b) -> Just $ a <= b
- GreaterThan' _ (LitBool' a) (LitBool' b) -> Just $ a > b
GreaterThan' _ (LitInt' a) (LitInt' b) -> Just $ a > b
- GreaterEqual' _ (LitBool' a) (LitBool' b) -> Just $ a >= b
+ GreaterEqual' _ (LitInt' a) (LitInt' b) -> Just $ a >= b
Equal' _ (LitInt' a) (LitInt' b) -> Just $ a == b
- Equal' _ (LitBool' a) (LitBool' b) -> Just $ a == b
NotEqual' _ (LitInt' a) (LitInt' b) -> Just $ a /= b
- NotEqual' _ (LitBool' a) (LitBool' b) -> Just $ a /= b
_ -> Nothing
+-- |
+-- == List of functions which are reduced
+--
+-- === Comparison functions
+--
+-- * `LessThan` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
+-- * `LessEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
+-- * `GreaterThan` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
+-- * `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 =
+ mconcat
+ [ -- TODO: implement lessthan and lessequal
+ -- NOTE: We can ignore greaterthan and greaterequal because EqualitySolving swaps inequalities.
+ [r| "equal/true" forall x. true == x = x |],
+ [r| "equal/true'" forall x. x == true = x |],
+ [r| "equal/false" forall x. false == x = not x |],
+ [r| "equal/false'" forall x. x == false = not x |],
+ [r| "notequal/true" forall x. true /= x = not x |],
+ [r| "notequal/true'" forall x. x /= true = not x |],
+ [r| "notequal/false" forall x. false /= x = x |],
+ [r| "notequal/false'" forall x. x /= false = x |]
+ ]
+
rule :: MonadError Error m => RewriteRule m
rule =
mconcat
[ reduceConstArithmeticExpr,
reduceConstMaxExpr,
+ reduceIdempotentBooleanExpr,
+ reduceUnitBooleanExpr,
reduceConstBooleanExpr,
+ reduceUnitBitExpr,
reduceConstBitExpr,
- reduceConstComparison
+ reduceConstIntComparison,
+ reduceUnitBooleanComparison
]
runProgram :: MonadError Error m => Program -> m Program
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
@@ -78,7 +78,7 @@
--
-- Before:
--
--- > sum (fun i -> a[i]) (range n)
+-- > sum (map (fun i -> a[i]) (range n))
--
-- After:
--
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
@@ -1,5 +1,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ViewPatterns #-}
-- |
-- Module : Jikka.Core.Convert.EqualitySolving
@@ -18,6 +20,16 @@
module Jikka.Core.Convert.EqualitySolving
( run,
rule,
+
+ -- * internal rules
+ moveLiteralToRight,
+ convertGreaterToLess,
+ reduceReflexivity,
+ makeRightZero,
+ reduceIntInjective,
+ reduceNot,
+ reduceListCtor,
+ reduceListInjective,
)
where
@@ -25,30 +37,103 @@
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
+-- | `moveLiteralToRight` moves literals to lhs of `(==)` or `(/=)`, using symmetricity.
+moveLiteralToRight :: Monad m => RewriteRule m
+moveLiteralToRight =
+ mconcat
+ [ simpleRewriteRule "equal/symmetricity/literal" $ \case
+ Equal' t x y | isLiteral x && not (isLiteral y) -> Just $ Equal' t y x
+ _ -> Nothing,
+ simpleRewriteRule "notequal/symmetricity/literal" $ \case
+ Equal' t x y | isLiteral x && not (isLiteral y) -> Just $ Equal' t y x
+ _ -> Nothing
+ ]
+
+-- | `convertGreaterToLess` erases `(>)` and `(>=)`.
+convertGreaterToLess :: Monad m => RewriteRule m
+convertGreaterToLess =
+ mconcat
+ [ [r| "greaterthan->lessthan" forall x y. x > y = y < x |],
+ [r| "greaterequal->lessequal" forall x y. x >= y = y <= x |]
+ ]
+
+-- | `reduceReflexivity` uses reflexivity.
+reduceReflexivity :: Monad m => RewriteRule m
+reduceReflexivity =
+ mconcat
+ [ [r| "lessthan/reflexivity" forall x. x == x = false |],
+ [r| "lessequal/reflexivity" forall x. x == x = true |],
+ [r| "equal/reflexivity" forall x. x == x = true |],
+ [r| "notequal/reflexivity" forall x. x == x = false |]
+ ]
+
+-- | `makeRightZero` makes RHS of integer equality/inequality zero with subtracting RHS from both sides.
+makeRightZero :: Monad m => RewriteRule m
+makeRightZero =
+ mconcat
+ [ simpleRewriteRule "lessthan/right-zero" $ \case
+ LessThan' IntTy x y | y /= LitInt' 0 -> Just $ LessThan' IntTy (Minus' x y) (LitInt' 0)
+ _ -> Nothing,
+ simpleRewriteRule "lessequal/right-zero" $ \case
+ LessEqual' IntTy x y | y /= LitInt' 0 -> Just $ LessEqual' IntTy (Minus' x y) (LitInt' 0)
+ _ -> Nothing,
+ simpleRewriteRule "equal/right-zero" $ \case
+ Equal' IntTy x y | y /= LitInt' 0 -> Just $ Equal' IntTy (Minus' x y) (LitInt' 0)
+ _ -> Nothing,
+ simpleRewriteRule "notequal/right-zero" $ \case
+ NotEqual' IntTy x y | y /= LitInt' 0 -> Just $ NotEqual' IntTy (Minus' x y) (LitInt' 0)
+ _ -> Nothing
+ ]
+
+-- | `reduceIntInjective` removes injective functions from equalities of integers.
+reduceIntInjective :: Monad m => RewriteRule m
+reduceIntInjective =
+ mconcat
+ [ [r| "equal/negate" forall x y k. - x == 0 = x == 0 |],
+ [r| "equal/fact" forall x y. fact x - fact y == 0 = x == y |],
+ [r| "equal/fact'" forall x y. - fact x + fact y == 0 = x == y |]
+ ]
+
+reduceNot :: Monad m => RewriteRule m
+reduceNot =
+ mconcat
+ [ [r| "equal/not" forall x y. not x == y = x /= y |],
+ [r| "equal/not'" forall x y. x == not y = x /= y |],
+ [r| "notequal/not" forall x y. not x /= y = x == y |],
+ [r| "notequal/not'" forall x y. x /= not y = x == y |]
+ ]
+
+reduceListCtor :: Monad m => RewriteRule m
+reduceListCtor =
+ mconcat
+ [ [r| "equal/nil/nil" forall x xs. nil == nil = true |],
+ [r| "equal/cons/nil" forall x xs. cons x xs == nil = false |],
+ [r| "equal/nil/cons" forall x xs. nil == cons x xs = false |],
+ [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 =
+ mconcat
+ [ [r| "equal/range/range" forall n1 n2. range n1 == range n2 = n1 == n2 |]
+ ]
+
rule :: Monad m => RewriteRule m
-rule = simpleRewriteRule "Jikka.Core.Convert.EqualitySolving" $ \case
- -- reduce identity
- Equal' _ a b | a == b -> Just LitTrue
- -- align value on the right side to 0
- Equal' IntTy a b | b /= Lit0 -> Just $ Equal' IntTy (Minus' a b) Lit0
- LessThan' IntTy a b | b /= Lit0 -> Just $ LessThan' IntTy (Minus' a b) Lit0
- LessEqual' IntTy a b | b /= Lit0 -> Just $ LessEqual' IntTy (Minus' a b) Lit0
- GreaterThan' IntTy a b | b /= Lit0 -> Just $ GreaterThan' IntTy (Minus' a b) Lit0
- GreaterEqual' IntTy a b | b /= Lit0 -> Just $ GreaterEqual' IntTy (Minus' a b) Lit0
- NotEqual' IntTy a b | b /= Lit0 -> Just $ NotEqual' IntTy (Minus' a b) Lit0
- -- reduce injective function
- Equal' t (Minus' (Negate' a) (Negate' b)) Lit0 -> Just $ Equal' t (Minus' a b) Lit0
- Equal' t (Minus' (Not' a) (Not' b)) Lit0 -> Just $ Equal' t (Minus' a b) Lit0
- Equal' t (Minus' (Fact' a) (Fact' b)) Lit0 -> Just $ Equal' t (Minus' a b) Lit0
- -- unpack list equality
- Equal' _ (Nil' _) (Cons' _ _ _) -> Just LitFalse
- Equal' (ListTy t) (Cons' _ x xs) (Cons' _ y ys) -> Just $ And' (Equal' t x y) (Equal' (ListTy t) xs ys)
- -- reduce boolean equality
- Equal' _ a LitTrue -> Just a
- Equal' _ a LitFalse -> Just $ Not' a
- _ -> Nothing
+rule =
+ mconcat
+ [ moveLiteralToRight,
+ convertGreaterToLess,
+ reduceReflexivity,
+ makeRightZero,
+ reduceIntInjective,
+ reduceNot,
+ reduceListCtor,
+ reduceListInjective
+ ]
runProgram :: MonadError Error m => Program -> m Program
runProgram = applyRewriteRuleProgram' rule
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
@@ -14,6 +14,7 @@
)
where
+import Control.Monad.Trans.Maybe
import Data.List
import Data.Maybe
import Jikka.Common.Alpha
@@ -23,105 +24,69 @@
import Jikka.Core.Language.BuiltinPatterns
import Jikka.Core.Language.Expr
import Jikka.Core.Language.Lint
+import Jikka.Core.Language.ModuloExpr
import Jikka.Core.Language.RewriteRules
import Jikka.Core.Language.TypeCheck
import Jikka.Core.Language.Util
--- | `Mod` is a newtype to avoid mistakes that swapping left and right of mod-op.
-newtype Mod = Mod Expr
-
-isModulo' :: Expr -> Mod -> Bool
-isModulo' e (Mod m) = case e of
- FloorMod' _ m' -> m' == m
- ModNegate' _ m' -> m' == m
- ModPlus' _ _ m' -> m' == m
- ModMinus' _ _ m' -> m' == m
- ModMult' _ _ m' -> m' == m
- ModInv' _ m' -> m' == m
- ModPow' _ _ m' -> m' == m
- VecFloorMod' _ _ m' -> m' == m
- MatFloorMod' _ _ _ m' -> m' == m
- ModMatAp' _ _ _ _ m' -> m' == m
- ModMatAdd' _ _ _ _ m' -> m' == m
- ModMatMul' _ _ _ _ _ m' -> m' == m
- ModMatPow' _ _ _ m' -> m' == m
- ModSum' _ m' -> m' == m
- ModProduct' _ m' -> m' == m
- LitInt' n -> case m of
- LitInt' m -> 0 <= n && n < m
- _ -> False
- Proj' ts _ e | isVectorTy' ts -> e `isModulo'` Mod m
- Proj' ts _ e | isMatrixTy' ts -> e `isModulo'` Mod m
- Map' _ _ f _ -> f `isModulo'` Mod m
- Lam _ _ body -> body `isModulo'` Mod m
- e@(App _ _) -> case curryApp e of
- (e@(Lam _ _ _), _) -> e `isModulo'` Mod m
- (Tuple' ts, es) | isVectorTy' ts -> all (`isModulo'` Mod m) es
- (Tuple' ts, es) | isMatrixTy' ts -> all (`isModulo'` Mod m) es
- _ -> False
- _ -> False
-
-isModulo :: Expr -> Expr -> Bool
-isModulo e m = e `isModulo'` Mod m
+isModulo' :: Expr -> Expr -> Bool
+isModulo' e m = e `isModulo` Modulo m
-putFloorMod :: MonadAlpha m => Mod -> Expr -> m (Maybe Expr)
-putFloorMod (Mod m) =
- let return' = return . Just
- in \case
- Negate' e -> return' $ ModNegate' e m
- Plus' e1 e2 -> return' $ ModPlus' e1 e2 m
- Minus' e1 e2 -> return' $ ModMinus' e1 e2 m
- Mult' e1 e2 -> return' $ ModMult' e1 e2 m
- Pow' e1 e2 -> return' $ ModPow' e1 e2 m
- MatAp' h w e1 e2 -> return' $ ModMatAp' h w e1 e2 m
- MatAdd' h w e1 e2 -> return' $ ModMatAdd' h w e1 e2 m
- MatMul' h n w e1 e2 -> return' $ ModMatMul' h n w e1 e2 m
- MatPow' n e1 e2 -> return' $ ModMatPow' n e1 e2 m
- Sum' e -> return' $ ModSum' e m
- Product' e -> return' $ ModProduct' e m
- LitInt' n -> case m of
- LitInt' m -> return' $ LitInt' (n `mod` m)
- _ -> return Nothing
- Proj' ts i e | isVectorTy' ts -> return' $ Proj' ts i (VecFloorMod' (genericLength ts) e m)
- Proj' ts i e
- | isMatrixTy' ts ->
- let (h, w) = fromJust (sizeOfMatrixTy (TupleTy ts))
- in return' $ Proj' ts i (MatFloorMod' (toInteger h) (toInteger w) e m)
- Map' t1 t2 f xs -> do
- f <- putFloorMod (Mod m) f
- case f of
- Nothing -> return Nothing
- Just f -> return' $ Map' t1 t2 f xs
- Lam x t body -> do
- -- TODO: rename only if required
- y <- genVarName x
- body <- substitute x (Var y) body
- body <- putFloorMod (Mod m) body
- case body of
- Nothing -> return Nothing
- Just body -> return' $ Lam y t body
- e@(App _ _) -> case curryApp e of
- (f@(Lam _ _ _), args) -> do
- f <- putFloorMod (Mod m) f
- case f of
- Nothing -> return Nothing
- Just f -> return' $ uncurryApp f args
- (Tuple' ts, es) | isVectorTy' ts -> do
- es' <- mapM (putFloorMod (Mod m)) es
- if all isNothing es'
- then return Nothing
- else return' $ uncurryApp (Tuple' ts) (zipWith fromMaybe es es')
- (Tuple' ts, es) | isMatrixTy (TupleTy ts) -> do
- es' <- mapM (putFloorMod (Mod m)) es
- if all isNothing es'
- then return Nothing
- else return' $ uncurryApp (Tuple' ts) (zipWith fromMaybe es es')
- _ -> return Nothing
- _ -> return Nothing
+putFloorMod :: MonadAlpha m => Modulo -> Expr -> m (Maybe Expr)
+putFloorMod (Modulo m) =
+ runMaybeT . \case
+ Negate' e -> return $ ModNegate' e m
+ Plus' e1 e2 -> return $ ModPlus' e1 e2 m
+ Minus' e1 e2 -> return $ ModMinus' e1 e2 m
+ Mult' e1 e2 -> return $ ModMult' e1 e2 m
+ JustDiv' e1 e2 -> return $ ModMult' e1 (ModInv' e2 m) m
+ Pow' e1 e2 -> return $ ModPow' e1 e2 m
+ MatAp' h w e1 e2 -> return $ ModMatAp' h w e1 e2 m
+ MatAdd' h w e1 e2 -> return $ ModMatAdd' h w e1 e2 m
+ MatMul' h n w e1 e2 -> return $ ModMatMul' h n w e1 e2 m
+ MatPow' n e1 e2 -> return $ ModMatPow' n e1 e2 m
+ Sum' e -> return $ ModSum' e m
+ Product' e -> return $ ModProduct' e m
+ LitInt' n -> case m of
+ LitInt' m -> return $ LitInt' (n `mod` m)
+ _ -> MaybeT $ return Nothing
+ Proj' ts i e | isVectorTy' ts -> return $ Proj' ts i (VecFloorMod' (genericLength ts) e m)
+ Proj' ts i e
+ | isMatrixTy' ts ->
+ let (h, w) = fromJust (sizeOfMatrixTy (TupleTy ts))
+ in return $ Proj' ts i (MatFloorMod' (toInteger h) (toInteger w) e m)
+ Map' t1 t2 f xs -> do
+ f <- MaybeT $ putFloorMod (Modulo m) f
+ return $ Map' t1 t2 f xs
+ Foldl' t1 t2 f init xs -> do
+ f <- MaybeT $ putFloorMod (Modulo m) f
+ return $ Foldl' t1 t2 f init xs
+ Lam x t body -> do
+ -- TODO: rename only if required
+ y <- lift $ genVarName x
+ body <- lift $ substitute x (Var y) body
+ body <- MaybeT $ putFloorMod (Modulo m) body
+ return $ Lam y t body
+ e@(App _ _) -> case curryApp e of
+ (f@(Lam _ _ _), args) -> do
+ f <- MaybeT $ putFloorMod (Modulo m) f
+ return $ uncurryApp f args
+ (Tuple' ts, es) | isVectorTy' ts -> do
+ es' <- lift $ mapM (putFloorMod (Modulo m)) es
+ if all isNothing es'
+ then MaybeT $ return Nothing
+ else return $ uncurryApp (Tuple' ts) (zipWith fromMaybe es es')
+ (Tuple' ts, es) | isMatrixTy (TupleTy ts) -> do
+ es' <- lift $ mapM (putFloorMod (Modulo m)) es
+ if all isNothing es'
+ then MaybeT $ return Nothing
+ else return $ uncurryApp (Tuple' ts) (zipWith fromMaybe es es')
+ _ -> MaybeT $ return Nothing
+ _ -> MaybeT $ return Nothing
-putFloorModGeneric :: MonadAlpha m => (Expr -> Mod -> m Expr) -> Mod -> Expr -> m Expr
+putFloorModGeneric :: MonadAlpha m => (Expr -> Modulo -> m Expr) -> Modulo -> Expr -> m Expr
putFloorModGeneric fallback m e =
- if e `isModulo'` m
+ if e `isModulo` m
then return e
else do
e' <- putFloorMod m e
@@ -129,29 +94,26 @@
Just e' -> return e'
Nothing -> fallback e m
-putFloorModInt :: MonadAlpha m => Mod -> Expr -> m Expr
-putFloorModInt = putFloorModGeneric (\e (Mod m) -> return $ FloorMod' e m)
-
-putMapFloorMod :: MonadAlpha m => Mod -> Expr -> m Expr
+putMapFloorMod :: MonadAlpha m => Modulo -> Expr -> m Expr
putMapFloorMod = putFloorModGeneric fallback
where
- fallback e (Mod m) = do
+ fallback e (Modulo m) = do
x <- genVarName'
return $ Map' IntTy IntTy (Lam x IntTy (FloorMod' (Var x) m)) e
-putVecFloorMod :: (MonadError Error m, MonadAlpha m) => [(VarName, Type)] -> Mod -> Expr -> m Expr
+putVecFloorMod :: (MonadError Error m, MonadAlpha m) => [(VarName, Type)] -> Modulo -> Expr -> m Expr
putVecFloorMod env = putFloorModGeneric fallback
where
- fallback e (Mod m) = do
+ fallback e (Modulo m) = do
t <- typecheckExpr env e
case t of
TupleTy ts -> return $ VecFloorMod' (genericLength ts) e m
_ -> throwInternalError $ "not a vector: " ++ formatType t
-putMatFloorMod :: (MonadError Error m, MonadAlpha m) => [(VarName, Type)] -> Mod -> Expr -> m Expr
+putMatFloorMod :: (MonadError Error m, MonadAlpha m) => [(VarName, Type)] -> Modulo -> Expr -> m Expr
putMatFloorMod env = putFloorModGeneric fallback
where
- fallback e (Mod m) = do
+ fallback e (Modulo m) = do
t <- typecheckExpr env e
case t of
TupleTy ts@(TupleTy ts' : _) -> return $ MatFloorMod' (genericLength ts) (genericLength ts') e m
@@ -159,33 +121,38 @@
rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m
rule =
- let go1 m f (t1, e1) = Just <$> (f <$> t1 (Mod m) e1 <*> pure m)
- go2 m f (t1, e1) (t2, e2) = Just <$> (f <$> t1 (Mod m) e1 <*> t2 (Mod m) e2 <*> pure m)
+ let go0 :: Expr -> Maybe Expr
+ go0 e = do
+ e' <- formatBottomModuloExpr <$> parseModuloExpr e
+ guard $ e' /= e
+ return e'
+ go1 m f (t1, e1) = Just <$> (f <$> t1 (Modulo m) e1 <*> pure m)
+ go2 m f (t1, e1) (t2, e2) = Just <$> (f <$> t1 (Modulo m) e1 <*> t2 (Modulo m) e2 <*> pure m)
in makeRewriteRule "Jikka.Core.Convert.PropagateMod" $ \env -> \case
- ModNegate' e m | not (e `isModulo` m) -> go1 m ModNegate' (putFloorModInt, e)
- ModPlus' e1 e2 m | not (e1 `isModulo` m) || not (e2 `isModulo` m) -> go2 m ModPlus' (putFloorModInt, e1) (putFloorModInt, e2)
- ModMinus' e1 e2 m | not (e1 `isModulo` m) || not (e2 `isModulo` m) -> go2 m ModMinus' (putFloorModInt, e1) (putFloorModInt, e2)
- ModMult' e1 e2 m | not (e1 `isModulo` m) || not (e2 `isModulo` m) -> go2 m ModMult' (putFloorModInt, e1) (putFloorModInt, e2)
- ModInv' e m | not (e `isModulo` m) -> go1 m ModInv' (putFloorModInt, e)
- ModPow' e1 e2 m | not (e1 `isModulo` m) -> go2 m ModPow' (putFloorModInt, 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 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)
- ModSum' e m | not (e `isModulo` m) -> go1 m ModSum' (putMapFloorMod, e)
- ModProduct' e m | not (e `isModulo` m) -> go1 m ModProduct' (putMapFloorMod, e)
+ e@(ModNegate' _ _) -> return $ go0 e
+ e@(ModPlus' _ _ _) -> return $ go0 e
+ e@(ModMinus' _ _ _) -> return $ go0 e
+ 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)
+ 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 ->
- if e `isModulo` m
+ if e `isModulo'` m
then return $ Just e
- else putFloorMod (Mod m) e
+ else putFloorMod (Modulo m) e
VecFloorMod' _ e m ->
- if e `isModulo` m
+ if e `isModulo'` m
then return $ Just e
- else putFloorMod (Mod m) e
+ else putFloorMod (Modulo m) e
MatFloorMod' _ _ e m ->
- if e `isModulo` m
+ if e `isModulo'` m
then return $ Just e
- else putFloorMod (Mod m) e
+ else putFloorMod (Modulo m) e
_ -> return Nothing
runProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Program
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
@@ -130,22 +130,31 @@
reduceCumulativeSum :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceCumulativeSum = makeRewriteRule "reduceCumulativeSum" $ \_ -> \case
-- foldl (fun a i -> setat a index(i) e(a, i)) base incides
- Foldl' t1 t2 (Lam2 a _ i _ (SetAt' t (Var a') index e)) base indices | a' == a && a `isUnusedVar` index -> runMaybeT $ do
+ Foldl' t1 (ListTy t2) (Lam2 a _ i _ (SetAt' t (Var a') index e)) base indices | a' == a && a `isUnusedVar` index -> runMaybeT $ do
+ -- list cumulative sums
let sums = listCumulativeSum (Var a) e
guard $ not (null sums)
let semigrps = nub (sort (map fst sums))
- let ts = t2 : map SegmentTreeTy semigrps
+ -- list segment trees
+ let ts = ListTy t2 : map SegmentTreeTy semigrps
c <- lift $ genVarName a
let proj i = Proj' ts i (Var c)
let e' = replaceWithSegtrees a (zip semigrps (map proj [1 ..])) e
guard $ e' /= e
+ -- e'(c0, i) = e(c0, i)
e' <- lift $ substitute a (proj 0) e'
- b' <- lift $ genVarName a
- let updateSegtrees i semigrp = SegmentTreeSetPoint' semigrp (proj i) index (At' t (Var b') index)
- let step = Lam2 c (TupleTy ts) i t1 (Let b' t2 (SetAt' t (proj 0) index e') (uncurryApp (Tuple' ts) (Var b' : zipWith updateSegtrees [1 ..] semigrps)))
+ e'' <- lift genVarName'
+ let updateSegtrees i semigrp = SegmentTreeSetPoint' semigrp (proj i) index (Var e'')
+ -- step = fun (c0, c1, ..., ck) i -> let e'' = e'(c0, i) in (setAt c0 index(i) e'', update c1 index(i) e'', ..., update ck index(i) e'')
+ let step =
+ Lam2 c (TupleTy ts) i t1 $
+ Let e'' t2 e' $
+ uncurryApp (Tuple' ts) (SetAt' t (proj 0) index (Var e'') : zipWith updateSegtrees [1 ..] semigrps)
b <- lift $ genVarName a
+ -- base' = (b, init b, ..., init b)
let base' = Var b : map (\semigrp -> SegmentTreeInitList' semigrp (Var b)) semigrps
- return $ Let b t2 base (Proj' ts 0 (Foldl' t1 (TupleTy ts) step (uncurryApp (Tuple' ts) base') indices))
+ -- let b = base in (foldl step base' indices).0
+ return $ Let b (ListTy t2) base (Proj' ts 0 (Foldl' t1 (TupleTy ts) step (uncurryApp (Tuple' ts) base') indices))
_ -> return Nothing
-- | `reduceFromMin` uses segment trees from accumulation of min/max which are not reducible to cumulative sums.
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
@@ -41,7 +41,6 @@
import Jikka.Core.Language.Lint
import Jikka.Core.Language.QuasiRules
import Jikka.Core.Language.RewriteRules
-import Jikka.Core.Language.Util
-- |
-- * `Range1` remains.
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
@@ -1,5 +1,6 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ViewPatterns #-}
-- |
-- Module : Jikka.Core.Convert.SpecializeFoldl
@@ -22,19 +23,46 @@
import Jikka.Common.Alpha
import Jikka.Common.Error
+import Jikka.Core.Language.ArithmeticExpr
import Jikka.Core.Language.BuiltinPatterns
import Jikka.Core.Language.Expr
import Jikka.Core.Language.FreeVars
import Jikka.Core.Language.Lint
+import Jikka.Core.Language.ModuloExpr
import Jikka.Core.Language.RewriteRules
+convertToSum :: Expr -> Maybe Expr
+convertToSum = \case
+ Foldl' t1 IntTy (Lam2 x2 _ x1 _ body) init xs -> do
+ (a, b) <- makeAffineFunctionFromArithmeticExpr x2 (parseArithmeticExpr body)
+ guard $ isOneArithmeticExpr a
+ return $ Plus' init (Sum' (Map' t1 IntTy (Lam x1 t1 (formatArithmeticExpr b)) xs))
+ _ -> Nothing
+
+convertToModSum :: Expr -> Maybe Expr
+convertToModSum = \case
+ Foldl' t1 IntTy (Lam2 x2 _ x1 _ body) init xs -> do
+ body <- parseModuloExpr body
+ (a, b) <- makeAffineFunctionFromArithmeticExpr x2 (arithmeticExprFromModuloExpr body)
+ guard $ isOneArithmeticExpr a
+
+ -- `if` is required for cases like `foldl (fun y x -> y % 2) 3 xs`, which is the same to `if xs == nil then 3 else 1`.
+ let wrap :: Expr -> Expr
+ wrap =
+ if init `isModulo` Modulo (moduloOfModuloExpr body)
+ then id
+ else If' IntTy (Equal' (ListTy t1) xs (Nil' t1)) init
+
+ return . wrap $
+ ModPlus' init (ModSum' (Map' t1 IntTy (Lam x1 t1 (formatArithmeticExpr b)) xs) (moduloOfModuloExpr body)) (moduloOfModuloExpr body)
+ _ -> Nothing
+
rule :: MonadAlpha m => RewriteRule m
rule = simpleRewriteRule "Jikka.Core.Convert.SpecializeFoldl" $ \case
+ (convertToSum -> Just e) -> return e
+ (convertToModSum -> Just e) -> return e
+ -- TODO: Replace these operators with the better implementation like sum.
Foldl' t1 t2 (Lam2 x2 _ x1 _ body) init xs -> case body of
- -- Sum
- Plus' (Var x2') e | x2' == x2 && x2 `isUnusedVar` e -> Just $ Sum' (Cons' t2 init (Map' t1 t2 (Lam x1 t1 e) xs))
- Plus' e (Var x2') | x2' == x2 && x2 `isUnusedVar` e -> Just $ Sum' (Cons' t2 init (Map' t1 t2 (Lam x1 t1 e) xs))
- Minus' (Var x2') e | x2' == x2 && x2 `isUnusedVar` e -> Just $ Minus' init (Sum' (Map' t1 t2 (Lam x1 t1 e) xs))
-- Product
Mult' (Var x2') e | x2' == x2 && x2 `isUnusedVar` e -> Just $ Product' (Cons' t2 init (Map' t1 t2 (Lam x1 t1 e) xs))
Mult' e (Var x2') | x2' == x2 && x2 `isUnusedVar` e -> Just $ Product' (Cons' t2 init (Map' t1 t2 (Lam x1 t1 e) xs))
@@ -60,10 +88,6 @@
_ -> Nothing
-- The outer floor-mod is required because foldl for empty lists returns values without modulo.
FloorMod' (Foldl' t1 t2 (Lam2 x2 _ x1 _ body) init xs) m -> case body of
- -- ModSum
- ModPlus' (Var x2') e m' | x2' == x2 && x2 `isUnusedVar` e && m' == m -> Just $ ModSum' (Cons' t2 init (Map' t1 t2 (Lam x1 t1 e) xs)) m
- ModPlus' e (Var x2') m' | x2' == x2 && x2 `isUnusedVar` e && m' == m -> Just $ ModSum' (Cons' t2 init (Map' t1 t2 (Lam x1 t1 e) xs)) m
- ModMinus' (Var x2') e m' | x2' == x2 && x2 `isUnusedVar` e && m' == m -> Just $ ModMinus' init (ModSum' (Map' t1 t2 (Lam x1 t1 e) xs) m) m
-- ModProduct
ModMult' (Var x2') e m' | x2' == x2 && x2 `isUnusedVar` e && m' == m -> Just $ ModProduct' (Cons' t2 init (Map' t1 t2 (Lam x1 t1 e) xs)) m
ModMult' e (Var x2') m' | x2' == x2 && x2 `isUnusedVar` e && m' == m -> Just $ ModProduct' (Cons' t2 init (Map' t1 t2 (Lam x1 t1 e) xs)) m
diff --git a/src/Jikka/Core/Convert/StrengthReduction.hs b/src/Jikka/Core/Convert/StrengthReduction.hs
deleted file mode 100644
--- a/src/Jikka/Core/Convert/StrengthReduction.hs
+++ /dev/null
@@ -1,107 +0,0 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE LambdaCase #-}
-
--- |
--- Module : Jikka.Core.Convert.StrengthReduction
--- Description : does strength reduction. / 演算子強度低減を行います。
--- Copyright : (c) Kimiyuki Onaka, 2020
--- License : Apache License 2.0
--- Maintainer : kimiyuki95@gmail.com
--- Stability : experimental
--- Portability : portable
-module Jikka.Core.Convert.StrengthReduction
- ( run,
- )
-where
-
-import Jikka.Common.Alpha
-import Jikka.Common.Error
-import Jikka.Core.Language.BuiltinPatterns
-import Jikka.Core.Language.Expr
-import Jikka.Core.Language.Lint
-import Jikka.Core.Language.RewriteRules
-
--- | `eliminateSomeBuiltins` removes some `Builtin` from `Expr` at all.
-eliminateSomeBuiltins :: Monad m => RewriteRule m
-eliminateSomeBuiltins = simpleRewriteRule "eliminateSomeBuiltins" $ \case
- -- advanced arithmetical functions
- Abs' e -> Just $ Max2' IntTy e (Negate' e)
- Lcm' e1 e2 -> Just $ FloorDiv' (Gcd' e1 e2) (Mult' e1 e2)
- -- logical functions
- Implies' e1 e2 -> Just $ Or' (Not' e1) e2
- -- comparison
- GreaterThan' t e1 e2 -> Just $ LessThan' t e2 e1
- GreaterEqual' t e1 e2 -> Just $ LessEqual' t e2 e1
- NotEqual' t e1 e2 -> Just $ Not' (Equal' t e1 e2)
- _ -> Nothing
-
--- | `reduceNegate` brings `Negate` to the root.
-reduceNegate :: Monad m => RewriteRule m
-reduceNegate = simpleRewriteRule "reduceNegate" $ \case
- Negate' (Negate' e) -> Just e
- Plus' (Negate' e1) (Negate' e2) -> Just $ Negate' (Plus' e1 e2)
- Minus' e1 (Negate' e2) -> Just $ Plus' e1 e2
- Minus' (Negate' e1) e2 -> Just $ Negate' (Plus' e1 e2)
- -- `Minus` is already removed.
- Mult' (Negate' e1) e2 -> Just $ Negate' (Mult' e1 e2)
- Mult' e1 (Negate' e2) -> Just $ Negate' (Mult' e1 e2)
- -- `Abs` is already removed.
- Min2' IntTy (Negate' e1) (Negate' e2) -> Just $ Negate' (Max2' IntTy e1 e2)
- Max2' IntTy (Negate' e1) (Negate' e2) -> Just $ Negate' (Min2' IntTy e1 e2)
- _ -> Nothing
-
--- | `reduceNot` brings `Not` to the root.
-reduceNot :: Monad m => RewriteRule m
-reduceNot = simpleRewriteRule "reduceNot" $ \case
- Not' (Not' e) -> Just e
- And' (Not' e1) (Not' e2) -> Just $ Not' (Or' e1 e2)
- Or' (Not' e1) (Not' e2) -> Just $ Not' (And' e1 e2)
- -- `Implies` is already removed.
- Mult' (Negate' e1) e2 -> Just $ Negate' (Mult' e1 e2)
- Mult' e1 (Negate' e2) -> Just $ Negate' (Mult' e1 e2)
- If' t (Not' e1) e2 e3 -> Just $ If' t e1 e3 e2
- _ -> Nothing
-
--- | `reduceBitNot` brings `BitNot` to the root.
-reduceBitNot :: Monad m => RewriteRule m
-reduceBitNot = simpleRewriteRule "reduceBitNot" $ \case
- BitNot' (BitNot' e) -> Just e
- BitAnd' (BitNot' e1) (BitNot' e2) -> Just $ BitNot' (BitOr' e1 e2)
- BitOr' (BitNot' e1) (BitNot' e2) -> Just $ BitNot' (BitAnd' e1 e2)
- BitXor' (BitNot' e1) e2 -> Just $ BitNot' (BitXor' e1 e2)
- BitXor' e1 (BitNot' e2) -> Just $ BitNot' (BitXor' e1 e2)
- _ -> Nothing
-
-reduceMisc :: Monad m => RewriteRule m
-reduceMisc = simpleRewriteRule "reduceMisc" $ \case
- -- arithmetical functions
- Pow' (Pow' e1 e2) e3 -> Just $ Pow' e1 (Plus' e2 e3)
- -- advanced arithmetical functions
- Gcd' (Mult' k1 e1) (Mult' k2 e2) | k1 == k2 -> Just $ Mult' k1 (Gcd' e1 e2)
- Gcd' (Mult' k1 e1) (Mult' e2 k2) | k1 == k2 -> Just $ Mult' k1 (Gcd' e1 e2)
- Gcd' (Mult' e1 k1) (Mult' e2 k2) | k1 == k2 -> Just $ Mult' k1 (Gcd' e1 e2)
- Gcd' (Mult' e1 k1) (Mult' k2 e2) | k1 == k2 -> Just $ Mult' k1 (Gcd' e1 e2)
- _ -> Nothing
-
-rule :: MonadAlpha m => RewriteRule m
-rule =
- mconcat
- [ eliminateSomeBuiltins,
- reduceNegate,
- reduceNot,
- reduceBitNot,
- reduceMisc
- ]
-
-runProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Program
-runProgram = applyRewriteRuleProgram' rule
-
--- | TODO: Split and remove this module.
-run :: (MonadAlpha m, MonadError Error m) => Program -> m Program
-run prog = wrapError' "Jikka.Core.Convert.StrengthReduction" $ do
- precondition $ do
- ensureWellTyped prog
- prog <- runProgram prog
- postcondition $ do
- ensureWellTyped 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
@@ -29,12 +29,12 @@
import Control.Arrow (second)
import Control.Monad.State.Strict
-import Control.Monad.Writer.Strict (MonadWriter, execWriterT, tell)
+import Control.Monad.Writer.Strict (MonadWriter, censor, execWriterT, tell)
import qualified Data.Map.Strict as M
import Data.Monoid (Dual (..))
import Jikka.Common.Alpha
import Jikka.Common.Error
-import Jikka.Core.Format (formatType)
+import Jikka.Core.Format (formatExpr, formatToplevelExpr, formatType)
import Jikka.Core.Language.BuiltinPatterns
import Jikka.Core.Language.Expr
import Jikka.Core.Language.FreeVars
@@ -42,21 +42,48 @@
import Jikka.Core.Language.TypeCheck (literalToType, typecheckExpr, typecheckProgram)
import Jikka.Core.Language.Util
+data Hint
+ = VarHint VarName
+ | ExprHint Expr
+ | ToplevelExprHint ToplevelExpr
+ deriving (Eq, Ord, Show, Read)
+
data Equation
- = TypeEquation Type Type
+ = TypeEquation Type Type [Hint]
| TypeAssertion VarName Type
deriving (Eq, Ord, Show, Read)
type Eqns = Dual [Equation]
+consHint :: Hint -> Equation -> Equation
+consHint hint = \case
+ TypeEquation t1 t2 hints -> TypeEquation t1 t2 (hint : hints)
+ TypeAssertion x t -> TypeAssertion x t
+
+wrapHint :: MonadWriter Eqns m => Hint -> m a -> m a
+wrapHint hint = censor (fmap (map (consHint hint)))
+
+wrapErrorFromHint :: MonadError Error m => Hint -> m a -> m a
+wrapErrorFromHint = \case
+ VarHint x -> wrapError' $ "around variable " ++ unVarName x
+ ExprHint e -> wrapError' $ "around expr " ++ summarize (formatExpr e)
+ ToplevelExprHint e -> wrapError' $ "around toplevel expr " ++ summarize (formatToplevelExpr e)
+ where
+ summarize s = case lines s of
+ (s : _ : _) -> s ++ " ..."
+ _ -> s
+
+wrapErrorFromHints :: MonadError Error m => [Hint] -> m a -> m a
+wrapErrorFromHints hints = foldr (\hint f -> wrapErrorFromHint hint . f) id hints
+
formularizeType :: MonadWriter Eqns m => Type -> Type -> m ()
-formularizeType t1 t2 = tell $ Dual [TypeEquation t1 t2]
+formularizeType t1 t2 = tell $ Dual [TypeEquation t1 t2 []]
formularizeVarName :: MonadWriter Eqns m => VarName -> Type -> m ()
formularizeVarName x t = tell $ Dual [TypeAssertion x t]
formularizeExpr :: (MonadWriter Eqns m, MonadAlpha m, MonadError Error m) => Expr -> m Type
-formularizeExpr = \case
+formularizeExpr e = wrapHint (ExprHint e) $ case e of
Var x -> do
t <- genType
formularizeVarName x t
@@ -84,10 +111,11 @@
formularizeExpr' :: (MonadWriter Eqns m, MonadAlpha m, MonadError Error m) => Expr -> Type -> m ()
formularizeExpr' e t = do
t' <- formularizeExpr e
- formularizeType t t'
+ wrapHint (ExprHint e) $ do
+ formularizeType t t'
formularizeToplevelExpr :: (MonadWriter Eqns m, MonadAlpha m, MonadError Error m) => ToplevelExpr -> m Type
-formularizeToplevelExpr = \case
+formularizeToplevelExpr e = wrapHint (ToplevelExprHint e) $ case e of
ResultExpr e -> formularizeExpr e
ToplevelLet x t e cont -> do
formularizeVarName x t
@@ -105,21 +133,21 @@
formularizeProgram :: (MonadAlpha m, MonadError Error m) => Program -> m [Equation]
formularizeProgram prog = getDual <$> execWriterT (formularizeToplevelExpr prog)
-sortEquations :: [Equation] -> ([(Type, Type)], [(VarName, Type)])
+sortEquations :: [Equation] -> ([(Type, Type, [Hint])], [(VarName, Type)])
sortEquations = go [] []
where
go eqns' assertions [] = (eqns', assertions)
go eqns' assertions (eqn : eqns) = case eqn of
- TypeEquation t1 t2 -> go ((t1, t2) : eqns') assertions eqns
+ TypeEquation t1 t2 hints -> go ((t1, t2, hints) : eqns') assertions eqns
TypeAssertion x t -> go eqns' ((x, t) : assertions) eqns
-mergeAssertions :: [(VarName, Type)] -> [(Type, Type)]
+mergeAssertions :: [(VarName, Type)] -> [(Type, Type, [Hint])]
mergeAssertions = go M.empty []
where
go _ eqns [] = eqns
go gamma eqns ((x, t) : assertions) = case M.lookup x gamma of
Nothing -> go (M.insert x t gamma) eqns assertions
- Just t' -> go gamma ((t, t') : eqns) assertions
+ Just t' -> go gamma ((t, t', [VarHint x]) : eqns) assertions
-- | `Subst` is type substituion. It's a mapping from type variables to their actual types.
newtype Subst = Subst {unSubst :: M.Map TypeName Type}
@@ -166,9 +194,12 @@
unifyType ret1 ret2
_ -> throwInternalError $ "different type ctors " ++ formatType t1 ++ " and " ++ formatType t2
-solveEquations :: MonadError Error m => [(Type, Type)] -> m Subst
+solveEquations :: MonadError Error m => [(Type, Type, [Hint])] -> m Subst
solveEquations eqns = wrapError' "failed to solve type equations" $ do
- execStateT (mapM_ (uncurry unifyType) eqns) (Subst M.empty)
+ (`execStateT` Subst M.empty) $ do
+ forM_ eqns $ \(t1, t2, hints) -> do
+ wrapErrorFromHints hints $ do
+ unifyType t1 t2
-- | `substDefault` replaces all undetermined type variables with the given default type.
substDefault :: Type -> Type -> Type
diff --git a/src/Jikka/Core/Evaluate.hs b/src/Jikka/Core/Evaluate.hs
--- a/src/Jikka/Core/Evaluate.hs
+++ b/src/Jikka/Core/Evaluate.hs
@@ -164,6 +164,7 @@
FloorMod -> go2' valueToInt valueToInt ValInt floorMod
CeilDiv -> go2' valueToInt valueToInt ValInt ceilDiv
CeilMod -> go2' valueToInt valueToInt ValInt ceilMod
+ JustDiv -> go2' valueToInt valueToInt ValInt justDiv
Pow -> go2 valueToInt valueToInt ValInt (^)
-- advanced arithmetical functions
Abs -> go1 valueToInt ValInt abs
diff --git a/src/Jikka/Core/Format.hs b/src/Jikka/Core/Format.hs
--- a/src/Jikka/Core/Format.hs
+++ b/src/Jikka/Core/Format.hs
@@ -17,6 +17,7 @@
formatBuiltin,
formatType,
formatExpr,
+ formatToplevelExpr,
formatProgram,
)
where
@@ -161,6 +162,7 @@
FloorMod -> InfixOp "%" multPrec LeftToRight
CeilDiv -> InfixOp "/^" multPrec LeftToRight
CeilMod -> InfixOp "%^" multPrec LeftToRight
+ JustDiv -> InfixOp "/!" multPrec LeftToRight
Pow -> InfixOp "**" powerPrec RightToLeft
-- advanced arithmetical functions
Abs -> Fun "abs"
@@ -327,21 +329,24 @@
formatExpr :: Expr -> String
formatExpr = unlines . makeIndentFromMarkers 4 . lines . resolvePrec parenPrec . formatExpr'
-formatToplevelExpr :: ToplevelExpr -> [String]
-formatToplevelExpr = \case
+formatToplevelExpr' :: ToplevelExpr -> [String]
+formatToplevelExpr' = \case
ResultExpr e -> lines (resolvePrec lambdaPrec (formatExpr' e))
ToplevelLet x t e cont -> let' (unVarName x) t e cont
ToplevelLetRec f args ret e cont -> let' ("rec " ++ unVarName f ++ " " ++ formatFormalArgs args) ret e cont
- ToplevelAssert e cont -> ["assert " ++ resolvePrec parenPrec (formatExpr' e), "in"] ++ formatToplevelExpr cont
+ ToplevelAssert e cont -> ["assert " ++ resolvePrec parenPrec (formatExpr' e), "in"] ++ formatToplevelExpr' cont
where
let' s t e cont =
["let " ++ s ++ ": " ++ formatType t ++ " =", indent]
++ lines (resolvePrec parenPrec (formatExpr' e))
++ [dedent, "in"]
- ++ formatToplevelExpr cont
+ ++ formatToplevelExpr' cont
+formatToplevelExpr :: ToplevelExpr -> String
+formatToplevelExpr = unlines . makeIndentFromMarkers 4 . formatToplevelExpr'
+
formatProgram :: Program -> String
-formatProgram = unlines . makeIndentFromMarkers 4 . formatToplevelExpr
+formatProgram = formatToplevelExpr
run :: Applicative m => Program -> m Text
run = pure . pack . formatProgram
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
@@ -225,10 +225,13 @@
let indices = V.imap (\i x -> map (i,) (findIndices (x `isFreeVar`) (productExprList e))) xs
case concat (V.toList indices) of
[] -> lift $ modifySTRef c (plusArithmeticExpr (arithmeticalExprFromProductExpr e))
- [(i, j)] -> do
- let e' = e {productExprList = take j (productExprList e) ++ drop (j + 1) (productExprList e)}
- lift $ MV.modify f (plusArithmeticExpr (arithmeticalExprFromProductExpr e')) i
- _ -> MaybeT $ return Nothing
+ [(i, j)] ->
+ if productExprList e !! j == Var (xs V.! i)
+ then do
+ let e' = e {productExprList = take j (productExprList e) ++ drop (j + 1) (productExprList e)}
+ lift $ MV.modify f (plusArithmeticExpr (arithmeticalExprFromProductExpr e')) i -- k x_i
+ else MaybeT $ return Nothing -- e.g. f(x_i)
+ _ -> MaybeT $ return Nothing -- e.g. x_1 x_2
f <- V.freeze f
c <- lift $ readSTRef c
return (V.map normalizeArithmeticExpr f, normalizeArithmeticExpr c)
diff --git a/src/Jikka/Core/Language/BuiltinPatterns.hs b/src/Jikka/Core/Language/BuiltinPatterns.hs
--- a/src/Jikka/Core/Language/BuiltinPatterns.hs
+++ b/src/Jikka/Core/Language/BuiltinPatterns.hs
@@ -32,6 +32,8 @@
pattern CeilMod' e1 e2 = AppBuiltin2 CeilMod e1 e2
+pattern JustDiv' e1 e2 = AppBuiltin2 JustDiv e1 e2
+
pattern Pow' e1 e2 = AppBuiltin2 Pow e1 e2
-- advanced arithmetical functions
diff --git a/src/Jikka/Core/Language/Expr.hs b/src/Jikka/Core/Language/Expr.hs
--- a/src/Jikka/Core/Language/Expr.hs
+++ b/src/Jikka/Core/Language/Expr.hs
@@ -90,6 +90,8 @@
CeilDiv
| -- | \(: \int \to \int \to \int\)
CeilMod
+ | -- | divison which has no remainder \(: \int \to \int \to \int\)
+ JustDiv
| -- | \(: \int \to \int \to \int\)
Pow
| -- advanced arithmetical functions
diff --git a/src/Jikka/Core/Language/ModuloExpr.hs b/src/Jikka/Core/Language/ModuloExpr.hs
new file mode 100644
--- /dev/null
+++ b/src/Jikka/Core/Language/ModuloExpr.hs
@@ -0,0 +1,386 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Jikka.Core.Language.ModuloExpr
+ ( -- * Basic functions
+ ModuloExpr,
+ parseModuloExpr,
+ formatTopModuloExpr,
+ formatBottomModuloExpr,
+ integerModuloExpr,
+ negateModuloExpr,
+ plusModuloExpr,
+ minusModuloExpr,
+ multModuloExpr,
+ isZeroModuloExpr,
+ isOneModuloExpr,
+ moduloOfModuloExpr,
+ arithmeticExprFromModuloExpr,
+
+ -- * Utilities
+ Modulo (..),
+ formatModulo,
+ isModulo,
+ )
+where
+
+import Data.List
+import Jikka.Common.Error
+import Jikka.Core.Format (formatExpr)
+import Jikka.Core.Language.ArithmeticExpr
+import Jikka.Core.Language.BuiltinPatterns
+import Jikka.Core.Language.Expr
+import Jikka.Core.Language.Runtime (modinv, modpow)
+import Jikka.Core.Language.Util
+
+-- | `Modulo` is just a newtype to avoid mistakes that swapping left and right of mod-op.
+newtype Modulo = Modulo {unModulo :: Expr}
+ deriving (Eq, Ord, Show, Read)
+
+formatModulo :: Modulo -> String
+formatModulo = formatExpr . unModulo
+
+isModulo :: Expr -> Modulo -> Bool
+isModulo e (Modulo m) = case e of
+ FloorMod' _ m' -> m' == m
+ ModNegate' _ m' -> m' == m
+ ModPlus' _ _ m' -> m' == m
+ ModMinus' _ _ m' -> m' == m
+ ModMult' _ _ m' -> m' == m
+ ModInv' _ m' -> m' == m
+ ModPow' _ _ m' -> m' == m
+ VecFloorMod' _ _ m' -> m' == m
+ MatFloorMod' _ _ _ m' -> m' == m
+ ModMatAp' _ _ _ _ m' -> m' == m
+ ModMatAdd' _ _ _ _ m' -> m' == m
+ ModMatMul' _ _ _ _ _ m' -> m' == m
+ ModMatPow' _ _ _ m' -> m' == m
+ ModSum' _ m' -> m' == m
+ ModProduct' _ m' -> m' == m
+ LitInt' n -> case m of
+ LitInt' m -> 0 <= n && n < m
+ _ -> False
+ Proj' ts _ e | isVectorTy' ts -> e `isModulo` Modulo m
+ Proj' ts _ e | isMatrixTy' ts -> e `isModulo` Modulo m
+ Map' _ _ f _ -> f `isModulo` Modulo m
+ Lam _ _ body -> body `isModulo` Modulo m
+ e@(App _ _) -> case curryApp e of
+ (e@(Lam _ _ _), _) -> e `isModulo` Modulo m
+ (Tuple' ts, es) | isVectorTy' ts -> all (`isModulo` Modulo m) es
+ (Tuple' ts, es) | isMatrixTy' ts -> all (`isModulo` Modulo m) es
+ _ -> False
+ _ -> False
+
+data ProductExpr = ProductExpr
+ { productExprConst :: Integer,
+ productExprList :: [Expr],
+ productExprInvList :: [Expr]
+ }
+ deriving (Eq, Ord, Show, Read)
+
+data SumExpr = SumExpr
+ { sumExprList :: [ProductExpr],
+ sumExprConst :: Integer
+ }
+ deriving (Eq, Ord, Show, Read)
+
+data ModuloExpr = ModuloExpr
+ { unModuloExpr :: SumExpr,
+ modulo :: Modulo
+ }
+ deriving (Show)
+
+instance Eq ModuloExpr where
+ e1 == e2 = unModuloExpr (normalizeModuloExpr e1) == unModuloExpr (normalizeModuloExpr e2) && modulo e1 == modulo e2
+
+instance Ord ModuloExpr where
+ e1 `compare` e2 = (unModuloExpr (normalizeModuloExpr e1), modulo e1) `compare` (unModuloExpr (normalizeModuloExpr e2), modulo e2)
+
+negateProductExpr :: ProductExpr -> ProductExpr
+negateProductExpr e = e {productExprConst = negate (productExprConst e)}
+
+multProductExpr :: ProductExpr -> ProductExpr -> ProductExpr
+multProductExpr e1 e2 =
+ ProductExpr
+ { productExprConst = productExprConst e1 * productExprConst e2,
+ productExprList = productExprList e1 ++ productExprList e2,
+ productExprInvList = productExprInvList e1 ++ productExprInvList e2
+ }
+
+powProductExpr :: Integer -> ProductExpr -> Integer -> ProductExpr
+powProductExpr m e k =
+ ProductExpr
+ { productExprConst = fromSuccess $ modpow (productExprConst e) k m,
+ productExprList = map (\e -> ModPow' e (LitInt' k) (LitInt' m)) (productExprList e),
+ productExprInvList = map (\e -> ModPow' e (LitInt' k) (LitInt' m)) (productExprInvList e)
+ }
+
+partitionMaybe :: (a -> Maybe b) -> [a] -> ([b], [a])
+partitionMaybe f = \case
+ [] -> ([], [])
+ x : xs ->
+ let (ys, xs') = partitionMaybe f xs
+ in case f x of
+ Just y -> (y : ys, xs')
+ Nothing -> (ys, x : xs')
+
+fromLitInt :: Expr -> Maybe Integer
+fromLitInt (LitInt' k) = Just k
+fromLitInt _ = Nothing
+
+invProductExpr :: Modulo -> ProductExpr -> ProductExpr
+invProductExpr m e =
+ let (invKs, invList) = partitionMaybe fromLitInt (productExprInvList e)
+ e' =
+ ProductExpr
+ { productExprConst = product invKs,
+ productExprList = LitInt' (productExprConst e) : invList,
+ productExprInvList = productExprList e
+ }
+ in case m of
+ Modulo (LitInt' m) -> case modinv (productExprConst e) m of
+ Right k ->
+ ProductExpr
+ { productExprConst = (k * product invKs) `mod` m,
+ productExprList = invList,
+ productExprInvList = productExprList e
+ }
+ _ -> e'
+ _ -> e'
+
+isInteger :: Modulo -> Bool
+isInteger (Modulo (LitInt' _)) = True
+isInteger _ = False
+
+moduloToInteger :: Modulo -> Integer
+moduloToInteger (Modulo (LitInt' m)) = m
+moduloToInteger m = error $ "Jikka.Core.Language.ModuloExpr.moduloToInteger: modulo is not an integer" ++ formatModulo m
+
+parseProductExpr :: Modulo -> Expr -> ProductExpr
+parseProductExpr m = \case
+ LitInt' n -> ProductExpr {productExprConst = n, productExprList = [], productExprInvList = []}
+ Negate' e -> negateProductExpr (parseProductExpr m e)
+ Mult' e1 e2 -> multProductExpr (parseProductExpr m e1) (parseProductExpr m e2)
+ JustDiv' e1 e2 -> multProductExpr (parseProductExpr m e1) (invProductExpr m (parseProductExpr m e2))
+ Pow' e1 (LitInt' k) | isInteger m -> powProductExpr (moduloToInteger m) (parseProductExpr m e1) k
+ ModNegate' e m' | Modulo m' == m -> negateProductExpr (parseProductExpr m e)
+ ModMult' e1 e2 m' | Modulo m' == m -> multProductExpr (parseProductExpr m e1) (parseProductExpr m e2)
+ ModPow' e1 (LitInt' k) (LitInt' m') | Modulo (LitInt' m') == m -> powProductExpr m' (parseProductExpr m e1) k
+ ModInv' e1 m' | Modulo m' == m -> invProductExpr m (parseProductExpr m e1)
+ e -> ProductExpr {productExprConst = 1, productExprList = [e], productExprInvList = []}
+
+sumExprFromProductExpr :: ProductExpr -> SumExpr
+sumExprFromProductExpr e =
+ SumExpr
+ { sumExprList = [e],
+ sumExprConst = 0
+ }
+
+integerSumExpr :: Integer -> SumExpr
+integerSumExpr n =
+ SumExpr
+ { sumExprConst = n,
+ sumExprList = []
+ }
+
+integerModuloExpr :: Modulo -> Integer -> ModuloExpr
+integerModuloExpr m k = ModuloExpr (integerSumExpr k) m
+
+negateSumExpr :: SumExpr -> SumExpr
+negateSumExpr e =
+ SumExpr
+ { sumExprList = map negateProductExpr (sumExprList e),
+ sumExprConst = negate (sumExprConst e)
+ }
+
+plusSumExpr :: SumExpr -> SumExpr -> SumExpr
+plusSumExpr e1 e2 =
+ SumExpr
+ { sumExprList = sumExprList e1 ++ sumExprList e2,
+ sumExprConst = sumExprConst e1 + sumExprConst e2
+ }
+
+multSumExpr :: Modulo -> SumExpr -> SumExpr -> SumExpr
+multSumExpr m e1 e2 =
+ SumExpr
+ { sumExprList =
+ let es1 = parseProductExpr m (LitInt' (sumExprConst e1)) : sumExprList e1
+ es2 = parseProductExpr m (LitInt' (sumExprConst e2)) : sumExprList e2
+ in tail $ map (uncurry multProductExpr) ((,) <$> es1 <*> es2),
+ sumExprConst = sumExprConst e1 * sumExprConst e2
+ }
+
+negateModuloExpr :: ModuloExpr -> ModuloExpr
+negateModuloExpr (ModuloExpr e m) = ModuloExpr (negateSumExpr e) m
+
+plusModuloExpr :: ModuloExpr -> ModuloExpr -> Maybe ModuloExpr
+plusModuloExpr (ModuloExpr e1 m) (ModuloExpr e2 m') | m == m' = Just $ ModuloExpr (plusSumExpr e1 e2) m
+plusModuloExpr _ _ = Nothing
+
+minusModuloExpr :: ModuloExpr -> ModuloExpr -> Maybe ModuloExpr
+minusModuloExpr (ModuloExpr e1 m) (ModuloExpr e2 m') | m == m' = Just $ ModuloExpr (plusSumExpr e1 (negateSumExpr e2)) m
+minusModuloExpr _ _ = Nothing
+
+multModuloExpr :: ModuloExpr -> ModuloExpr -> Maybe ModuloExpr
+multModuloExpr (ModuloExpr e1 m) (ModuloExpr e2 m') | m == m' = Just $ ModuloExpr (multSumExpr m e1 e2) m
+multModuloExpr _ _ = Nothing
+
+parseSumExpr :: Modulo -> Expr -> SumExpr
+parseSumExpr m = \case
+ LitInt' n -> SumExpr {sumExprList = [], sumExprConst = n}
+ Negate' e -> negateSumExpr (parseSumExpr m e)
+ Plus' e1 e2 -> plusSumExpr (parseSumExpr m e1) (parseSumExpr m e2)
+ Minus' e1 e2 -> plusSumExpr (parseSumExpr m e1) (negateSumExpr (parseSumExpr m e2))
+ Mult' e1 e2 -> multSumExpr m (parseSumExpr m e1) (parseSumExpr m e2)
+ FloorMod' e m' | Modulo m' == m -> parseSumExpr m e
+ ModNegate' e m' | Modulo m' == m -> negateSumExpr (parseSumExpr m e)
+ ModPlus' e1 e2 m' | Modulo m' == m -> plusSumExpr (parseSumExpr m e1) (parseSumExpr m e2)
+ ModMinus' e1 e2 m' | Modulo m' == m -> plusSumExpr (parseSumExpr m e1) (negateSumExpr (parseSumExpr m e2))
+ ModMult' e1 e2 m' | Modulo m' == m -> multSumExpr m (parseSumExpr m e1) (parseSumExpr m e2)
+ e -> sumExprFromProductExpr (parseProductExpr m e)
+
+getModuloFromExpr :: Expr -> Maybe Modulo
+getModuloFromExpr = \case
+ FloorMod' _ m -> Just $ Modulo m
+ ModNegate' _ m -> Just $ Modulo m
+ ModPlus' _ _ m -> Just $ Modulo m
+ ModMinus' _ _ m -> Just $ Modulo m
+ ModMult' _ _ m -> Just $ Modulo m
+ _ -> Nothing
+
+-- | `parseModuloExpr` converts a given expr to a normal form \(\sum_i \prod_j e _ {i,j}) \bmod m\).
+-- This assumes given exprs have the type \(\mathbf{int}\).
+parseModuloExpr :: Expr -> Maybe ModuloExpr
+parseModuloExpr e = do
+ m <- getModuloFromExpr e
+ return $ ModuloExpr (parseSumExpr m e) m
+
+formatTopProductExpr :: Modulo -> ProductExpr -> Expr
+formatTopProductExpr m e =
+ let k = LitInt' (productExprConst e)
+ k' e' = case productExprConst e of
+ 0 -> LitInt' 0
+ 1 -> e'
+ -1 -> Negate' e'
+ _ -> Mult' e' k
+ invList = map (`FloorMod'` unModulo m) (productExprInvList e)
+ in case productExprList e ++ invList of
+ [] -> k
+ eHead : esTail -> k' (foldl Mult' eHead esTail)
+
+formatTopSumExpr :: Modulo -> SumExpr -> Expr
+formatTopSumExpr m e = case sumExprList e of
+ [] -> LitInt' (sumExprConst e)
+ eHead : esTail ->
+ let op e'
+ | productExprConst e' > 0 = Plus'
+ | productExprConst e' < 0 = Minus'
+ | otherwise = const
+ go e1 e2 = op e2 e1 (formatTopProductExpr m (e2 {productExprConst = abs (productExprConst e2)}))
+ k' e'
+ | sumExprConst e > 0 = Plus' e' (LitInt' (sumExprConst e))
+ | sumExprConst e < 0 = Minus' e' (LitInt' (abs (sumExprConst e)))
+ | otherwise = e'
+ in k' (foldl go (formatTopProductExpr m eHead) esTail)
+
+-- | `formatTopModuloExpr` convert `ModuloExpr` to `Expr` with adding `FloorMod` at only the root.
+formatTopModuloExpr :: ModuloExpr -> Expr
+formatTopModuloExpr e = FloorMod' (formatTopSumExpr (modulo e) . unModuloExpr $ normalizeModuloExpr e) (unModulo $ modulo e)
+
+formatBottomInteger :: Modulo -> Integer -> Expr
+formatBottomInteger m k = case unModulo m of
+ LitInt' m -> LitInt' (k `mod` m)
+ m -> FloorMod' (LitInt' k) m
+
+formatBottomProductExpr :: Modulo -> ProductExpr -> Expr
+formatBottomProductExpr m e =
+ let k = formatBottomInteger m (productExprConst e)
+ k' e' = case productExprConst e of
+ 0 -> LitInt' 0
+ 1 -> e'
+ -1 -> ModNegate' e' (unModulo m)
+ _ -> ModMult' e' k (unModulo m)
+ invList = map (`ModInv'` unModulo m) (productExprInvList e)
+ list = map (\e -> if e `isModulo` m then e else FloorMod' e (unModulo m)) (productExprList e)
+ in case list ++ invList of
+ [] -> k
+ eHead : esTail -> k' (foldl (\e1 e2 -> ModMult' e1 e2 (unModulo m)) eHead esTail)
+
+formatBottomSumExpr :: Modulo -> SumExpr -> Expr
+formatBottomSumExpr m e = case sumExprList e of
+ [] -> formatBottomInteger m (sumExprConst e)
+ eHead : esTail ->
+ let go e1 e2
+ | productExprConst e2 == 0 = e1
+ | productExprConst e2 == -1 = ModMinus' e1 (formatBottomProductExpr m (e2 {productExprConst = 1})) (unModulo m)
+ | otherwise = ModPlus' e1 (formatBottomProductExpr m e2) (unModulo m)
+ plusConst e'
+ | sumExprConst e == 0 = e'
+ | otherwise = ModPlus' e' (formatBottomInteger m (sumExprConst e)) (unModulo m)
+ in plusConst (foldl go (formatBottomProductExpr m eHead) esTail)
+
+-- | `formatBottomModuloExpr` convert `ModuloExpr` to `Expr` with adding `FloorMod` at every nodes.
+formatBottomModuloExpr :: ModuloExpr -> Expr
+formatBottomModuloExpr e = formatBottomSumExpr (modulo e) . unModuloExpr $ normalizeModuloExpr e
+
+normalizeProductExpr :: Modulo -> ProductExpr -> ProductExpr
+normalizeProductExpr m e =
+ let k = case m of
+ Modulo (LitInt' m) -> productExprConst e `mod` m
+ _ -> productExprConst e
+ es =
+ if k == 0
+ then []
+ else sort (productExprList e)
+ es' =
+ if k == 0
+ then []
+ else sort (productExprInvList e)
+ in e
+ { productExprList = es,
+ productExprInvList = es',
+ productExprConst = k
+ }
+
+normalizeSumExpr :: Modulo -> SumExpr -> SumExpr
+normalizeSumExpr m e =
+ let f e = (productExprList e, productExprInvList e)
+ cmp e1 e2 = f e1 `compare` f e2
+ cmp' e1 e2 = cmp e1 e2 == EQ
+ es = sortBy cmp (map (normalizeProductExpr m) (sumExprList e))
+ es' = groupBy cmp' es
+ es'' =
+ map
+ ( \group ->
+ ProductExpr
+ { productExprConst = sum (map productExprConst group),
+ productExprList = productExprList (head group),
+ productExprInvList = productExprInvList (head group)
+ }
+ )
+ es'
+ es''' = filter (\e -> productExprConst e /= 0 && not (null (productExprList e))) es''
+ k = sum (map (\e -> if null (productExprList e) then productExprConst e else 0) es'')
+ k' = sumExprConst e + k
+ k'' = case m of
+ Modulo (LitInt' m) -> k' `mod` m
+ _ -> k'
+ in SumExpr
+ { sumExprList = es''',
+ sumExprConst = k''
+ }
+
+normalizeModuloExpr :: ModuloExpr -> ModuloExpr
+normalizeModuloExpr e = ModuloExpr (normalizeSumExpr (modulo e) (unModuloExpr e)) (modulo e)
+
+isZeroModuloExpr :: ModuloExpr -> Bool
+isZeroModuloExpr e = normalizeModuloExpr e == integerModuloExpr (modulo e) 0
+
+isOneModuloExpr :: ModuloExpr -> Bool
+isOneModuloExpr e = normalizeModuloExpr e == integerModuloExpr (modulo e) 1
+
+moduloOfModuloExpr :: ModuloExpr -> Expr
+moduloOfModuloExpr = unModulo . modulo
+
+arithmeticExprFromModuloExpr :: ModuloExpr -> ArithmeticExpr
+arithmeticExprFromModuloExpr e = parseArithmeticExpr . formatTopSumExpr (modulo e) $ unModuloExpr e
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
@@ -4,8 +4,16 @@
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
-module Jikka.Core.Language.QuasiRules where
+module Jikka.Core.Language.QuasiRules
+ ( r,
+ -- * Things which `r` uses.
+ module Jikka.Core.Language.Expr,
+ makeRewriteRule,
+ genVarName',
+ )
+where
+
import Control.Arrow
import Control.Monad.State.Strict
import Data.Data
@@ -14,6 +22,7 @@
import qualified Jikka.Core.Convert.TypeInfer as TypeInfer
import Jikka.Core.Language.Expr
import Jikka.Core.Language.RewriteRules
+import Jikka.Core.Language.Util
import Jikka.Core.Parse (parseRule)
import Language.Haskell.TH (Exp (..), Lit (..), Pat (..), Q, Stmt (..))
import qualified Language.Haskell.TH as TH
@@ -27,13 +36,6 @@
Left err -> fail $ "Jikka.Core.Language.QuasiRules.liftError: " ++ unlines (prettyError' err)
Right y -> return y
-lookupValueName :: (MonadTrans t, Monad (t Q), MonadFail (t Q)) => String -> t Q TH.Name
-lookupValueName x = do
- y <- lift $ TH.lookupValueName x
- case y of
- Nothing -> fail $ "Jikka.Core.Language.QuasiRules.lookupValueName: undefined symbol: " ++ x
- Just y -> return y
-
fromVarName :: VarName -> Q TH.Name
fromVarName (VarName x) = do
let base = takeWhile (/= '$') x
@@ -47,8 +49,29 @@
liftDataP :: Data a => a -> Q Pat
liftDataP = TH.dataToPatQ (const Nothing)
+-- | `Exp` with type `Expr`.
+type ExprExp = Exp
+
+data RenamedVarName
+ = DeclaredAtForall
+ | RenamedVar ExprExp
+ | RenamedPatLam TH.Name ExprExp
+ | RenamedExpLam ExprExp
+ | RenamedPatLet TH.Name ExprExp
+ | RenamedExpLet ExprExp
+ deriving (Eq, Ord, Show)
+
+expFromRenamedVarName :: RenamedVarName -> Maybe ExprExp
+expFromRenamedVarName = \case
+ DeclaredAtForall -> Nothing
+ RenamedVar e -> Just e
+ RenamedPatLam _ e -> Just e
+ RenamedExpLam e -> Just e
+ RenamedPatLet _ e -> Just e
+ RenamedExpLet e -> Just e
+
data Env = Env
- { vars :: [(VarName, Maybe Exp)],
+ { vars :: [(VarName, RenamedVarName)],
typeVars :: [(TypeName, TH.Name)]
}
@@ -99,14 +122,14 @@
then return WildP
else do
env <- gets vars
- case lookup x env of
+ case expFromRenamedVarName <$> lookup x env of
Just (Just y) -> do
lift [p|((== $(pure y)) -> True)|]
Just Nothing -> do
y <- lift $ fromVarName x
- modify' (\env -> env {vars = (x, Just (VarE y)) : vars env})
+ modify' (\env -> env {vars = (x, RenamedVar (VarE y)) : vars env})
return $ VarP y
- Nothing -> fail $ "Jikka.Core.Language.QuasiRules.toPatE: undefined variable: " ++ unVarName x
+ Nothing -> fail $ "Jikka.Core.Language.QuasiRules.toPatE: undefined variable (forall is required): " ++ unVarName x
Lit lit -> do
lit <- toPatL lit
lift [p|Lit $(pure lit)|]
@@ -118,14 +141,15 @@
t <- toPatT t
y <- lift $ fromVarName x
y' <- lift [e|Var $(pure (VarE y))|]
- modify' (\env -> env {vars = (x, Just y') : vars env})
+ modify' (\env -> env {vars = (x, RenamedPatLam y y') : vars env})
e <- toPatE e
lift [p|Lam $(pure (VarP y)) $(pure t) $(pure e)|]
Let x t e1 e2 -> do
t <- toPatT t
e1 <- toPatE e1
y <- lift $ fromVarName x
- modify' (\env -> env {vars = (x, Just (VarE y)) : vars env})
+ y' <- lift [e|Var $(pure (VarE y))|]
+ modify' (\env -> env {vars = (x, RenamedPatLet y y') : vars env})
e2 <- toPatE e2
lift [p|Let $(pure (VarP y)) $(pure t) $(pure e1) $(pure e2)|]
Assert e1 e2 -> do
@@ -173,12 +197,12 @@
toExpE :: Expr -> StateT Env Q ([Stmt], Exp)
toExpE e = do
- var <- lookupValueName "Var"
- genVarName <- lookupValueName "Jikka.Core.Language.Util.genVarName'"
+ var <- lift [e|Var|]
+ genVarName <- lift [e|genVarName'|]
case e of
Var x -> do
env <- gets vars
- case lookup x env of
+ case expFromRenamedVarName <$> lookup x env of
Just (Just y) -> return ([], y)
_ -> fail $ "Jikka.Core.Language.QuasiRules.toExpE: undefined variable: " ++ unVarName x
Lit lit -> do
@@ -192,19 +216,39 @@
return (stmts ++ stmts', e)
Lam x t e -> do
t <- toExpT t
- y <- lift $ fromVarName x
- modify' (\env -> env {vars = (x, Just (AppE (ConE var) (VarE y))) : vars env})
- (stmts, e) <- toExpE e
- e <- lift [e|Lam $(pure (VarE y)) $(pure t) $(pure e)|]
- return (BindS (VarP y) (VarE genVarName) : stmts, e)
+ y <- gets (lookup x . vars)
+ case y of
+ Just (RenamedPatLam y _) -> do
+ -- Use the same variable name
+ (stmts, e) <- toExpE e
+ e <- lift [e|Lam $(pure (VarE y)) $(pure t) $(pure e)|]
+ return (stmts, e)
+ Nothing -> do
+ -- Introduce a new name
+ y <- lift $ fromVarName x
+ modify' (\env -> env {vars = (x, RenamedExpLam (AppE var (VarE y))) : vars env})
+ (stmts, e) <- toExpE e
+ e <- lift [e|Lam $(pure (VarE y)) $(pure t) $(pure e)|]
+ return (BindS (VarP y) genVarName : stmts, e)
+ _ -> fail $ "Jikka.Core.Language.QuasiRules.toExpE: variable conflicts: " ++ unVarName x
Let x t e1 e2 -> do
t <- toExpT t
(stmts, e1) <- toExpE e1
- y <- lift $ fromVarName x
- modify' (\env -> env {vars = (x, Just (AppE (ConE var) (VarE y))) : vars env})
- (stmts', e2) <- toExpE e2
- e <- lift [e|Let $(pure (VarE y)) $(pure t) $(pure e1) $(pure e2)|]
- return (stmts ++ BindS (VarP y) (VarE genVarName) : stmts', e)
+ y <- gets (lookup x . vars)
+ case y of
+ Just (RenamedPatLet y _) -> do
+ -- Use the same variable name
+ (stmts', e2) <- toExpE e2
+ e <- lift [e|Let $(pure (VarE y)) $(pure t) $(pure e1) $(pure e2)|]
+ return (stmts ++ stmts', e)
+ Nothing -> do
+ -- Introduce a new name
+ y <- lift $ fromVarName x
+ modify' (\env -> env {vars = (x, RenamedExpLet (AppE var (VarE y))) : vars env})
+ (stmts', e2) <- toExpE e2
+ e <- lift [e|Let $(pure (VarE y)) $(pure t) $(pure e1) $(pure e2)|]
+ return (stmts ++ BindS (VarP y) genVarName : stmts', e)
+ _ -> fail $ "Jikka.Core.Language.QuasiRules.toExpE: variable conflicts: " ++ unVarName x
Assert e1 e2 -> do
(stmts1, e1) <- toExpE e1
(stmts2, e2) <- toExpE e2
@@ -218,12 +262,12 @@
env <-
return $
Env
- { vars = map (second (const Nothing)) args,
+ { vars = map (second (const DeclaredAtForall)) args,
typeVars = []
}
(pat, env) <- runStateT (toPatE e1) env
supressUnusedMatchesWarnings <- (concat <$>) . forM (vars env) $ \case
- (_, Just e) -> do
+ (_, expFromRenamedVarName -> Just e) -> do
e <- [e|return $(pure e)|]
return [NoBindS e]
_ -> return []
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
@@ -73,7 +73,7 @@
case e' of
Just e' -> return $ Just e'
Nothing -> go ruleName dumpTrace g
- TraceRule f -> go ruleName False f
+ TraceRule f -> go ruleName True f
makeRewriteRule :: Monad m => String -> ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule name f = NamedRule name (RewriteRule f)
diff --git a/src/Jikka/Core/Language/Runtime.hs b/src/Jikka/Core/Language/Runtime.hs
--- a/src/Jikka/Core/Language/Runtime.hs
+++ b/src/Jikka/Core/Language/Runtime.hs
@@ -20,6 +20,11 @@
ceilMod _ 0 = throwRuntimeError "zero div"
ceilMod a b = return (a - ((a + b - 1) `div` b) * b)
+justDiv :: MonadError Error m => Integer -> Integer -> m Integer
+justDiv _ 0 = throwRuntimeError "zero div"
+justDiv a b | a `mod` b /= 0 = throwRuntimeError "not a just div"
+justDiv a b = return (a `div` b)
+
modinv :: MonadError Error m => Integer -> Integer -> m Integer
modinv a m | m <= 0 || a `mod` m == 0 = throwRuntimeError $ "invalid argument for inv: " ++ show (a, m)
modinv a m = go a m 0 1 1 0
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
@@ -35,6 +35,7 @@
FloorMod -> go0 $ Fun2STy IntTy
CeilDiv -> go0 $ Fun2STy IntTy
CeilMod -> go0 $ Fun2STy IntTy
+ JustDiv -> go0 $ Fun2STy IntTy
Pow -> go0 $ Fun2STy IntTy
-- advanced arithmetical functions
Abs -> go0 $ Fun1STy IntTy
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
@@ -208,6 +208,7 @@
FloorMod -> True
CeilDiv -> True
CeilMod -> True
+ JustDiv -> True
Pow -> True
-- advanced arithmetical functions
Abs -> True
@@ -300,6 +301,11 @@
SegmentTreeInitList _ -> False
SegmentTreeGetRange _ -> False
SegmentTreeSetPoint _ -> False
+
+isLiteral :: Expr -> Bool
+isLiteral = \case
+ Lit _ -> True
+ _ -> False
-- | `isConstantTimeExpr` checks whether given exprs are suitable to propagate.
isConstantTimeExpr :: Expr -> Bool
diff --git a/src/Jikka/Core/Parse/Alex.x b/src/Jikka/Core/Parse/Alex.x
--- a/src/Jikka/Core/Parse/Alex.x
+++ b/src/Jikka/Core/Parse/Alex.x
@@ -37,7 +37,7 @@
$hexdigit = [0-9a-fA-F]
$shortstringchar_single = [^ \\ \r \n ']
-$shortstringchar_double = [^ \\ \r \n ']
+$shortstringchar_double = [^ \\ \r \n "]
@stringescapeseq = $backslash .
tokens :-
@@ -90,6 +90,7 @@
"%" { tok (Operator FloorMod) }
"/^" { tok (Operator CeilDiv) }
"%^" { tok (Operator CeilMod) }
+ "/!" { tok (Operator JustDiv) }
"**" { tok (Operator Pow) }
-- boolean operators
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
@@ -89,6 +89,7 @@
-- builtins
"nil" { WithLoc _ (L.Ident "nil") }
+ "bottom" { WithLoc _ (L.Ident "bottom") }
"abs" { WithLoc _ (L.Ident "abs") }
"gcd" { WithLoc _ (L.Ident "gcd") }
"lcm" { WithLoc _ (L.Ident "lcm") }
@@ -163,6 +164,7 @@
"%" { WithLoc _ (L.Operator L.FloorMod) }
"/^" { WithLoc _ (L.Operator L.CeilDiv) }
"%^" { WithLoc _ (L.Operator L.CeilMod) }
+ "/!" { WithLoc _ (L.Operator L.JustDiv) }
"**" { WithLoc _ (L.Operator L.Pow) }
-- boolean operators
@@ -224,8 +226,9 @@
| topdecl topdecls { $1 $2 }
topdecl :: { ToplevelExpr -> ToplevelExpr }
- : "let" identifier ":" type "=" expression "in" { ToplevelLet $2 $4 $6 }
- | "let" "rec" identifier list(arg) ":" type "=" expression "in" { ToplevelLetRec $3 $4 $6 $8 }
+ : "let" identifier opt_colon_type "=" expression "in" { ToplevelLet $2 $3 $5 }
+ | "let" "rec" identifier list(arg) opt_colon_type "=" expression "in" { ToplevelLetRec $3 $4 $5 $7 }
+ | "assert" expression "in" { ToplevelAssert $2 }
-- Types
atom_type :: { Type }
@@ -246,6 +249,10 @@
: tuple_type { $1 }
| tuple_type "->" type { FunTy $1 $3 }
+opt_colon_type :: { Type }
+ : {- empty -} { underscoreTy }
+ | ":" type { $2 }
+
-- Data Structures
datastructure :: { DataStructure }
: "convex_hull_trick" { ConvexHullTrick }
@@ -280,6 +287,8 @@
| BOOLEAN { let (L.Bool p) = value $1 in LitBool p }
| "nil" { LitNil underscoreTy }
| "nil" "@" atom_type { LitNil $3 }
+ | "bottom" "<" STRING ">" { let L.String msg = value $3 in LitBottom underscoreTy msg }
+ | "bottom" "<" STRING ">" "@" atom_type { let L.String msg = value $3 in LitBottom $6 msg }
parenth_form :: { Expr }
: "(" ")" {% makeTuple [] UnitTy }
@@ -368,9 +377,38 @@
| "cht_init" { (ConvexHullTrickInit, []) }
| "cht_getmin" { (ConvexHullTrickGetMin, []) }
| "cht_insert" { (ConvexHullTrickInsert, []) }
- | "segtree_init" semigroup { (SegmentTreeInitList $2, []) }
- | "segtree_getrange" semigroup { (SegmentTreeGetRange $2, []) }
- | "segtree_setpoint" semigroup { (SegmentTreeSetPoint $2, []) }
+ | "segtree_init" "<" semigroup ">" { (SegmentTreeInitList $3, []) }
+ | "segtree_getrange" "<" semigroup ">" { (SegmentTreeGetRange $3, []) }
+ | "segtree_setpoint" "<" semigroup ">" { (SegmentTreeSetPoint $3, []) }
+ | "(" "+" ")" { (Plus, []) }
+ | "(" "-" ")" { (Minus, []) }
+ | "(" "*" ")" { (Mult, []) }
+ | "(" "/" ")" { (FloorDiv, []) }
+ | "(" "%" ")" { (FloorMod, []) }
+ | "(" "/^" ")" { (CeilDiv, []) }
+ | "(" "%^" ")" { (CeilMod, []) }
+ | "(" "/!" ")" { (JustDiv, []) }
+ | "(" "**" ")" { (Pow, []) }
+ | "(" "&&" ")" { (And, []) }
+ | "(" "||" ")" { (Or, []) }
+ | "(" "~" ")" { (BitNot, []) }
+ | "(" "&" ")" { (BitAnd, []) }
+ | "(" "|" ")" { (BitOr, []) }
+ | "(" "^" ")" { (BitXor, []) }
+ | "(" "<<" ")" { (BitLeftShift, []) }
+ | "(" ">>" ")" { (BitRightShift, []) }
+ | "(" ">" ")" { (GreaterThan, [underscoreTy]) }
+ | "(" ">" ")" "@" atom_type { (GreaterThan, [$5]) }
+ | "(" "<" ")" { (LessThan, [underscoreTy]) }
+ | "(" "<" ")" "@" atom_type { (LessThan, [$5]) }
+ | "(" "<=" ")" { (LessEqual, [underscoreTy]) }
+ | "(" "<=" ")" "@" atom_type { (LessEqual, [$5]) }
+ | "(" ">=" ")" { (GreaterEqual, [underscoreTy]) }
+ | "(" ">=" ")" "@" atom_type { (GreaterEqual, [$5]) }
+ | "(" "==" ")" { (Equal, [underscoreTy]) }
+ | "(" "==" ")" "@" atom_type { (Equal, [$5]) }
+ | "(" "/=" ")" { (NotEqual, [underscoreTy]) }
+ | "(" "/=" ")" "@" atom_type { (NotEqual, [$5]) }
-- Primaries
primary :: { Expr }
@@ -411,6 +449,7 @@
| m_expr "%" u_expr { FloorMod' $1 $3 }
| m_expr "/^" u_expr { CeilDiv' $1 $3 }
| m_expr "%^" u_expr { CeilMod' $1 $3 }
+ | m_expr "/!" u_expr { JustDiv' $1 $3 }
a_expr :: { Expr }
: m_expr { $1 }
| a_expr "+" m_expr { Plus' $1 $3 }
@@ -465,20 +504,20 @@
-- Let
let_expr :: { Expr }
- : "let" identifier ":" type "=" expression "in" expression { Let $2 $4 $6 $8 }
+ : "let" identifier opt_colon_type "=" expression "in" expression { Let $2 $3 $5 $7 }
-- Assertion
assert_expr :: { Expr }
- : "assert" expression "->" expression { Assert $2 $4 }
+ : "assert" expression "in" expression { Assert $2 $4 }
expression_nolet :: { Expr }
: or_test { $1 }
| conditional_expression { $1 }
| lambda_expr { $1 }
- | assert_expr { $1 }
expression :: { Expr }
: expression_nolet { $1 }
| let_expr { $1 }
+ | assert_expr { $1 }
-- Expression lists
expression_list :: { [Expr] }
diff --git a/src/Jikka/Core/Parse/Token.hs b/src/Jikka/Core/Parse/Token.hs
--- a/src/Jikka/Core/Parse/Token.hs
+++ b/src/Jikka/Core/Parse/Token.hs
@@ -19,6 +19,7 @@
| FloorMod
| CeilDiv
| CeilMod
+ | JustDiv
| Pow
| -- boolean operators
And
diff --git a/src/Jikka/Python/Parse/Alex.x b/src/Jikka/Python/Parse/Alex.x
--- a/src/Jikka/Python/Parse/Alex.x
+++ b/src/Jikka/Python/Parse/Alex.x
@@ -19,7 +19,7 @@
import Data.Char (chr, isHexDigit, isOctDigit)
import Jikka.Common.Error
import Jikka.Common.Location
-import Jikka.Common.Parse.JoinLines (joinLinesWithParens, removeEmptyLines)
+import Jikka.Common.Parse.JoinLines (joinLinesWithParens, putTrailingNewline, removeEmptyLines)
import Jikka.Common.Parse.OffsideRule (insertIndents)
import Jikka.Python.Parse.Token
}
@@ -42,7 +42,7 @@
$hexdigit = [0-9a-fA-F]
$shortstringchar_single = [^ \\ \r \n ']
-$shortstringchar_double = [^ \\ \r \n ']
+$shortstringchar_double = [^ \\ \r \n "]
@stringescapeseq = $backslash .
tokens :-
@@ -243,6 +243,7 @@
Left err -> throwInternalError $ "Alex says: " ++ err
Right tokens -> return tokens
tokens <- reportErrors tokens
+ tokens <- return $ putTrailingNewline (WithLoc (Loc 0 0 0) Newline) tokens
tokens <- joinLinesWithParens (`elem` [OpenParen, OpenBracket, OpenBrace]) (`elem` [CloseParen, CloseBracket, CloseBrace]) (== Newline) tokens
tokens <- return $ removeEmptyLines (== Newline) tokens
tokens <- insertIndents Indent Dedent (== Newline) tokens
diff --git a/test/Jikka/Core/Convert/CloseSumSpec.hs b/test/Jikka/Core/Convert/CloseSumSpec.hs
--- a/test/Jikka/Core/Convert/CloseSumSpec.hs
+++ b/test/Jikka/Core/Convert/CloseSumSpec.hs
@@ -39,7 +39,7 @@
IntTy
( Mult'
(Lit (LitInt 100))
- ( FloorDiv'
+ ( JustDiv'
( Mult'
(Var "n")
(Minus' (Var "n") Lit1)
diff --git a/test/Jikka/Core/Convert/CumulativeSumSpec.hs b/test/Jikka/Core/Convert/CumulativeSumSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Jikka/Core/Convert/CumulativeSumSpec.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Jikka.Core.Convert.CumulativeSumSpec
+ ( spec,
+ )
+where
+
+import Jikka.Common.Alpha
+import Jikka.Common.Error
+import Jikka.Core.Convert.CumulativeSum (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" $ do
+ let prog =
+ parseProgram'
+ [ "let rec f: int =", -- Remove distinction between top-level and non-top-level.
+ " let a: int list = range 1000",
+ " in let n: int = 500",
+ " in sum (map (fun i -> a[i]) (range n))",
+ "in f"
+ ]
+ 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"
+ ]
+ (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
diff --git a/test/Jikka/Core/Convert/KubaruToMorauSpec.hs b/test/Jikka/Core/Convert/KubaruToMorauSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Jikka/Core/Convert/KubaruToMorauSpec.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Jikka.Core.Convert.KubaruToMorauSpec
+ ( spec,
+ )
+where
+
+import Jikka.Common.Alpha
+import Jikka.Common.Error
+import qualified Jikka.Core.Convert.ConstantFolding as ConstantFolding
+import Jikka.Core.Convert.KubaruToMorau (run)
+import qualified Jikka.Core.Convert.TypeInfer as TypeInfer
+import Jikka.Core.Format (formatProgram)
+import Jikka.Core.Language.Expr
+import Jikka.Core.Parse (parseProgram)
+import Test.Hspec
+
+run' :: Program -> Either Error Program
+run' = flip evalAlphaT 0 . (ConstantFolding.run <=< run)
+
+parseProgram' :: [String] -> Program
+parseProgram' = fromSuccess . flip evalAlphaT 100 . (TypeInfer.run <=< parseProgram . unlines)
+
+spec :: Spec
+spec = describe "run" $ do
+ it "works on simple kubaru-style DP" $ do
+ let prog =
+ parseProgram'
+ [ "let k: int = 1000",
+ "in let dp1: int list = range k",
+ "in foldl (fun dp2 i ->",
+ " foldl (fun dp3 j ->",
+ " dp3[i + j + 1 <- dp3[i + j + 1] + dp3[i]]",
+ " ) dp2 (range (k - i - 1))",
+ ") dp1 (range k)"
+ ]
+ let expected =
+ parseProgram'
+ [ "let k: int = 1000",
+ "in let dp1: int list = range k",
+ "in build (fun dp3 ->",
+ " foldl (fun $1 i ->",
+ " $1 + dp3[i]",
+ " ) dp1[len dp3] (range (len dp3))",
+ ") nil k"
+ ]
+ (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
diff --git a/test/Jikka/Core/Convert/PropagateModSpec.hs b/test/Jikka/Core/Convert/PropagateModSpec.hs
--- a/test/Jikka/Core/Convert/PropagateModSpec.hs
+++ b/test/Jikka/Core/Convert/PropagateModSpec.hs
@@ -8,30 +8,41 @@
import Jikka.Common.Alpha
import Jikka.Common.Error
import Jikka.Core.Convert.PropagateMod (run)
-import Jikka.Core.Language.BuiltinPatterns
+import qualified Jikka.Core.Convert.TypeInfer as TypeInfer
+import Jikka.Core.Format (formatProgram)
import Jikka.Core.Language.Expr
+import Jikka.Core.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" $ do
- let m = LitInt' 1000000007
- let f e = FloorMod' e m
+ it "works over a function" $ do
let prog =
- ResultExpr
- ( Lam
- "y"
- IntTy
- (f (App (Lam "x" IntTy (Plus' (Mult' (Var "x") (Var "x")) (Var "x"))) (Var "y")))
- )
+ parseProgram'
+ [ "fun y ->",
+ " (fun x -> x * x + x) y % 1000000007"
+ ]
let expected =
- ResultExpr
- ( Lam
- "y"
- IntTy
- (App (Lam "x$0" IntTy (ModPlus' (ModMult' (f (Var "x$0")) (f (Var "x$0")) m) (f (Var "x$0")) m)) (Var "y"))
- )
- run' prog `shouldBe` Right expected
+ parseProgram'
+ [ "fun y ->",
+ " (fun x$0 -> modplus (x$0 % 1000000007) (modmult (x$0 % 1000000007) (x$0 % 1000000007) 1000000007) 1000000007) y"
+ ]
+ (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
+ it "works with sum" $ do
+ let prog =
+ parseProgram'
+ [ "fun xs ->",
+ " sum (map (fun x -> 2 * x) xs) % 1000000007"
+ ]
+ let expected =
+ parseProgram'
+ [ "fun xs ->",
+ " modsum (map (fun x$0 -> modmult (x$0 % 1000000007) 2 1000000007) xs) 1000000007"
+ ]
+ (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
diff --git a/test/Jikka/Core/Convert/SegmentTreeSpec.hs b/test/Jikka/Core/Convert/SegmentTreeSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Jikka/Core/Convert/SegmentTreeSpec.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Jikka.Core.Convert.SegmentTreeSpec
+ ( spec,
+ )
+where
+
+import Jikka.Common.Alpha
+import Jikka.Common.Error
+import Jikka.Core.Convert.SegmentTree (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 on int-plus semigroup" $ do
+ let prog =
+ parseProgram'
+ [ "let a1: int list = range 1000",
+ "in let rec f (k: int): int list =", -- Remove distinction between top-level and non-top-level.
+ " foldl (fun a2 i ->",
+ " a2[i + 10 <- (scanl (fun x y -> x + y) 0 a2)[i + 100]]",
+ " ) a1 (range k)",
+ "in f 100"
+ ]
+ 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"
+ ]
+ (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
diff --git a/test/Jikka/Core/Convert/SpecializeFoldlSpec.hs b/test/Jikka/Core/Convert/SpecializeFoldlSpec.hs
--- a/test/Jikka/Core/Convert/SpecializeFoldlSpec.hs
+++ b/test/Jikka/Core/Convert/SpecializeFoldlSpec.hs
@@ -5,51 +5,67 @@
import Jikka.Common.Alpha
import Jikka.Common.Error
import Jikka.Core.Convert.SpecializeFoldl (run)
-import Jikka.Core.Language.BuiltinPatterns
+import qualified Jikka.Core.Convert.TypeInfer as TypeInfer
+import Jikka.Core.Format (formatProgram)
import Jikka.Core.Language.Expr
+import Jikka.Core.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" $ do
+ it "works about sum" $ do
let prog =
- ResultExpr
- ( Lam
- "n"
- IntTy
- ( Foldl'
- IntTy
- IntTy
- ( Lam2
- "y"
- IntTy
- "x"
- IntTy
- (Plus' (Var "y") (Var "x"))
- )
- Lit0
- (Range1' (Var "n"))
- )
- )
+ parseProgram'
+ [ "fun n ->",
+ " foldl (fun y x -> y + x) 12 (range n)"
+ ]
let expected =
- ResultExpr
- ( Lam
- "n"
- IntTy
- ( Sum'
- ( Cons'
- IntTy
- Lit0
- ( Map'
- IntTy
- IntTy
- (Lam "x" IntTy (Var "x"))
- (Range1' (Var "n"))
- )
- )
- )
- )
- run' prog `shouldBe` Right expected
+ parseProgram'
+ [ "fun n ->",
+ " 12 + sum (map (fun x -> x) (range n))"
+ ]
+ (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
+ it "works about complicated sum" $ do
+ let prog =
+ parseProgram'
+ [ "fun n ->",
+ " foldl (fun y x -> 1 + 2 + y + x + 3) 0 (range n)"
+ ]
+ let expected =
+ parseProgram'
+ [ "fun n ->",
+ " 0 + sum (map (fun x -> x + 6) (range n))"
+ ]
+ (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
+ it "works about modsum" $ do
+ let prog =
+ parseProgram'
+ [ "fun n ->",
+ " foldl (fun y x -> modplus y x 1000000007) 0 (range n)"
+ ]
+ let expected =
+ parseProgram'
+ [ "fun n ->",
+ " modplus 0 (modsum (map (fun x -> x) (range n)) 1000000007) 1000000007"
+ ]
+ (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
+ it "works about modsum with wrapping" $ do
+ let prog =
+ parseProgram'
+ [ "fun n init ->",
+ " foldl (fun y x -> y % 3) init (range n)"
+ ]
+ let expected =
+ parseProgram'
+ [ "fun n init ->",
+ " if (range n) == nil",
+ " then init",
+ " else modplus init (modsum (map (fun x -> 0) (range n)) 3) 3"
+ ]
+ (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
diff --git a/test/Jikka/Core/Language/ArithmeticExprSpec.hs b/test/Jikka/Core/Language/ArithmeticExprSpec.hs
--- a/test/Jikka/Core/Language/ArithmeticExprSpec.hs
+++ b/test/Jikka/Core/Language/ArithmeticExprSpec.hs
@@ -22,6 +22,11 @@
let f = V.fromList [parseArithmeticExpr (LitInt' 2), parseArithmeticExpr (LitInt' 3)]
let c = parseArithmeticExpr (LitInt' (-10))
makeVectorFromArithmeticExpr xs e `shouldBe` Just (f, c)
+ it "fails with modulo" $ do
+ -- See https://github.com/kmyk/Jikka/issues/173
+ let xs = V.singleton "x"
+ let e = parseArithmeticExpr (FloorMod' (Var "x") (LitInt' 3))
+ makeVectorFromArithmeticExpr xs e `shouldBe` Nothing
describe "normalizeArithmeticExpr" $ do
it "works" $ do
let e = Plus' (LitInt' 2) (Plus' (Var "a") (LitInt' (-2)))
diff --git a/test/Jikka/Python/Parse/AlexSpec.hs b/test/Jikka/Python/Parse/AlexSpec.hs
--- a/test/Jikka/Python/Parse/AlexSpec.hs
+++ b/test/Jikka/Python/Parse/AlexSpec.hs
@@ -20,17 +20,17 @@
spec = describe "run" $ do
it "works" $ do
let input = "abc ** 123"
- let tokens = [Ident "abc", PowOp, Int 123]
+ let tokens = [Ident "abc", PowOp, Int 123, Newline]
run' input `shouldBe` Right tokens
it "puts 1-based position info" $ do
let input = "abc def\n123"
- let tokens = [WithLoc (Loc 1 1 3) $ Ident "abc", WithLoc (Loc 1 5 3) Def, WithLoc (Loc 1 8 1) Newline, WithLoc (Loc 2 1 3) $ Int 123]
+ let tokens = [WithLoc (Loc 1 1 3) $ Ident "abc", WithLoc (Loc 1 5 3) Def, WithLoc (Loc 1 8 1) Newline, WithLoc (Loc 2 1 3) $ Int 123, WithLoc (Loc 0 0 0) Newline]
run input `shouldBe` Right tokens
it "inserts tokens" $ do
let input = "if:\n return"
- let tokens = [If, Colon, Newline, Indent, Return, Dedent]
+ let tokens = [If, Colon, Newline, Indent, Return, Newline, Dedent]
run' input `shouldBe` Right tokens
it "uses the longest match" $ do
let input = "i in int ints"
- let tokens = [Ident "i", In, Ident "int", Ident "ints"]
+ let tokens = [Ident "i", In, Ident "int", Ident "ints", Newline]
run' input `shouldBe` Right tokens
diff --git a/test/Jikka/Python/ParseSpec.hs b/test/Jikka/Python/ParseSpec.hs
--- a/test/Jikka/Python/ParseSpec.hs
+++ b/test/Jikka/Python/ParseSpec.hs
@@ -16,15 +16,24 @@
at :: a -> (Int, Int, Int) -> WithLoc a
at a (y, x, width) = WithLoc (Loc y x width) a
-run' :: [String] -> Either Error Program
-run' lines = run "test.py" (pack $ unlines lines)
+run' :: String -> Either Error Program
+run' prog = run "test.py" (pack prog)
spec :: Spec
spec = describe "run" $ do
it "works" $ do
let input =
- [ "def solve() -> int:",
- " return 42"
- ]
+ unlines
+ [ "def solve() -> int:",
+ " return 42"
+ ]
+ let parsed = [FunctionDef ("solve" `at` (1, 5, 5)) emptyArguments [Return (Just (constIntExp 42 `at` (2, 12, 2))) `at` (2, 5, 6)] [] (Just (Name ("int" `at` (1, 16, 3)) `at` (1, 16, 3))) `at` (1, 1, 3)]
+ run' input `shouldBe` Right parsed
+ it "works even without trailing newline" $ do
+ let input = "def solve() -> int:\n return 42"
+ let parsed = [FunctionDef ("solve" `at` (1, 5, 5)) emptyArguments [Return (Just (constIntExp 42 `at` (2, 12, 2))) `at` (2, 5, 6)] [] (Just (Name ("int" `at` (1, 16, 3)) `at` (1, 16, 3))) `at` (1, 1, 3)]
+ run' input `shouldBe` Right parsed
+ it "works even with CRLF" $ do
+ let input = "def solve() -> int:\r\n return 42\r\n"
let parsed = [FunctionDef ("solve" `at` (1, 5, 5)) emptyArguments [Return (Just (constIntExp 42 `at` (2, 12, 2))) `at` (2, 5, 6)] [] (Just (Name ("int" `at` (1, 16, 3)) `at` (1, 16, 3))) `at` (1, 1, 3)]
run' input `shouldBe` Right parsed