Merge pull request #18 from kmyk/develop

v5.0.3.0

CHANGELOG.md

@@ -1,7 +1,13 @@
 # Changelog for Jikka
 
+## 2021-06-23: v5.0.3.0
+
+Now the conversion from restricted Python to core works.
+
 ## 2021-06-19: v5.0.2.0
 
+Most conversions in restricted Python are implemented.
+
 ## 2020-12-03: v5.0.1.0
 
 `v5.0.1.0` is the first version of the third prototype.

examples/test.sh

@@ -1,5 +1,6 @@
 #!/bin/bash
 set -ex
 for f in examples/*.in ; do
-    diff <(stack --system-ghc run execute ${f%.in}.py < $f) ${f%.in}.out
+    diff <(stack --system-ghc run -- execute --target rpython ${f%.in}.py < $f) ${f%.in}.out
+    diff <(stack --system-ghc run -- execute --target core ${f%.in}.py < $f) ${f%.in}.out
 done

package.yaml

@@ -1,5 +1,5 @@
 name:                Jikka
-version:             5.0.2.0
+version:             5.0.3.0
 github:              "kmyk/Jikka"
 license:             Apache
 author:              "Kimiyuki Onaka"

src/Jikka/CPlusPlus/Convert.hs

@@ -0,0 +1,18 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+module Jikka.CPlusPlus.Convert
+  ( run,
+  )
+where
+
+import qualified Jikka.CPlusPlus.Convert.FromCore as FromCore
+import qualified Jikka.CPlusPlus.Language.Expr as Y
+import Jikka.Common.Alpha
+import Jikka.Common.Error
+import qualified Jikka.Core.Convert.ANormal as ANormal
+import qualified Jikka.Core.Language.Expr as X
+
+run :: (MonadAlpha m, MonadError Error m) => X.Program -> m Y.Program
+run prog = do
+  prog <- ANormal.run prog
+  FromCore.run prog

src/Jikka/CPlusPlus/Convert/FromCore.hs

@@ -24,21 +24,37 @@ import Jikka.Common.Error
 import qualified Jikka.Core.Language.Beta as X
 import qualified Jikka.Core.Language.BuiltinPatterns as X
 import qualified Jikka.Core.Language.Expr as X
-import qualified Jikka.Core.Language.Lint as X
+import qualified Jikka.Core.Language.TypeCheck as X
 
 --------------------------------------------------------------------------------
 -- monad
 
-newFreshName :: MonadAlpha m => String -> String -> m String
-newFreshName base hint = do
+data NameKind
+  = LocalNameKind
+  | LocalArgumentNameKind
+  | ConstantNameKind
+  | FunctionNameKind
+  | ArgumentNameKind
+  deriving (Eq, Ord, Show, Read)
+
+fromNameKind :: NameKind -> String
+fromNameKind = \case
+  LocalNameKind -> "x"
+  LocalArgumentNameKind -> "b"
+  ConstantNameKind -> "c"
+  FunctionNameKind -> "f"
+  ArgumentNameKind -> "a"
+
+newFreshName :: MonadAlpha m => NameKind -> String -> m Y.VarName
+newFreshName kind hint = do
   i <- nextCounter
-  let suffix = case takeWhile (\c -> isAlphaNum c || c == '_') hint of
-        "" -> ""
-        hint' -> "_" ++ hint'
-  return (base ++ show i ++ suffix)
+  let prefix = case takeWhile (\c -> isAlphaNum c || c == '_') hint of
+        "" -> fromNameKind kind
+        hint' -> hint' ++ "_"
+  return (Y.VarName (prefix ++ show i))
 
-renameVarName :: MonadAlpha m => String -> X.VarName -> m Y.VarName
-renameVarName kind x = Y.VarName <$> newFreshName kind (X.unVarName x)
+renameVarName :: MonadAlpha m => NameKind -> X.VarName -> m Y.VarName
+renameVarName kind x = newFreshName kind (X.unVarName x)
 
 type Env = [(X.VarName, X.Type, Y.VarName)]
 
@@ -62,11 +78,14 @@ runType = \case
   X.TupleTy ts -> Y.TyTuple <$> mapM runType ts
   t@X.FunTy {} -> throwInternalError $ "function type appears at invalid place: " ++ show t
 
-runLiteral :: MonadError Error m => X.Literal -> m Y.Literal
+runLiteral :: MonadError Error m => X.Literal -> m Y.Expr
 runLiteral = \case
   X.LitBuiltin builtin -> throwInternalError $ "cannot use builtin functaions as values: " ++ show builtin
-  X.LitInt n -> return $ Y.LitInt64 n
-  X.LitBool p -> return $ Y.LitBool p
+  X.LitInt n -> return $ Y.Lit (Y.LitInt64 n)
+  X.LitBool p -> return $ Y.Lit (Y.LitBool p)
+  X.LitNil t -> do
+    t <- runType t
+    return $ Y.Call (Y.Function "std::vector" [t]) []
 
 runAppBuiltin :: MonadError Error m => X.Builtin -> [Y.Expr] -> m Y.Expr
 runAppBuiltin f args = case (f, args) of
@@ -88,8 +107,12 @@ runAppBuiltin f args = case (f, args) of
   (X.Abs, [e]) -> return $ Y.Call (Y.Function "std::abs" []) [e]
   (X.Gcd, [e1, e2]) -> return $ Y.Call (Y.Function "std::gcd" []) [e1, e2]
   (X.Lcm, [e1, e2]) -> return $ Y.Call (Y.Function "std::lcm" []) [e1, e2]
-  (X.Min, [e1, e2]) -> return $ Y.Call (Y.Function "std::min" []) [e1, e2]
-  (X.Max, [e1, e2]) -> return $ Y.Call (Y.Function "std::max" []) [e1, e2]
+  (X.Min2 t, [e1, e2]) -> do
+    t <- runType t
+    return $ Y.Call (Y.Function "std::min" [t]) [e1, e2]
+  (X.Max2 t, [e1, e2]) -> do
+    t <- runType t
+    return $ Y.Call (Y.Function "std::max" [t]) [e1, e2]
   -- logical functions
   (X.Not, [e]) -> return $ Y.UnOp Y.Not e
   (X.And, [e1, e2]) -> return $ Y.BinOp Y.And e1 e2
@@ -104,8 +127,8 @@ runAppBuiltin f args = case (f, args) of
   (X.BitLeftShift, [e1, e2]) -> return $ Y.BinOp Y.BitLeftShift e1 e2
   (X.BitRightShift, [e1, e2]) -> return $ Y.BinOp Y.BitRightShift e1 e2
   -- modular functions
-  (X.Inv, [e1, e2]) -> return $ Y.Call (Y.Function "std::modinv" []) [e1, e2]
-  (X.PowMod, [e1, e2, e3]) -> return $ Y.Call (Y.Function "std::modpow" []) [e1, e2, e3]
+  (X.ModInv, [e1, e2]) -> return $ Y.Call (Y.Function "std::modinv" []) [e1, e2]
+  (X.ModPow, [e1, e2, e3]) -> return $ Y.Call (Y.Function "std::modpow" []) [e1, e2, e3]
   -- list functions
   (X.Len _, [e]) -> return $ Y.Cast Y.TyInt64 (Y.Call (Y.Method e "size") [])
   (X.Tabulate t, [n, f]) -> do
@@ -118,10 +141,18 @@ runAppBuiltin f args = case (f, args) of
   (X.At _, [e1, e2]) -> return $ Y.At e1 e2
   (X.Sum, [e]) -> return $ Y.Call (Y.Function "jikka::sum" []) [e]
   (X.Product, [e]) -> return $ Y.Call (Y.Function "jikka::product" []) [e]
-  (X.Min1, [e]) -> return $ Y.Call (Y.Function "jikka::minimum" []) [e]
-  (X.Max1, [e]) -> return $ Y.Call (Y.Function "jikka::maximum" []) [e]
-  (X.ArgMin, [e]) -> return $ Y.Call (Y.Function "jikka::argmin" []) [e]
-  (X.ArgMax, [e]) -> return $ Y.Call (Y.Function "jikka::argmax" []) [e]
+  (X.Min1 t, [e]) -> do
+    t <- runType t
+    return $ Y.Call (Y.Function "jikka::minimum" [t]) [e]
+  (X.Max1 t, [e]) -> do
+    t <- runType t
+    return $ Y.Call (Y.Function "jikka::maximum" [t]) [e]
+  (X.ArgMin t, [e]) -> do
+    t <- runType t
+    return $ Y.Call (Y.Function "jikka::argmin" [t]) [e]
+  (X.ArgMax t, [e]) -> do
+    t <- runType t
+    return $ Y.Call (Y.Function "jikka::argmax" [t]) [e]
   (X.All, [e]) -> return $ Y.Call (Y.Function "jikka::all" []) [e]
   (X.Any, [e]) -> return $ Y.Call (Y.Function "jikka::any" []) [e]
   (X.Sorted t, [e]) -> do
@@ -134,12 +165,11 @@ runAppBuiltin f args = case (f, args) of
   (X.Range1, [e]) -> return $ Y.Call (Y.Function "jikka::range" []) [e]
   (X.Range2, [e1, e2]) -> return $ Y.Call (Y.Function "jikka::range" []) [e1, e2]
   (X.Range3, [e1, e2, e3]) -> return $ Y.Call (Y.Function "jikka::range" []) [e1, e2, e3]
-  -- arithmetical relations
-  (X.LessThan, [e1, e2]) -> return $ Y.BinOp Y.LessThan e1 e2
-  (X.LessEqual, [e1, e2]) -> return $ Y.BinOp Y.LessEqual e1 e2
-  (X.GreaterThan, [e1, e2]) -> return $ Y.BinOp Y.GreaterThan e1 e2
-  (X.GreaterEqual, [e1, e2]) -> return $ Y.BinOp Y.GreaterEqual e1 e2
-  -- equality relations (polymorphic)
+  -- comparison
+  (X.LessThan _, [e1, e2]) -> return $ Y.BinOp Y.LessThan e1 e2
+  (X.LessEqual _, [e1, e2]) -> return $ Y.BinOp Y.LessEqual e1 e2
+  (X.GreaterThan _, [e1, e2]) -> return $ Y.BinOp Y.GreaterThan e1 e2
+  (X.GreaterEqual _, [e1, e2]) -> return $ Y.BinOp Y.GreaterEqual e1 e2
   (X.Equal _, [e1, e2]) -> return $ Y.BinOp Y.Equal e1 e2
   (X.NotEqual _, [e1, e2]) -> return $ Y.BinOp Y.NotEqual e1 e2
   -- combinational functions
@@ -152,7 +182,7 @@ runAppBuiltin f args = case (f, args) of
 runExpr :: (MonadAlpha m, MonadError Error m) => Env -> X.Expr -> m Y.Expr
 runExpr env = \case
   X.Var x -> Y.Var <$> lookupVarName env x
-  X.Lit lit -> Y.Lit <$> runLiteral lit
+  X.Lit lit -> runLiteral lit
   X.App f args -> do
     args <- mapM (runExpr env) args
     case f of
@@ -162,7 +192,7 @@ runExpr env = \case
         return $ Y.Call (Y.Callable e) args
   X.Lam args e -> do
     args <- forM args $ \(x, t) -> do
-      y <- renameVarName "b" x
+      y <- renameVarName LocalArgumentNameKind x
       return (x, t, y)
     let env' = reverse args ++ env
     args <- forM args $ \(_, t, y) -> do
@@ -176,7 +206,7 @@ runExpr env = \case
 runExprToStatements :: (MonadAlpha m, MonadError Error m) => Env -> X.Expr -> m [Y.Statement]
 runExprToStatements env = \case
   X.Let x t e1 e2 -> do
-    y <- renameVarName "x" x
+    y <- renameVarName LocalNameKind x
     t' <- runType t
     e1 <- runExpr env e1
     e2 <- runExprToStatements ((x, t, y) : env) e2
@@ -194,7 +224,7 @@ runToplevelFunDef :: (MonadAlpha m, MonadError Error m) => Env -> Y.VarName -> [
 runToplevelFunDef env f args ret body = do
   ret <- runType ret
   args <- forM args $ \(x, t) -> do
-    y <- renameVarName "a" x
+    y <- renameVarName ArgumentNameKind x
     return (x, t, y)
   body <- runExprToStatements (reverse args ++ env) body
   args <- forM args $ \(_, t, y) -> do
@@ -217,20 +247,22 @@ runToplevelExpr env = \case
         let f = Y.VarName "solve"
         args <- forM ts $ \t -> do
           t <- runType t
-          y <- Y.VarName <$> newFreshName "a" ""
+          y <- newFreshName ArgumentNameKind ""
           return (t, y)
         ret <- runType ret
         e <- runExpr env e
         let body = [Y.Return (Y.Call (Y.Callable e) (map (Y.Var . snd) args))]
         return [Y.FunDef ret f args body]
       _ -> runToplevelVarDef env (Y.VarName "ans") t e
-  X.ToplevelLet rec f args ret body cont -> do
-    g <- renameVarName "f" f
+  X.ToplevelLet x t e cont -> do
+    y <- renameVarName ConstantNameKind x
+    stmt <- runToplevelVarDef env y t e
+    cont <- runToplevelExpr ((x, t, y) : env) cont
+    return $ stmt ++ cont
+  X.ToplevelLetRec f args ret body cont -> do
+    g <- renameVarName FunctionNameKind f
     let t = X.FunTy (map snd args) ret
-    stmt <- case (rec, args) of
-      (X.NonRec, []) -> runToplevelVarDef env g ret body
-      (X.NonRec, _) -> runToplevelFunDef env g args ret body
-      (X.Rec, _) -> runToplevelFunDef ((f, t, g) : env) g args ret body
+    stmt <- runToplevelFunDef ((f, t, g) : env) g args ret body
     cont <- runToplevelExpr ((f, t, g) : env) cont
     return $ stmt ++ cont
 

src/Jikka/Core/Convert/ANormal.hs

@@ -16,21 +16,22 @@ where
 
 import Jikka.Common.Alpha (MonadAlpha)
 import Jikka.Common.Error
-import Jikka.Core.Convert.Alpha (gensym)
 import qualified Jikka.Core.Convert.Alpha as Alpha (runProgram)
 import Jikka.Core.Language.Expr
-import Jikka.Core.Language.Lint (TypeEnv, typecheckExpr, typecheckProgram')
+import Jikka.Core.Language.Lint
+import Jikka.Core.Language.TypeCheck
+import Jikka.Core.Language.Util
 
 destruct :: (MonadAlpha m, MonadError Error m) => TypeEnv -> Expr -> m (TypeEnv, Expr -> Expr, Expr)
 destruct env = \case
   e@Var {} -> return (env, id, e)
   e@Lit {} -> return (env, id, e)
   e@App {} -> do
-    x <- gensym
+    x <- genVarName'
     t <- typecheckExpr env e
     return ((x, t) : env, Let x t e, Var x)
   e@Lam {} -> do
-    x <- gensym
+    x <- genVarName'
     t <- typecheckExpr env e
     return ((x, t) : env, Let x t e, Var x)
   Let x t e1 e2 -> do
@@ -72,16 +73,19 @@ runExpr env = \case
 runToplevelExpr :: (MonadAlpha m, MonadError Error m) => TypeEnv -> ToplevelExpr -> m ToplevelExpr
 runToplevelExpr env = \case
   ResultExpr e -> ResultExpr <$> runExpr env e
-  ToplevelLet rec f args ret body cont -> do
+  ToplevelLet x t e cont -> do
+    e <- runExpr env e
+    cont <- runToplevelExpr ((x, t) : env) cont
+    return $ ToplevelLet x t e cont
+  ToplevelLetRec f args ret body cont -> do
     let t = FunTy (map snd args) ret
-    body <- case rec of
-      NonRec -> runExpr (reverse args ++ env) body
-      Rec -> runExpr (reverse args ++ (f, t) : env) body
+    body <- runExpr (reverse args ++ (f, t) : env) body
     cont <- runToplevelExpr ((f, t) : env) cont
-    return $ ToplevelLet rec f args ret body cont
+    return $ ToplevelLetRec f args ret body cont
 
 run :: (MonadAlpha m, MonadError Error m) => Program -> m Program
-run prog = do
+run prog = wrapError' "Jikka.Core.Convert.ANormal" $ do
   prog <- Alpha.runProgram prog
   prog <- runToplevelExpr [] prog
-  typecheckProgram' prog
+  ensureWellTyped prog
+  return prog

src/Jikka/Core/Convert/Alpha.hs

@@ -17,21 +17,12 @@ module Jikka.Core.Convert.Alpha where
 import Jikka.Common.Alpha
 import Jikka.Common.Error
 import Jikka.Core.Language.Expr
-import Jikka.Core.Language.Lint (typecheckProgram')
-
-gensym :: MonadAlpha m => m VarName
-gensym = rename' (VarName "") <$> nextCounter
 
 rename :: MonadAlpha m => VarName -> m VarName
-rename hint = rename' hint <$> nextCounter
-
-rename' :: VarName -> Int -> VarName
-rename' hint i =
-  let base = takeWhile (/= '@') (unVarName hint)
-   in VarName (base ++ "@" ++ show i)
-
--- -----------------------------------------------------------------------------
--- run
+rename x = do
+  let base = takeWhile (/= '$') (unVarName x)
+  i <- nextCounter
+  return $ VarName (base ++ "$" ++ show i)
 
 runExpr :: (MonadAlpha m, MonadError Error m) => [(VarName, VarName)] -> Expr -> m Expr
 runExpr env = \case
@@ -57,23 +48,25 @@ runExpr env = \case
 runToplevelExpr :: (MonadAlpha m, MonadError Error m) => [(VarName, VarName)] -> ToplevelExpr -> m ToplevelExpr
 runToplevelExpr env = \case
   ResultExpr e -> ResultExpr <$> runExpr env e
-  ToplevelLet rec f args ret body cont -> do
+  ToplevelLet x t e cont -> do
+    y <- rename x
+    e <- runExpr env e
+    cont <- runToplevelExpr ((x, y) : env) cont
+    return $ ToplevelLet y t e cont
+  ToplevelLetRec f args ret body cont -> do
     g <- rename f
     args <- forM args $ \(x, t) -> do
       y <- rename x
       return (x, y, t)
     let args1 = map (\(x, y, _) -> (x, y)) args
     let args2 = map (\(_, y, t) -> (y, t)) args
-    body <- case rec of
-      NonRec -> runExpr (args1 ++ env) body
-      Rec -> runExpr (args1 ++ (f, g) : env) body
+    body <- runExpr (args1 ++ (f, g) : env) body
     cont <- runToplevelExpr ((f, g) : env) cont
-    return $ ToplevelLet rec g args2 ret body cont
+    return $ ToplevelLetRec g args2 ret body cont
 
 runProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Program
 runProgram = runToplevelExpr []
 
 run :: (MonadAlpha m, MonadError Error m) => Program -> m Program
-run prog = do
-  prog <- runToplevelExpr [] prog
-  typecheckProgram' prog
+run prog = wrapError' "Jikka.Core.Convert.Alpha" $ do
+  runToplevelExpr [] prog