packages feed

Jikka 5.3.0.0 → 5.4.0.0

raw patch · 42 files changed

+1378/−552 lines, 42 files

Files

CHANGELOG.md view
@@ -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: <https://judge.kimiyuki.net/>+  - This judge contains example problems which Jikka can/will be able to solve.+ ## 2021-08-16: v5.3.0.0  Many bugs are removed.
Jikka.cabal view
@@ -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 <https://github.com/kmyk/Jikka> 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
runtime/include/jikka/divmod.hpp view
@@ -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
src/Jikka/CPlusPlus/Convert/FromCore.hs view
@@ -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]
src/Jikka/Common/Parse/JoinLines.hs view
@@ -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 []
src/Jikka/Core/Convert.hs view
@@ -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
src/Jikka/Core/Convert/CloseAll.hs view
@@ -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 =
src/Jikka/Core/Convert/CloseMin.hs view
@@ -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,
src/Jikka/Core/Convert/CloseSum.hs view
@@ -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
src/Jikka/Core/Convert/ConstantFolding.hs view
@@ -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
src/Jikka/Core/Convert/CumulativeSum.hs view
@@ -78,7 +78,7 @@ -- -- Before: ----- > sum (fun i -> a[i]) (range n)+-- > sum (map (fun i -> a[i]) (range n)) -- -- After: --
src/Jikka/Core/Convert/EqualitySolving.hs view
@@ -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
src/Jikka/Core/Convert/PropagateMod.hs view
@@ -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
src/Jikka/Core/Convert/SegmentTree.hs view
@@ -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.
src/Jikka/Core/Convert/ShortCutFusion.hs view
@@ -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.
src/Jikka/Core/Convert/SpecializeFoldl.hs view
@@ -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
− src/Jikka/Core/Convert/StrengthReduction.hs 
@@ -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
src/Jikka/Core/Convert/TypeInfer.hs view
@@ -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
src/Jikka/Core/Evaluate.hs view
@@ -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
src/Jikka/Core/Format.hs view
@@ -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
src/Jikka/Core/Language/ArithmeticExpr.hs view
@@ -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)
src/Jikka/Core/Language/BuiltinPatterns.hs view
@@ -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
src/Jikka/Core/Language/Expr.hs view
@@ -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
+ src/Jikka/Core/Language/ModuloExpr.hs view
@@ -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
src/Jikka/Core/Language/QuasiRules.hs view
@@ -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 []
src/Jikka/Core/Language/RewriteRules.hs view
@@ -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)
src/Jikka/Core/Language/Runtime.hs view
@@ -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
src/Jikka/Core/Language/TypeCheck.hs view
@@ -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
src/Jikka/Core/Language/Util.hs view
@@ -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
src/Jikka/Core/Parse/Alex.x view
@@ -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
src/Jikka/Core/Parse/Happy.y view
@@ -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] }
src/Jikka/Core/Parse/Token.hs view
@@ -19,6 +19,7 @@   | FloorMod   | CeilDiv   | CeilMod+  | JustDiv   | Pow   | -- boolean operators     And
src/Jikka/Python/Parse/Alex.x view
@@ -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
test/Jikka/Core/Convert/CloseSumSpec.hs view
@@ -39,7 +39,7 @@                 IntTy                 ( Mult'                     (Lit (LitInt 100))-                    ( FloorDiv'+                    ( JustDiv'                         ( Mult'                             (Var "n")                             (Minus' (Var "n") Lit1)
+ test/Jikka/Core/Convert/CumulativeSumSpec.hs view
@@ -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)
+ test/Jikka/Core/Convert/KubaruToMorauSpec.hs view
@@ -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)
test/Jikka/Core/Convert/PropagateModSpec.hs view
@@ -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)
+ test/Jikka/Core/Convert/SegmentTreeSpec.hs view
@@ -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<int_plus> a2$7.1 0 (i$8 + 100)",+              "        in (a2$7.0[i$8 + 10 <- $9], segtree_setpoint<int_plus> a2$7.1 (i$8 + 10) $9)",+              "    ) (a2$6, segtree_init<int_plus> a2$6) (range k$5)).0",+              "in f$4 100"+            ]+    (formatProgram <$> run' prog) `shouldBe` Right (formatProgram expected)
test/Jikka/Core/Convert/SpecializeFoldlSpec.hs view
@@ -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)
test/Jikka/Core/Language/ArithmeticExprSpec.hs view
@@ -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)))
test/Jikka/Python/Parse/AlexSpec.hs view
@@ -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 <indent> 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
test/Jikka/Python/ParseSpec.hs view
@@ -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