{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}

-- |
-- Module      : Jikka.Core.Language.RewriteRules
-- Description : checks and obtains types of exprs. / 式の型を検査し取得します。
-- Copyright   : (c) Kimiyuki Onaka, 2021
-- License     : Apache License 2.0
-- Maintainer  : kimiyuki95@gmail.com
-- Stability   : experimental
-- Portability : portable
module Jikka.Core.Language.TypeCheck where

import Jikka.Common.Error
import Jikka.Core.Format (formatBuiltinIsolated, formatExpr, formatType)
import Jikka.Core.Language.Expr
import Jikka.Core.Language.Util

builtinToType :: MonadError Error m => Builtin -> [Type] -> m Type
builtinToType :: Builtin -> [Type] -> m Type
builtinToType Builtin
builtin [Type]
ts =
  let go0 :: a -> m a
go0 a
f = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
f
      go1 :: (Type -> a) -> m a
go1 Type -> a
f = case [Type]
ts of
        [Type
t1] -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Type -> a
f Type
t1
        [Type]
_ -> String -> m a
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"expected 1 type argument, but got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Builtin -> [Type] -> String
formatBuiltinIsolated Builtin
builtin [Type]
ts
      go2 :: (Type -> Type -> a) -> m a
go2 Type -> Type -> a
f = case [Type]
ts of
        [Type
t1, Type
t2] -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Type -> Type -> a
f Type
t1 Type
t2
        [Type]
_ -> String -> m a
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"expected 2 type arguments, but got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Builtin -> [Type] -> String
formatBuiltinIsolated Builtin
builtin [Type]
ts
   in case Builtin
builtin of
        -- arithmetical functions
        Builtin
Negate -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun1STy Type
IntTy
        Builtin
Plus -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
Minus -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
Mult -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
FloorDiv -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
FloorMod -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
CeilDiv -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
CeilMod -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
JustDiv -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
Pow -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        -- advanced arithmetical functions
        Builtin
Abs -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun1STy Type
IntTy
        Builtin
Gcd -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
Lcm -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
Min2 -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type
Fun2STy Type
t
        Builtin
Max2 -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type
Fun2STy Type
t
        Builtin
Iterate -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type -> Type
Fun3Ty Type
IntTy (Type -> Type -> Type
FunTy Type
t Type
t) Type
t Type
t
        -- logical functions
        Builtin
Not -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun1STy Type
BoolTy
        Builtin
And -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
BoolTy
        Builtin
Or -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
BoolTy
        Builtin
Implies -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
BoolTy
        Builtin
If -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type -> Type
Fun3Ty Type
BoolTy Type
t Type
t Type
t
        -- bitwise functions
        Builtin
BitNot -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun1STy Type
IntTy
        Builtin
BitAnd -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
BitOr -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
BitXor -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
BitLeftShift -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
BitRightShift -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        -- matrix functions
        MatAp Integer
h Integer
w -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type
Fun2Ty (Integer -> Integer -> Type
matrixTy Integer
h Integer
w) (Integer -> Type
vectorTy Integer
w) (Integer -> Type
vectorTy Integer
h)
        MatZero Integer
h Integer
w -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Type
matrixTy Integer
h Integer
w
        MatOne Integer
n -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Type
matrixTy Integer
n Integer
n
        MatAdd Integer
h Integer
w -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type
Fun2Ty (Integer -> Integer -> Type
matrixTy Integer
h Integer
w) (Integer -> Integer -> Type
matrixTy Integer
h Integer
w) (Integer -> Integer -> Type
matrixTy Integer
h Integer
w)
        MatMul Integer
h Integer
n Integer
w -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type
Fun2Ty (Integer -> Integer -> Type
matrixTy Integer
h Integer
n) (Integer -> Integer -> Type
matrixTy Integer
n Integer
w) (Integer -> Integer -> Type
matrixTy Integer
h Integer
w)
        MatPow Integer
n -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type
Fun2Ty (Integer -> Integer -> Type
matrixTy Integer
n Integer
n) Type
IntTy (Integer -> Integer -> Type
matrixTy Integer
n Integer
n)
        VecFloorMod Integer
n -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type
Fun2Ty (Integer -> Type
vectorTy Integer
n) Type
IntTy (Integer -> Type
vectorTy Integer
n)
        MatFloorMod Integer
h Integer
w -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type
Fun2Ty (Integer -> Integer -> Type
matrixTy Integer
h Integer
w) Type
IntTy (Integer -> Integer -> Type
matrixTy Integer
h Integer
w)
        -- modular functions
        Builtin
ModNegate -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
ModPlus -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun3STy Type
IntTy
        Builtin
ModMinus -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun3STy Type
IntTy
        Builtin
ModMult -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun3STy Type
IntTy
        Builtin
ModInv -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
ModPow -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun3STy Type
IntTy
        ModMatAp Integer
h Integer
w -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type -> Type
Fun3Ty (Integer -> Integer -> Type
matrixTy Integer
h Integer
w) (Integer -> Type
vectorTy Integer
w) Type
IntTy (Integer -> Type
vectorTy Integer
h)
        ModMatAdd Integer
h Integer
w -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type -> Type
Fun3Ty (Integer -> Integer -> Type
matrixTy Integer
h Integer
w) (Integer -> Integer -> Type
matrixTy Integer
h Integer
w) Type
IntTy (Integer -> Integer -> Type
matrixTy Integer
h Integer
w)
        ModMatMul Integer
h Integer
n Integer
w -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type -> Type
Fun3Ty (Integer -> Integer -> Type
matrixTy Integer
h Integer
n) (Integer -> Integer -> Type
matrixTy Integer
n Integer
w) Type
IntTy (Integer -> Integer -> Type
matrixTy Integer
h Integer
w)
        ModMatPow Integer
n -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type -> Type
Fun3Ty (Integer -> Integer -> Type
matrixTy Integer
n Integer
n) Type
IntTy Type
IntTy (Integer -> Integer -> Type
matrixTy Integer
n Integer
n)
        -- list functions
        Builtin
Cons -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t (Type -> Type
ListTy Type
t) (Type -> Type
ListTy Type
t)
        Builtin
Snoc -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty (Type -> Type
ListTy Type
t) Type
t (Type -> Type
ListTy Type
t)
        Builtin
Foldl -> (Type -> Type -> Type) -> m Type
forall (m :: * -> *) a.
MonadError Error m =>
(Type -> Type -> a) -> m a
go2 ((Type -> Type -> Type) -> m Type)
-> (Type -> Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t1 Type
t2 -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Type -> Type -> Type -> Type
Fun2Ty Type
t2 Type
t1 Type
t2) Type
t2 (Type -> Type
ListTy Type
t1) Type
t2
        Builtin
Scanl -> (Type -> Type -> Type) -> m Type
forall (m :: * -> *) a.
MonadError Error m =>
(Type -> Type -> a) -> m a
go2 ((Type -> Type -> Type) -> m Type)
-> (Type -> Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t1 Type
t2 -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Type -> Type -> Type -> Type
Fun2Ty Type
t2 Type
t1 Type
t2) Type
t2 (Type -> Type
ListTy Type
t1) (Type -> Type
ListTy Type
t2)
        Builtin
Build -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Type -> Type -> Type
FunTy (Type -> Type
ListTy Type
t) Type
t) (Type -> Type
ListTy Type
t) Type
IntTy (Type -> Type
ListTy Type
t)
        Builtin
Len -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type
FunTy (Type -> Type
ListTy Type
t) Type
IntTy
        Builtin
Map -> (Type -> Type -> Type) -> m Type
forall (m :: * -> *) a.
MonadError Error m =>
(Type -> Type -> a) -> m a
go2 ((Type -> Type -> Type) -> m Type)
-> (Type -> Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t1 Type
t2 -> Type -> Type -> Type -> Type
Fun2Ty (Type -> Type -> Type
FunTy Type
t1 Type
t2) (Type -> Type
ListTy Type
t1) (Type -> Type
ListTy Type
t2)
        Builtin
Filter -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty (Type -> Type -> Type
FunTy Type
t Type
BoolTy) (Type -> Type
ListTy Type
t) (Type -> Type
ListTy Type
t)
        Builtin
At -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty (Type -> Type
ListTy Type
t) Type
IntTy Type
t
        Builtin
SetAt -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type -> Type
Fun3Ty (Type -> Type
ListTy Type
t) Type
IntTy Type
t (Type -> Type
ListTy Type
t)
        Builtin
Elem -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t (Type -> Type
ListTy Type
t) Type
BoolTy
        Builtin
Sum -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
FunLTy Type
IntTy
        Builtin
Product -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
FunLTy Type
IntTy
        Builtin
ModSum -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type
Fun2Ty (Type -> Type
ListTy Type
IntTy) Type
IntTy Type
IntTy
        Builtin
ModProduct -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type
Fun2Ty (Type -> Type
ListTy Type
IntTy) Type
IntTy Type
IntTy
        Builtin
Min1 -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type
FunLTy Type
t
        Builtin
Max1 -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type
FunLTy Type
t
        Builtin
ArgMin -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type
FunTy (Type -> Type
ListTy Type
t) Type
IntTy
        Builtin
ArgMax -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type
FunTy (Type -> Type
ListTy Type
t) Type
IntTy
        Builtin
Gcd1 -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
FunLTy Type
IntTy
        Builtin
Lcm1 -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
FunLTy Type
IntTy
        Builtin
All -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
FunLTy Type
BoolTy
        Builtin
Any -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
FunLTy Type
BoolTy
        Builtin
Sorted -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type
Fun1STy (Type -> Type
ListTy Type
t)
        Builtin
Reversed -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type
Fun1STy (Type -> Type
ListTy Type
t)
        Builtin
Range1 -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
FunTy Type
IntTy (Type -> Type
ListTy Type
IntTy)
        Builtin
Range2 -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type
Fun2Ty Type
IntTy Type
IntTy (Type -> Type
ListTy Type
IntTy)
        Builtin
Range3 -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type -> Type
Fun3Ty Type
IntTy Type
IntTy Type
IntTy (Type -> Type
ListTy Type
IntTy)
        -- tuple functions
        Builtin
Tuple -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Type -> Type
curryFunTy [Type]
ts ([Type] -> Type
TupleTy [Type]
ts)
        Proj Integer
n ->
          if Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n Bool -> Bool -> Bool
&& Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts)
            then Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
FunTy ([Type] -> Type
TupleTy [Type]
ts) ([Type]
ts [Type] -> Int -> Type
forall a. [a] -> Int -> a
!! Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)
            else String -> m Type
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwTypeError (String -> m Type) -> String -> m Type
forall a b. (a -> b) -> a -> b
$ String
"projection index is out of range: type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType ([Type] -> Type
TupleTy [Type]
ts) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", index = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
        -- comparison
        Builtin
LessThan -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
        Builtin
LessEqual -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
        Builtin
GreaterThan -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
        Builtin
GreaterEqual -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
        Builtin
Equal -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
        Builtin
NotEqual -> (Type -> Type) -> m Type
forall (m :: * -> *) a. MonadError Error m => (Type -> a) -> m a
go1 ((Type -> Type) -> m Type) -> (Type -> Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \Type
t -> Type -> Type -> Type -> Type
Fun2Ty Type
t Type
t Type
BoolTy
        -- combinational functions
        Builtin
Fact -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun1STy Type
IntTy
        Builtin
Choose -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
Permute -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        Builtin
MultiChoose -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Fun2STy Type
IntTy
        -- data structure
        Builtin
ConvexHullTrickInit -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 Type
ConvexHullTrickTy
        Builtin
ConvexHullTrickGetMin -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type
Fun2Ty Type
ConvexHullTrickTy Type
IntTy Type
IntTy
        Builtin
ConvexHullTrickInsert -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type -> Type
Fun3Ty Type
ConvexHullTrickTy Type
IntTy Type
IntTy Type
ConvexHullTrickTy
        SegmentTreeInitList Semigroup'
semigrp -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
FunTy (Type -> Type
ListTy (Semigroup' -> Type
semigroupToType Semigroup'
semigrp)) (Semigroup' -> Type
SegmentTreeTy Semigroup'
semigrp)
        SegmentTreeGetRange Semigroup'
semigrp -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type -> Type
Fun3Ty (Semigroup' -> Type
SegmentTreeTy Semigroup'
semigrp) Type
IntTy Type
IntTy (Semigroup' -> Type
semigroupToType Semigroup'
semigrp)
        SegmentTreeSetPoint Semigroup'
semigrp -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
go0 (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Type -> Type
Fun3Ty (Semigroup' -> Type
SegmentTreeTy Semigroup'
semigrp) Type
IntTy (Semigroup' -> Type
semigroupToType Semigroup'
semigrp) (Semigroup' -> Type
SegmentTreeTy Semigroup'
semigrp)

semigroupToType :: Semigroup' -> Type
semigroupToType :: Semigroup' -> Type
semigroupToType = \case
  Semigroup'
SemigroupIntPlus -> Type
IntTy
  Semigroup'
SemigroupIntMin -> Type
IntTy
  Semigroup'
SemigroupIntMax -> Type
IntTy
  Semigroup'
SemigroupIntGcd -> Type
IntTy
  Semigroup'
SemigroupIntLcm -> Type
IntTy

literalToType :: MonadError Error m => Literal -> m Type
literalToType :: Literal -> m Type
literalToType = \case
  LitBuiltin Builtin
builtin [Type]
ts -> Builtin -> [Type] -> m Type
forall (m :: * -> *).
MonadError Error m =>
Builtin -> [Type] -> m Type
builtinToType Builtin
builtin [Type]
ts
  LitInt Integer
_ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
IntTy
  LitBool Bool
_ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
BoolTy
  LitNil Type
t -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
ListTy Type
t
  LitBottom Type
t String
_ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t

arityOfBuiltin :: MonadError Error m => Builtin -> [Type] -> m Int
arityOfBuiltin :: Builtin -> [Type] -> m Int
arityOfBuiltin Builtin
builtin [Type]
ts = case Builtin
builtin of
  Builtin
Min2 -> Int -> m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
2
  Builtin
Max2 -> Int -> m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
2
  Builtin
Foldl -> Int -> m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
3
  Builtin
Iterate -> Int -> m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
3
  Builtin
At -> Int -> m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
2
  Builtin
Min1 -> Int -> m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
  Builtin
Max1 -> Int -> m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
  Proj Integer
_ -> Int -> m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
  Builtin
builtin -> [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Type] -> Int) -> (Type -> [Type]) -> Type -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Type], Type) -> [Type]
forall a b. (a, b) -> a
fst (([Type], Type) -> [Type])
-> (Type -> ([Type], Type)) -> Type -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ([Type], Type)
uncurryFunTy (Type -> Int) -> m Type -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Builtin -> [Type] -> m Type
forall (m :: * -> *).
MonadError Error m =>
Builtin -> [Type] -> m Type
builtinToType Builtin
builtin [Type]
ts

type TypeEnv = [(VarName, Type)]

-- | `typecheckExpr` checks that the given `Expr` has the correct types.
typecheckExpr :: MonadError Error m => TypeEnv -> Expr -> m Type
typecheckExpr :: TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env = \case
  Var VarName
x -> case VarName -> TypeEnv -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VarName
x TypeEnv
env of
    Maybe Type
Nothing -> String -> m Type
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m Type) -> String -> m Type
forall a b. (a -> b) -> a -> b
$ String
"undefined variable: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarName -> String
formatVarName VarName
x
    Just Type
t -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
  Lit Literal
lit -> Literal -> m Type
forall (m :: * -> *). MonadError Error m => Literal -> m Type
literalToType Literal
lit
  App Expr
f Expr
e -> do
    Type
tf <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
f
    Type
te <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e
    case Type
tf of
      FunTy Type
te' Type
ret | Type
te' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
te -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ret
      Type
_ -> String -> m Type
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m Type) -> String -> m Type
forall a b. (a -> b) -> a -> b
$ String
"wrong type funcall: function = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and argument = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", function's type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
tf String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", but argument's type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
te
  Lam VarName
x Type
t Expr
e ->
    let env' :: TypeEnv
env' = if VarName
x VarName -> VarName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName -> NameFlavour -> VarName
VarName OccName
forall a. Maybe a
Nothing NameFlavour
forall a. Maybe a
Nothing then TypeEnv
env else (VarName
x, Type
t) (VarName, Type) -> TypeEnv -> TypeEnv
forall a. a -> [a] -> [a]
: TypeEnv
env
     in Type -> Type -> Type
FunTy Type
t (Type -> Type) -> m Type -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env' Expr
e
  Let VarName
x Type
t Expr
e1 Expr
e2 -> do
    Type
t' <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e1
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
t') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      String -> m ()
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"wrong type binding: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr (VarName -> Type -> Expr -> Expr -> Expr
Let VarName
x Type
t Expr
e1 Expr
e2)
    let env' :: TypeEnv
env' = if VarName
x VarName -> VarName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName -> NameFlavour -> VarName
VarName OccName
forall a. Maybe a
Nothing NameFlavour
forall a. Maybe a
Nothing then TypeEnv
env else (VarName
x, Type
t) (VarName, Type) -> TypeEnv -> TypeEnv
forall a. a -> [a] -> [a]
: TypeEnv
env
    TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env' Expr
e2
  Assert Expr
e1 Expr
e2 -> do
    Type
t <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e1
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
BoolTy) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      String -> m ()
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"wrong type assertion: expr = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
t
    TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e2

typecheckToplevelExpr :: MonadError Error m => TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr :: TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr TypeEnv
env = \case
  ResultExpr Expr
e -> TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e
  ToplevelLet VarName
x Type
t Expr
e ToplevelExpr
cont -> do
    Type
t' <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type
t' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      String -> m ()
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"assigned type is not correct: context = (let " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarName -> String
formatVarName VarName
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in ...), expected type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", actual type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
t'
    TypeEnv -> ToplevelExpr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr ((VarName
x, Type
t) (VarName, Type) -> TypeEnv -> TypeEnv
forall a. a -> [a] -> [a]
: TypeEnv
env) ToplevelExpr
cont
  ToplevelLetRec VarName
f TypeEnv
args Type
ret Expr
body ToplevelExpr
cont -> do
    let t :: Type
t = [Type] -> Type -> Type
curryFunTy (((VarName, Type) -> Type) -> TypeEnv -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (VarName, Type) -> Type
forall a b. (a, b) -> b
snd TypeEnv
args) Type
ret
    Type
ret' <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr (TypeEnv -> TypeEnv
forall a. [a] -> [a]
reverse TypeEnv
args TypeEnv -> TypeEnv -> TypeEnv
forall a. [a] -> [a] -> [a]
++ (VarName
f, Type
t) (VarName, Type) -> TypeEnv -> TypeEnv
forall a. a -> [a] -> [a]
: TypeEnv
env) Expr
body
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type
ret' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
ret) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      String -> m ()
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"returned type is not correct: context = (let rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarName -> String
formatVarName VarName
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (((VarName, Type) -> String) -> TypeEnv -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(VarName
x, Type
t) -> VarName -> String
formatVarName VarName
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
t) TypeEnv
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
ret String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
body String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in ...), expected type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
ret String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", actual type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
ret'
    TypeEnv -> ToplevelExpr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr ((VarName
f, Type
t) (VarName, Type) -> TypeEnv -> TypeEnv
forall a. a -> [a] -> [a]
: TypeEnv
env) ToplevelExpr
cont
  ToplevelAssert Expr
e1 ToplevelExpr
e2 -> do
    Type
t <- TypeEnv -> Expr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> Expr -> m Type
typecheckExpr TypeEnv
env Expr
e1
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
BoolTy) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      String -> m ()
forall (m :: * -> *) a. MonadError Error m => String -> m a
throwInternalError (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"wrong type toplevel assertion: expr = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has type = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
formatType Type
t
    TypeEnv -> ToplevelExpr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr TypeEnv
env ToplevelExpr
e2

typecheckProgram :: MonadError Error m => Program -> m Type
typecheckProgram :: ToplevelExpr -> m Type
typecheckProgram ToplevelExpr
prog = String -> m Type -> m Type
forall (m :: * -> *) a. MonadError Error m => String -> m a -> m a
wrapError' String
"Jikka.Core.Language.TypeCheck.typecheckProgram" (m Type -> m Type) -> m Type -> m Type
forall a b. (a -> b) -> a -> b
$ do
  TypeEnv -> ToplevelExpr -> m Type
forall (m :: * -> *).
MonadError Error m =>
TypeEnv -> ToplevelExpr -> m Type
typecheckToplevelExpr [] ToplevelExpr
prog