{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module Gibbon.L1.Typecheck
  ( -- * The two main typechecker functions
    tcProg, tcExp

    -- * Helpers
  , TCError(..)
  , extendEnv, lookupVar, tcProj, checkLen, ensureEqual, ensureEqualTy, TcM
  )
where


import Control.Monad
import Control.Monad.Except
import Data.Map as M
import Data.Set as S
import qualified Data.List as L
import Data.Maybe
import Text.PrettyPrint
import Text.PrettyPrint.GenericPretty

import Gibbon.Common
import Gibbon.L1.Syntax as L1
import Gibbon.DynFlags
import Prelude hiding (exp)

--------------------------------------------------------------------------------

-- | Typecheck a L1 expression
--
tcExp :: DDefs1 -> Env2 Ty1 -> Exp1 -> TcM Ty1 Exp1
tcExp :: DDefs1 -> Env2 Ty1 -> Exp1 -> TcM Ty1 Exp1
tcExp DDefs1
ddfs Env2 Ty1
env Exp1
exp =
  case Exp1
exp of
    VarE Var
v    -> Env2 Ty1 -> Var -> Exp1 -> TcM Ty1 Exp1
forall l (e :: * -> * -> *).
Env2 (UrTy l)
-> Var -> PreExp e () Ty1 -> TcM (UrTy l) (PreExp e () Ty1)
lookupVar Env2 Ty1
env Var
v Exp1
exp
    LitE Int
_    -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntTy
    CharE Char
_   -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
CharTy
    FloatE{}  -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
FloatTy
    LitSymE Var
_ -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
SymTy

    AppE Var
v [()]
locs [Exp1]
ls -> do
      let funty :: ([Ty1], Ty1)
funty =
            case (Var -> Map Var ([Ty1], Ty1) -> Maybe ([Ty1], Ty1)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
v (Env2 Ty1 -> TyEnv (ArrowTy Ty1)
forall a. Env2 a -> TyEnv (ArrowTy a)
fEnv Env2 Ty1
env)) of
              Just ([Ty1], Ty1)
ty -> ([Ty1], Ty1)
ty
              Maybe ([Ty1], Ty1)
Nothing -> [Char] -> ([Ty1], Ty1)
forall a. HasCallStack => [Char] -> a
error ([Char] -> ([Ty1], Ty1)) -> [Char] -> ([Ty1], Ty1)
forall a b. (a -> b) -> a -> b
$ [Char]
"Function not found: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Out a => a -> [Char]
sdoc Var
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" while checking " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                 Exp1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Exp1
exp [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\nat "
      -- Check that the expression does not have any locations
      case [()]
locs of
        [] -> () -> ExceptT (TCError Exp1) Identity ()
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        [()]
_  -> TCError Exp1 -> ExceptT (TCError Exp1) Identity ()
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> ExceptT (TCError Exp1) Identity ())
-> TCError Exp1 -> ExceptT (TCError Exp1) Identity ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Expected the locations to be empty in L1. Got"
                                      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [()] -> [Char]
forall a. Out a => a -> [Char]
sdoc [()]
locs)
                           Exp1
exp

      -- Get argument types
      [Ty1]
argTys <- (Exp1 -> TcM Ty1 Exp1)
-> [Exp1] -> ExceptT (TCError Exp1) Identity [Ty1]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Exp1 -> TcM Ty1 Exp1
go [Exp1]
ls

      -- Check arity
      if ([Exp1] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp1]
ls) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= ([Ty1] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ty1]
argTys)
      then TCError Exp1 -> ExceptT (TCError Exp1) Identity ()
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> ExceptT (TCError Exp1) Identity ())
-> TCError Exp1 -> ExceptT (TCError Exp1) Identity ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Arity mismatch. Expected:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([Ty1] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ty1]
argTys) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                   [Char]
" Got:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([Exp1] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp1]
ls)) Exp1
exp
      else () -> ExceptT (TCError Exp1) Identity ()
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

      let ([Ty1]
funInTys,Ty1
funRetTy) = (ArrowTy Ty1 -> [Ty1]
forall ty. FunctionTy ty => ArrowTy ty -> [ty]
inTys ([Ty1], Ty1)
ArrowTy Ty1
funty, ArrowTy Ty1 -> Ty1
forall ty. FunctionTy ty => ArrowTy ty -> ty
outTy ([Ty1], Ty1)
ArrowTy Ty1
funty)

          combAr :: (UrTy loc, UrTy loc) -> Map Var Var -> Map Var Var
combAr (SymDictTy (Just Var
v1) Ty1
_, SymDictTy (Just Var
v2) Ty1
_) Map Var Var
m = Var -> Var -> Map Var Var -> Map Var Var
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
v2 Var
v1 Map Var Var
m
          combAr (UrTy loc, UrTy loc)
_ Map Var Var
m = Map Var Var
m
          arMap :: Map Var Var
arMap = ((Ty1, Ty1) -> Map Var Var -> Map Var Var)
-> Map Var Var -> [(Ty1, Ty1)] -> Map Var Var
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr (Ty1, Ty1) -> Map Var Var -> Map Var Var
forall {loc} {loc}.
(UrTy loc, UrTy loc) -> Map Var Var -> Map Var Var
combAr Map Var Var
forall k a. Map k a
M.empty ([(Ty1, Ty1)] -> Map Var Var) -> [(Ty1, Ty1)] -> Map Var Var
forall a b. (a -> b) -> a -> b
$ [Ty1] -> [Ty1] -> [(Ty1, Ty1)]
forall a b.
(Show a, Show b, HasCallStack) =>
[a] -> [b] -> [(a, b)]
fragileZip [Ty1]
argTys [Ty1]
funInTys

          subDictTy :: Map Var Var -> Ty1 -> Ty1
subDictTy Map Var Var
m (SymDictTy (Just Var
w) Ty1
ty) =
              case Var -> Map Var Var -> Maybe Var
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
w Map Var Var
m of
                Just Var
w' -> Maybe Var -> Ty1 -> Ty1
forall loc. Maybe Var -> Ty1 -> UrTy loc
SymDictTy (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
w') Ty1
ty
                Maybe Var
Nothing -> [Char] -> Ty1
forall a. HasCallStack => [Char] -> a
error ([Char] -> Ty1) -> [Char] -> Ty1
forall a b. (a -> b) -> a -> b
$ ([Char]
"Cannot match up arena for dictionary in function application: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Exp1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Exp1
exp)
          subDictTy Map Var Var
_ Ty1
ty = Ty1
ty

          subFunInTys :: [Ty1]
subFunInTys = (Ty1 -> Ty1) -> [Ty1] -> [Ty1]
forall a b. (a -> b) -> [a] -> [b]
L.map (Map Var Var -> Ty1 -> Ty1
subDictTy Map Var Var
arMap) [Ty1]
funInTys
          subFunOutTy :: Ty1
subFunOutTy = Map Var Var -> Ty1 -> Ty1
subDictTy Map Var Var
arMap Ty1
funRetTy

      [Ty1]
_ <- ((Ty1, Ty1) -> TcM Ty1 Exp1)
-> [(Ty1, Ty1)] -> ExceptT (TCError Exp1) Identity [Ty1]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Ty1
a,Ty1
b) -> Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
a Ty1
b) ([Ty1] -> [Ty1] -> [(Ty1, Ty1)]
forall a b.
(Show a, Show b, HasCallStack) =>
[a] -> [b] -> [(a, b)]
fragileZip [Ty1]
subFunInTys [Ty1]
argTys)
      Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
subFunOutTy

    PrimAppE Prim Ty1
pr [Exp1]
es -> do
      -- Special case because we can't lookup the type of the function pointer
      [Ty1]
tys <- case Prim Ty1
pr of
               VSortP{} -> (Exp1 -> TcM Ty1 Exp1)
-> [Exp1] -> ExceptT (TCError Exp1) Identity [Ty1]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Exp1 -> TcM Ty1 Exp1
go ([Exp1] -> [Exp1]
forall a. HasCallStack => [a] -> [a]
init [Exp1]
es)
               InplaceVSortP{} -> (Exp1 -> TcM Ty1 Exp1)
-> [Exp1] -> ExceptT (TCError Exp1) Identity [Ty1]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Exp1 -> TcM Ty1 Exp1
go ([Exp1] -> [Exp1]
forall a. HasCallStack => [a] -> [a]
init [Exp1]
es)
               Prim Ty1
_ -> (Exp1 -> TcM Ty1 Exp1)
-> [Exp1] -> ExceptT (TCError Exp1) Identity [Ty1]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Exp1 -> TcM Ty1 Exp1
go [Exp1]
es

      let len0 :: ExceptT (TCError Exp1) Identity ()
len0 = Exp1
-> Prim Ty1 -> Int -> [Exp1] -> ExceptT (TCError Exp1) Identity ()
forall op arg (e :: * -> * -> *).
(Out op, Out arg) =>
PreExp e () Ty1 -> op -> Int -> [arg] -> TcM () (PreExp e () Ty1)
checkLen Exp1
exp Prim Ty1
pr Int
0 [Exp1]
es
          len1 :: ExceptT (TCError Exp1) Identity ()
len1 = Exp1
-> Prim Ty1 -> Int -> [Exp1] -> ExceptT (TCError Exp1) Identity ()
forall op arg (e :: * -> * -> *).
(Out op, Out arg) =>
PreExp e () Ty1 -> op -> Int -> [arg] -> TcM () (PreExp e () Ty1)
checkLen Exp1
exp Prim Ty1
pr Int
1 [Exp1]
es
          len2 :: ExceptT (TCError Exp1) Identity ()
len2 = Exp1
-> Prim Ty1 -> Int -> [Exp1] -> ExceptT (TCError Exp1) Identity ()
forall op arg (e :: * -> * -> *).
(Out op, Out arg) =>
PreExp e () Ty1 -> op -> Int -> [arg] -> TcM () (PreExp e () Ty1)
checkLen Exp1
exp Prim Ty1
pr Int
2 [Exp1]
es
          len3 :: ExceptT (TCError Exp1) Identity ()
len3 = Exp1
-> Prim Ty1 -> Int -> [Exp1] -> ExceptT (TCError Exp1) Identity ()
forall op arg (e :: * -> * -> *).
(Out op, Out arg) =>
PreExp e () Ty1 -> op -> Int -> [arg] -> TcM () (PreExp e () Ty1)
checkLen Exp1
exp Prim Ty1
pr Int
3 [Exp1]
es
          len4 :: ExceptT (TCError Exp1) Identity ()
len4 = Exp1
-> Prim Ty1 -> Int -> [Exp1] -> ExceptT (TCError Exp1) Identity ()
forall op arg (e :: * -> * -> *).
(Out op, Out arg) =>
PreExp e () Ty1 -> op -> Int -> [arg] -> TcM () (PreExp e () Ty1)
checkLen Exp1
exp Prim Ty1
pr Int
4 [Exp1]
es

          mk_bools :: TcM Ty1 Exp1
mk_bools = do
            ExceptT (TCError Exp1) Identity ()
len0
            Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
BoolTy

          bool_ops :: TcM Ty1 Exp1
bool_ops = do
            ExceptT (TCError Exp1) Identity ()
len2
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
BoolTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
BoolTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
            Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
BoolTy

          int_ops :: TcM Ty1 Exp1
int_ops = do
            ExceptT (TCError Exp1) Identity ()
len2
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
IntTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
IntTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
            Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
IntTy

          float_ops :: TcM Ty1 Exp1
float_ops = do
            ExceptT (TCError Exp1) Identity ()
len2
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
forall loc. UrTy loc
FloatTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
forall loc. UrTy loc
FloatTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
            Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
FloatTy

          int_cmps :: TcM Ty1 Exp1
int_cmps = do
            ExceptT (TCError Exp1) Identity ()
len2
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
IntTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
IntTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
            Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
BoolTy

          float_cmps :: TcM Ty1 Exp1
float_cmps = do
            ExceptT (TCError Exp1) Identity ()
len2
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
forall loc. UrTy loc
FloatTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
forall loc. UrTy loc
FloatTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
            Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
BoolTy

          char_cmps :: TcM Ty1 Exp1
char_cmps = do
            ExceptT (TCError Exp1) Identity ()
len2
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
forall loc. UrTy loc
CharTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
            Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
forall loc. UrTy loc
CharTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
            Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
BoolTy

      case Prim Ty1
pr of
        Prim Ty1
MkTrue  -> TcM Ty1 Exp1
mk_bools
        Prim Ty1
MkFalse -> TcM Ty1 Exp1
mk_bools
        Prim Ty1
AddP    -> TcM Ty1 Exp1
int_ops
        Prim Ty1
SubP    -> TcM Ty1 Exp1
int_ops
        Prim Ty1
MulP    -> TcM Ty1 Exp1
int_ops
        Prim Ty1
DivP    -> TcM Ty1 Exp1
int_ops
        Prim Ty1
ModP    -> TcM Ty1 Exp1
int_ops
        Prim Ty1
ExpP    -> TcM Ty1 Exp1
int_ops
        Prim Ty1
FAddP   -> TcM Ty1 Exp1
float_ops
        Prim Ty1
FSubP   -> TcM Ty1 Exp1
float_ops
        Prim Ty1
FMulP   -> TcM Ty1 Exp1
float_ops
        Prim Ty1
FDivP   -> TcM Ty1 Exp1
float_ops
        Prim Ty1
FExpP   -> TcM Ty1 Exp1
float_ops
        Prim Ty1
EqIntP  -> TcM Ty1 Exp1
int_cmps
        Prim Ty1
LtP     -> TcM Ty1 Exp1
int_cmps
        Prim Ty1
GtP     -> TcM Ty1 Exp1
int_cmps
        Prim Ty1
LtEqP   -> TcM Ty1 Exp1
int_cmps
        Prim Ty1
GtEqP   -> TcM Ty1 Exp1
int_cmps
        Prim Ty1
EqFloatP -> TcM Ty1 Exp1
float_cmps
        Prim Ty1
FLtP     -> TcM Ty1 Exp1
float_cmps
        Prim Ty1
FGtP     -> TcM Ty1 Exp1
float_cmps
        Prim Ty1
FLtEqP   -> TcM Ty1 Exp1
float_cmps
        Prim Ty1
FGtEqP   -> TcM Ty1 Exp1
float_cmps
        Prim Ty1
OrP     -> TcM Ty1 Exp1
bool_ops
        Prim Ty1
AndP    -> TcM Ty1 Exp1
bool_ops
        Prim Ty1
EqCharP  -> TcM Ty1 Exp1
char_cmps
        Prim Ty1
Gensym -> ExceptT (TCError Exp1) Identity ()
len0 ExceptT (TCError Exp1) Identity ()
-> (() -> TcM Ty1 Exp1) -> TcM Ty1 Exp1
forall a b.
ExceptT (TCError Exp1) Identity a
-> (a -> ExceptT (TCError Exp1) Identity b)
-> ExceptT (TCError Exp1) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \()
_ -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
SymTy

        Prim Ty1
EqSymP -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
BoolTy

        EqBenchProgP [Char]
_ -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
BoolTy

        Prim Ty1
RandP -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntTy
        Prim Ty1
FRandP -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
FloatTy
        Prim Ty1
FSqrtP -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
forall loc. UrTy loc
FloatTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
FloatTy

        Prim Ty1
FTanP -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
forall loc. UrTy loc
FloatTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
FloatTy

        Prim Ty1
FloatToIntP -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
forall loc. UrTy loc
FloatTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntTy

        Prim Ty1
IntToFloatP -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
forall loc. UrTy loc
IntTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
FloatTy

        Prim Ty1
PrintInt -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
IntTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [])

        Prim Ty1
PrintChar -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
CharTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [])

        Prim Ty1
PrintFloat -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
FloatTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [])

        Prim Ty1
PrintBool -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
BoolTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [])

        Prim Ty1
PrintSym -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [])

        Prim Ty1
ReadInt -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntTy

        Prim Ty1
SymSetEmpty -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
SymSetTy

        Prim Ty1
SymSetInsert -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
SymSetTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
SymSetTy

        Prim Ty1
SymSetContains -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
SymSetTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
BoolTy

        Prim Ty1
SymHashEmpty -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
SymHashTy

        Prim Ty1
SymHashInsert -> do
          ExceptT (TCError Exp1) Identity ()
len3
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
SymHashTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
2) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
2)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
SymHashTy

        Prim Ty1
SymHashLookup -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
SymHashTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
SymTy

        Prim Ty1
SymHashContains -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
SymHashTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
BoolTy

        DictEmptyP Ty1
ty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          let [Ty1
a] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
forall loc. UrTy loc
ArenaTy Ty1
a
          case ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) of
            (VarE Var
var) -> do Exp1 -> Env2 Ty1 -> Maybe Var -> ExceptT (TCError Exp1) Identity ()
forall exp (m :: * -> *) a.
MonadError (TCError exp) m =>
exp -> Env2 a -> Maybe Var -> m ()
ensureArenaScope Exp1
exp Env2 Ty1
env (Maybe Var -> ExceptT (TCError Exp1) Identity ())
-> Maybe Var -> ExceptT (TCError Exp1) Identity ()
forall a b. (a -> b) -> a -> b
$ Var -> Maybe Var
forall a. a -> Maybe a
Just Var
var
                             Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ty1 -> TcM Ty1 Exp1) -> Ty1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ Maybe Var -> Ty1 -> Ty1
forall loc. Maybe Var -> Ty1 -> UrTy loc
SymDictTy (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
var) Ty1
ty
            Exp1
_ -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Expected arena variable argument" Exp1
exp

        DictInsertP Ty1
ty -> do
          ExceptT (TCError Exp1) Identity ()
len4
          let [Ty1
a,Ty1
d,Ty1
k,Ty1
v] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
forall loc. UrTy loc
ArenaTy Ty1
a
          case Ty1
d of
            SymDictTy Maybe Var
ar Ty1
dty -> do Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
forall loc. UrTy loc
SymTy Ty1
k
                                   Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
ty Ty1
v
                                   Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
ty Ty1
dty
                                   Exp1 -> Env2 Ty1 -> Maybe Var -> ExceptT (TCError Exp1) Identity ()
forall exp (m :: * -> *) a.
MonadError (TCError exp) m =>
exp -> Env2 a -> Maybe Var -> m ()
ensureArenaScope Exp1
exp Env2 Ty1
env Maybe Var
ar
                                   case [Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0 of
                                     (VarE Var
var) -> do Exp1 -> Env2 Ty1 -> Maybe Var -> ExceptT (TCError Exp1) Identity ()
forall exp (m :: * -> *) a.
MonadError (TCError exp) m =>
exp -> Env2 a -> Maybe Var -> m ()
ensureArenaScope Exp1
exp Env2 Ty1
env (Maybe Var -> ExceptT (TCError Exp1) Identity ())
-> Maybe Var -> ExceptT (TCError Exp1) Identity ()
forall a b. (a -> b) -> a -> b
$ Var -> Maybe Var
forall a. a -> Maybe a
Just Var
var
                                                      Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ty1 -> TcM Ty1 Exp1) -> Ty1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ Maybe Var -> Ty1 -> Ty1
forall loc. Maybe Var -> Ty1 -> UrTy loc
SymDictTy (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
var) Ty1
ty
                                     Exp1
_ -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Expected arena variable argument" Exp1
exp
            Ty1
_ -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Expected SymDictTy" Exp1
exp

        DictLookupP Ty1
ty -> do
          ExceptT (TCError Exp1) Identity ()
len2
          let [Ty1
d,Ty1
k] = [Ty1]
tys
          case Ty1
d of
            SymDictTy Maybe Var
ar Ty1
dty -> do Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
forall loc. UrTy loc
SymTy Ty1
k
                                   Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
ty Ty1
dty
                                   -- dbgTrace 3 (show $ vEnv env) $ return ()
                                   Exp1 -> Env2 Ty1 -> Maybe Var -> ExceptT (TCError Exp1) Identity ()
forall exp (m :: * -> *) a.
MonadError (TCError exp) m =>
exp -> Env2 a -> Maybe Var -> m ()
ensureArenaScope Exp1
exp Env2 Ty1
env Maybe Var
ar
                                   Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
ty
            Ty1
_ -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Expected SymDictTy" Exp1
exp

        DictHasKeyP Ty1
ty -> do
          ExceptT (TCError Exp1) Identity ()
len2
          let [Ty1
d,Ty1
k] = [Ty1]
tys
          case Ty1
d of
            SymDictTy Maybe Var
ar Ty1
dty -> do Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
forall loc. UrTy loc
SymTy Ty1
k
                                   Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
ty Ty1
dty
                                   Exp1 -> Env2 Ty1 -> Maybe Var -> ExceptT (TCError Exp1) Identity ()
forall exp (m :: * -> *) a.
MonadError (TCError exp) m =>
exp -> Env2 a -> Maybe Var -> m ()
ensureArenaScope Exp1
exp Env2 Ty1
env Maybe Var
ar
                                   Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
BoolTy
            Ty1
_ -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Expected SymDictTy" Exp1
exp

        ErrorP [Char]
_str Ty1
ty -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
ty

        Prim Ty1
SizeParam -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntTy

        Prim Ty1
IsBig -> do
          ExceptT (TCError Exp1) Identity ()
len2
          let [Ty1
ity,Ty1
ety] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
ity Ty1
forall loc. UrTy loc
IntTy
          if Ty1 -> Bool
forall a. UrTy a -> Bool
isPackedTy Ty1
ety
          then Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
BoolTy
          else [Char] -> TcM Ty1 Exp1
forall a. HasCallStack => [Char] -> a
error ([Char] -> TcM Ty1 Exp1) -> [Char] -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char]
"L1.Typecheck: IsBig expects a Packed value. Got: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
ety

        ReadPackedFile Maybe [Char]
_fp [Char]
_tycon Maybe Var
_reg Ty1
ty -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
ty

        WritePackedFile [Char]
_ Ty1
ty
           | PackedTy{} <- Ty1
ty  -> do
             ExceptT (TCError Exp1) Identity ()
len1
             let [Ty1
packed_ty] = [Ty1]
tys
             Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
packed_ty Ty1
ty
             Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [])
           | Bool
otherwise -> [Char] -> TcM Ty1 Exp1
forall a. HasCallStack => [Char] -> a
error ([Char] -> TcM Ty1 Exp1) -> [Char] -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char]
"writePackedFile expects a packed type. Given" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
ty

        ReadArrayFile Maybe ([Char], Int)
_ Ty1
ty -> do
          ExceptT (TCError Exp1) Identity ()
len0
          if Ty1 -> Bool
forall a. UrTy a -> Bool
isValidListElemTy Ty1
ty
          then Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
ty)
          else TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Not a valid list type" Exp1
exp

        Prim Ty1
RequestSizeOf -> do
          ExceptT (TCError Exp1) Identity ()
len1
          case ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) of
            VarE{} -> if Ty1 -> Bool
forall a. UrTy a -> Bool
isPackedTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
                      then Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntTy
                      else case ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) of
                             Ty1
SymTy -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntTy
                             Ty1
IntTy -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntTy
                             Ty1
_ -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Expected PackedTy" Exp1
exp
            Exp1
_ -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Expected a variable argument" Exp1
exp

        VAllocP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
i] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
forall loc. UrTy loc
IntTy Ty1
i
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty)

        VFreeP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
i] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty) Ty1
i
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [])

        VFree2P Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
i] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty) Ty1
i
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [])

        VLengthP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
ls] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty) Ty1
ls
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
IntTy

        VNthP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
ls, Ty1
i] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty) Ty1
ls
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
forall loc. UrTy loc
IntTy Ty1
i
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
elty

        VSliceP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len3
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
from,Ty1
to,Ty1
ls] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
forall loc. UrTy loc
IntTy Ty1
from
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
forall loc. UrTy loc
IntTy Ty1
to
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty) Ty1
ls
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty)

        InplaceVUpdateP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len3
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
ls,Ty1
i,Ty1
x] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty) Ty1
ls
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
forall loc. UrTy loc
IntTy Ty1
i
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) Ty1
elty Ty1
x
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty)

        VConcatP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
ls] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty)) Ty1
ls
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty)

        -- Given that the first argument is a list of type (VectorTy t),
        -- ensure that the 2nd argument is function reference of type:
        -- ty -> ty -> IntTy
        VSortP Ty1
elty ->
          case ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) of
            VarE Var
f -> do
              ExceptT (TCError Exp1) Identity ()
len2
              let [Ty1
ls] = [Ty1]
tys
                  fn_ty :: ArrowTy Ty1
fn_ty@([Ty1]
in_tys, Ty1
ret_ty) = Var -> Env2 Ty1 -> ArrowTy Ty1
forall a. Out (ArrowTy a) => Var -> Env2 a -> ArrowTy a
lookupFEnv Var
f Env2 Ty1
env
                  err :: ([Ty1], Ty1) -> TcM Ty1 Exp1
err ([Ty1], Ty1)
x = TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"vsort: Expected a sort function of type (ty -> ty -> Bool). Got"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Ty1], Ty1) -> [Char]
forall a. Out a => a -> [Char]
sdoc ([Ty1], Ty1)
x) Exp1
exp
              Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty) Ty1
ls
              case [Ty1]
in_tys of
                [Ty1
a,Ty1
b] -> do
                   -- [2021.05.08]: looks suspicious
                   Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
a Ty1
elty
                   Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
b Ty1
elty
                   Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
ret_ty Ty1
forall loc. UrTy loc
IntTy
                   Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty)
                [Ty1]
_ -> ([Ty1], Ty1) -> TcM Ty1 Exp1
err ([Ty1], Ty1)
ArrowTy Ty1
fn_ty
            Exp1
oth -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"vsort: function pointer has to be a variable reference. Got"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Exp1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Exp1
oth) Exp1
exp

        InplaceVSortP Ty1
elty -> Exp1 -> TcM Ty1 Exp1
go (Prim Ty1 -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE (Ty1 -> Prim Ty1
forall ty. ty -> Prim ty
VSortP Ty1
elty) [Exp1]
es)

        VMergeP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
ls1,Ty1
ls2] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty) Ty1
ls1
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty) Ty1
ls2
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
VectorTy Ty1
elty)


        PDictInsertP Ty1
kty Ty1
vty -> do
          ExceptT (TCError Exp1) Identity ()
len3
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
kty
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
vty
          let [Ty1
key, Ty1
val, Ty1
dict] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
key Ty1
kty
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
val Ty1
vty
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) Ty1
dict (Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty)

        PDictLookupP Ty1
kty Ty1
vty -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
kty
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
vty
          let [Ty1
key, Ty1
dict] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
key Ty1
kty
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
dict (Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1
vty)

        PDictAllocP Ty1
kty Ty1
vty -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
kty
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
vty
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty)

        PDictHasKeyP Ty1
kty Ty1
vty -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
kty
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
vty
          let [Ty1
key, Ty1
dict] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
key Ty1
kty
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
dict (Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1
forall loc. UrTy loc
BoolTy)

        PDictForkP Ty1
kty Ty1
vty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
kty
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
vty
          let [Ty1
dict] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
dict (Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty, Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty])

        PDictJoinP Ty1
kty Ty1
vty -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
kty
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
vty
          let [Ty1
dict1, Ty1
dict2] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
dict1 (Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
dict2 (Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc -> UrTy loc
PDictTy Ty1
kty Ty1
vty)

        LLAllocP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty)

        LLIsEmptyP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
ll] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
ll (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1
forall loc. UrTy loc
BoolTy)

        LLConsP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
elt, Ty1
ll] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
elt Ty1
elty
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty1
ll (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty)

        LLHeadP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
ll] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
ll (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1
elty)

        LLTailP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
ll] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty1
ll (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty)

        LLFreeP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
i] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty) Ty1
i
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [])

        LLFree2P Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
i] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty) Ty1
i
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [])

        LLCopyP Ty1
elty -> do
          ExceptT (TCError Exp1) Identity ()
len1
          Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
elty
          let [Ty1
i] = [Ty1]
tys
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty) Ty1
i
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty1 -> Ty1
forall loc. UrTy loc -> UrTy loc
ListTy Ty1
elty)

        Prim Ty1
GetNumProcessors -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
IntTy

        Prim Ty1
IntHashEmpty -> do
          ExceptT (TCError Exp1) Identity ()
len0
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntHashTy

        Prim Ty1
IntHashInsert -> do
          ExceptT (TCError Exp1) Identity ()
len3
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
IntHashTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
2) Ty1
forall loc. UrTy loc
IntTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
2)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntHashTy

        Prim Ty1
IntHashLookup -> do
          ExceptT (TCError Exp1) Identity ()
len2
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) Ty1
forall loc. UrTy loc
IntHashTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
          Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy ([Exp1]
es [Exp1] -> Int -> Exp1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) Ty1
forall loc. UrTy loc
SymTy ([Ty1]
tys [Ty1] -> Int -> Ty1
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
          Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
IntTy

        Write3dPpmFile{} -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Write3dPpmFile not handled yet" Exp1
exp

        RequestEndOf{} -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC  [Char]
"tcExp of PrimAppE: RequestEndOf not handled yet" Exp1
exp

    LetE (Var
v,[],SymDictTy Maybe Var
_ Ty1
pty, Exp1
rhs) Exp1
e -> do
      Ty1
tyRhs <- Exp1 -> TcM Ty1 Exp1
go Exp1
rhs
      case Ty1
tyRhs of
        SymDictTy Maybe Var
ar Ty1
pty' ->
            do  Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
pty Ty1
pty'
                Bool
-> ExceptT (TCError Exp1) Identity ()
-> ExceptT (TCError Exp1) Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Maybe Var -> Bool
forall a. Maybe a -> Bool
isJust Maybe Var
ar) (ExceptT (TCError Exp1) Identity ()
 -> ExceptT (TCError Exp1) Identity ())
-> ExceptT (TCError Exp1) Identity ()
-> ExceptT (TCError Exp1) Identity ()
forall a b. (a -> b) -> a -> b
$ TCError Exp1 -> ExceptT (TCError Exp1) Identity ()
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> ExceptT (TCError Exp1) Identity ())
-> TCError Exp1 -> ExceptT (TCError Exp1) Identity ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Expected arena variable annotation" Exp1
rhs
                let env' :: Env2 Ty1
env' = Env2 Ty1 -> [(Var, Ty1)] -> Env2 Ty1
forall l. Env2 (UrTy l) -> [(Var, UrTy l)] -> Env2 (UrTy l)
extendEnv Env2 Ty1
env [(Var
v,Maybe Var -> Ty1 -> Ty1
forall loc. Maybe Var -> Ty1 -> UrTy loc
SymDictTy Maybe Var
ar Ty1
pty')]
                DDefs1 -> Env2 Ty1 -> Exp1 -> TcM Ty1 Exp1
tcExp DDefs1
ddfs Env2 Ty1
env' Exp1
e
        Ty1
_ -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Expected expression to be SymDict type:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Exp1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Exp1
rhs) Exp1
exp

    LetE (Var
v,[()]
locs,Ty1
ty,Exp1
rhs) Exp1
e -> do
      -- Check that the expression does not have any locations
      case [()]
locs of
        [] -> () -> ExceptT (TCError Exp1) Identity ()
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        [()]
_  -> TCError Exp1 -> ExceptT (TCError Exp1) Identity ()
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> ExceptT (TCError Exp1) Identity ())
-> TCError Exp1 -> ExceptT (TCError Exp1) Identity ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Expected the locations to be empty in L1. Got"
                                      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [()] -> [Char]
forall a. Out a => a -> [Char]
sdoc [()]
locs)
                           Exp1
exp
      -- Check RHS
      Ty1
tyRhs <- Exp1 -> TcM Ty1 Exp1
go Exp1
rhs
      Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
tyRhs Ty1
ty
      let env' :: Env2 Ty1
env' = Env2 Ty1 -> [(Var, Ty1)] -> Env2 Ty1
forall l. Env2 (UrTy l) -> [(Var, UrTy l)] -> Env2 (UrTy l)
extendEnv Env2 Ty1
env [(Var
v,Ty1
ty)]
      -- Check body
      DDefs1 -> Env2 Ty1 -> Exp1 -> TcM Ty1 Exp1
tcExp DDefs1
ddfs Env2 Ty1
env' Exp1
e

    IfE Exp1
tst Exp1
consq Exp1
alt -> do
      -- Check if the test is a boolean
      Ty1
tyTst <- Exp1 -> TcM Ty1 Exp1
go Exp1
tst
      Ty1
_ <- Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
exp Ty1
tyTst Ty1
forall loc. UrTy loc
BoolTy

      -- Check if both branches match
      Ty1
tyConsq <- Exp1 -> TcM Ty1 Exp1
go Exp1
consq
      Ty1
tyAlt   <- Exp1 -> TcM Ty1 Exp1
go Exp1
alt

      -- _ <- ensureEqualTy exp tyConsq tyAlt
      if Ty1
tyConsq Ty1 -> Ty1 -> Bool
forall a. Eq a => a -> a -> Bool
== Ty1
tyAlt
      then Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
tyConsq
      else TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"If branches have mismatched types:"
                                   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
tyConsq [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
tyAlt) Exp1
exp


    MkProdE [Exp1]
es -> do
      [Ty1]
tys <- (Exp1 -> TcM Ty1 Exp1)
-> [Exp1] -> ExceptT (TCError Exp1) Identity [Ty1]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Exp1 -> TcM Ty1 Exp1
go [Exp1]
es
      Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ty1 -> TcM Ty1 Exp1) -> Ty1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Ty1] -> Ty1
forall loc. [UrTy loc] -> UrTy loc
ProdTy [Ty1]
tys

    ProjE Int
i Exp1
e -> do
      Ty1
ty  <- Exp1 -> TcM Ty1 Exp1
go Exp1
e
      Ty1
tyi <- Exp1 -> Int -> Ty1 -> TcM Ty1 Exp1
forall l (e :: * -> * -> *).
Out l =>
PreExp e () Ty1 -> Int -> UrTy l -> TcM (UrTy l) (PreExp e () Ty1)
tcProj Exp1
exp Int
i Ty1
ty
      Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
tyi

    CaseE Exp1
e [([Char], [(Var, ())], Exp1)]
cs -> do
      Ty1
tye  <- Exp1 -> TcM Ty1 Exp1
go Exp1
e
      let tycons :: [[Char]]
tycons = (([Char], [(Var, ())], Exp1) -> [Char])
-> [([Char], [(Var, ())], Exp1)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
L.map (DDefs1 -> [Char] -> [Char]
forall a. Out a => DDefs a -> [Char] -> [Char]
getTyOfDataCon DDefs1
ddfs ([Char] -> [Char])
-> (([Char], [(Var, ())], Exp1) -> [Char])
-> ([Char], [(Var, ())], Exp1)
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\([Char]
a,[(Var, ())]
_,Exp1
_) -> [Char]
a)) [([Char], [(Var, ())], Exp1)]
cs
      case [[Char]] -> [[Char]]
forall a. Eq a => [a] -> [a]
L.nub [[Char]]
tycons of
        [[Char]
one] -> do
          -- _ <- ensureEqualTy exp (PackedTy one ()) tye
          let (PackedTy [Char]
t ()
_l) = Ty1
tye
          if [Char]
one [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
t
          then () -> ExceptT (TCError Exp1) Identity ()
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          else [Char] -> ExceptT (TCError Exp1) Identity ()
forall a. HasCallStack => [Char] -> a
error([Char] -> ExceptT (TCError Exp1) Identity ())
-> [Char] -> ExceptT (TCError Exp1) Identity ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Expected these to be the same: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
one [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" & " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Out a => a -> [Char]
sdoc [Char]
t
          DDefs1 -> Env2 Ty1 -> [([Char], [(Var, ())], Exp1)] -> TcM Ty1 Exp1
tcCases DDefs1
ddfs Env2 Ty1
env [([Char], [(Var, ())], Exp1)]
cs
        [[Char]]
oth   -> TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Case branches have mismatched types: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
forall a. Out a => a -> [Char]
sdoc [[Char]]
oth
                                         [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
" , in " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Exp1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Exp1
exp) Exp1
exp

    DataConE ()
loc [Char]
dc [Exp1]
es -> do
      [Ty1]
tys <- (Exp1 -> TcM Ty1 Exp1)
-> [Exp1] -> ExceptT (TCError Exp1) Identity [Ty1]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Exp1 -> TcM Ty1 Exp1
go [Exp1]
es
      let dcTy :: [Char]
dcTy = DDefs1 -> [Char] -> [Char]
forall a. Out a => DDefs a -> [Char] -> [Char]
getTyOfDataCon DDefs1
ddfs [Char]
dc
          args :: [Ty1]
args = DDefs1 -> [Char] -> [Ty1]
forall a. Out a => DDefs a -> [Char] -> [a]
lookupDataCon DDefs1
ddfs [Char]
dc
      if [Ty1] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ty1]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Exp1] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp1]
es
      then TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Invalid argument length: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Exp1] -> [Char]
forall a. Out a => a -> [Char]
sdoc [Exp1]
es) Exp1
exp
      else do
        -- Check if arguments match with expected datacon types
        [TcM Ty1 Exp1] -> ExceptT (TCError Exp1) Identity ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ Exp1 -> Ty1 -> Ty1 -> TcM Ty1 Exp1
forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy Exp1
e Ty1
ty1 Ty1
ty2
                  | (Ty1
ty1,Ty1
ty2,Exp1
e) <- [Ty1] -> [Ty1] -> [Exp1] -> [(Ty1, Ty1, Exp1)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Ty1]
args [Ty1]
tys [Exp1]
es]
        Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ty1 -> TcM Ty1 Exp1) -> Ty1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> () -> Ty1
forall loc. [Char] -> loc -> UrTy loc
PackedTy [Char]
dcTy ()
loc

    TimeIt Exp1
e Ty1
_ty Bool
_b -> do
      -- Before flatten, _ty is always (PackedTy "DUMMY_TY" ())
      -- enforce ty == _ty in strict mode ?
      Ty1
ty <- Exp1 -> TcM Ty1 Exp1
go Exp1
e
      Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
ty

    SpawnE Var
v [()]
locs [Exp1]
ls -> do
      Ty1
ty <- Exp1 -> TcM Ty1 Exp1
go (Var -> [()] -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
v [()]
locs [Exp1]
ls)
      if Ty1 -> Bool
forall a. UrTy a -> Bool
isScalarTy Ty1
ty Bool -> Bool -> Bool
|| Ty1 -> Bool
forall a. UrTy a -> Bool
isPackedTy Ty1
ty
      then Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
ty
      else case Ty1
ty of
             ProdTy [Ty1]
tys ->
               case (Ty1 -> Bool) -> [Ty1] -> [Ty1]
forall a. (a -> Bool) -> [a] -> [a]
L.filter Ty1 -> Bool
forall a. UrTy a -> Bool
isPackedTy [Ty1]
tys of
                 []    -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
ty
                 [Ty1
_one]-> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
ty
                 [Ty1]
_     -> [Char] -> TcM Ty1 Exp1
forall a. HasCallStack => [Char] -> a
error ([Char] -> TcM Ty1 Exp1) -> [Char] -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char]
"Gibbon-TODO: Product types not allowed in SpawnE. Got: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
ty
             VectorTy{} -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
ty
             Ty1
_ -> [Char] -> TcM Ty1 Exp1
forall a. HasCallStack => [Char] -> a
error [Char]
"L1.Typecheck: SpawnE; type shouldn't be anything else."

    Exp1
SyncE -> Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
voidTy

    WithArenaE Var
v Exp1
e -> do
      let env' :: Env2 Ty1
env' = Env2 Ty1 -> [(Var, Ty1)] -> Env2 Ty1
forall l. Env2 (UrTy l) -> [(Var, UrTy l)] -> Env2 (UrTy l)
extendEnv Env2 Ty1
env [(Var
v,Ty1
forall loc. UrTy loc
ArenaTy)]
      DDefs1 -> Env2 Ty1 -> Exp1 -> TcM Ty1 Exp1
tcExp DDefs1
ddfs Env2 Ty1
env' Exp1
e

    Ext (BenchE Var
fn [()]
tyapps [Exp1]
args Bool
_b) -> do
      Exp1 -> TcM Ty1 Exp1
go (Var -> [()] -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
fn [()]
tyapps [Exp1]
args)

    Ext (AddFixed{}) ->
      Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
CursorTy

    Ext (StartOfPkdCursor Var
cur) -> do
      Ty1
ty <- Env2 Ty1 -> Var -> Exp1 -> TcM Ty1 Exp1
forall l (e :: * -> * -> *).
Env2 (UrTy l)
-> Var -> PreExp e () Ty1 -> TcM (UrTy l) (PreExp e () Ty1)
lookupVar Env2 Ty1
env Var
cur Exp1
exp
      if Ty1 -> Bool
forall a. UrTy a -> Bool
isPackedTy Ty1
ty
        then Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty1
forall loc. UrTy loc
CursorTy
        else TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Expected a packed argument" Exp1
exp

    MapE{} -> [Char] -> TcM Ty1 Exp1
forall a. HasCallStack => [Char] -> a
error ([Char] -> TcM Ty1 Exp1) -> [Char] -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char]
"L1.Typecheck: TODO: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Exp1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Exp1
exp
    FoldE{} -> [Char] -> TcM Ty1 Exp1
forall a. HasCallStack => [Char] -> a
error ([Char] -> TcM Ty1 Exp1) -> [Char] -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char]
"L1.Typecheck: TODO: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Exp1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Exp1
exp

  where
    go :: Exp1 -> TcM Ty1 Exp1
go = DDefs1 -> Env2 Ty1 -> Exp1 -> TcM Ty1 Exp1
tcExp DDefs1
ddfs Env2 Ty1
env

    checkListElemTy :: Ty1 -> ExceptT (TCError Exp1) Identity ()
checkListElemTy Ty1
el_ty =
      if Ty1 -> Bool
forall a. UrTy a -> Bool
isValidListElemTy Ty1
el_ty
      then () -> ExceptT (TCError Exp1) Identity ()
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      else TCError Exp1 -> ExceptT (TCError Exp1) Identity ()
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> ExceptT (TCError Exp1) Identity ())
-> TCError Exp1 -> ExceptT (TCError Exp1) Identity ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Gibbon-TODO: Lists of only scalars or flat products of scalars are allowed. Got" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
el_ty) Exp1
exp

-- | Typecheck a L1 program
--
tcProg :: Prog1 -> PassM Prog1
tcProg :: Prog1 -> PassM Prog1
tcProg prg :: Prog1
prg@Prog{DDefs (TyOf Exp1)
ddefs :: DDefs (TyOf Exp1)
ddefs :: forall ex. Prog ex -> DDefs (TyOf ex)
ddefs,FunDefs Exp1
fundefs :: FunDefs Exp1
fundefs :: forall ex. Prog ex -> FunDefs ex
fundefs,Maybe (Exp1, TyOf Exp1)
mainExp :: Maybe (Exp1, TyOf Exp1)
mainExp :: forall ex. Prog ex -> Maybe (ex, TyOf ex)
mainExp} = do
  -- Get flags to check if we're in packed mode
  DynFlags
flags <- PassM DynFlags
forall (m :: * -> *). MonadReader Config m => m DynFlags
getDynFlags

  -- check ddefs
  DynFlags
dynflags <- PassM DynFlags
forall (m :: * -> *). MonadReader Config m => m DynFlags
getDynFlags
  let isPacked :: Bool
isPacked = GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_Packed DynFlags
dynflags
  Bool -> PassM () -> PassM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isPacked (PassM () -> PassM ()) -> PassM () -> PassM ()
forall a b. (a -> b) -> a -> b
$
    (DDef Ty1 -> PassM ()) -> [DDef Ty1] -> PassM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ DDef Ty1 -> PassM ()
forall {m :: * -> *} {a}. Monad m => DDef (UrTy a) -> m ()
checkDDef (DDefs1 -> [DDef Ty1]
forall k a. Map k a -> [a]
M.elems DDefs (TyOf Exp1)
DDefs1
ddefs)

  -- Handle functions
  (FunDef Exp1 -> PassM ()) -> [FunDef Exp1] -> PassM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ FunDef Exp1 -> PassM ()
fd ([FunDef Exp1] -> PassM ()) -> [FunDef Exp1] -> PassM ()
forall a b. (a -> b) -> a -> b
$ FunDefs Exp1 -> [FunDef Exp1]
forall k a. Map k a -> [a]
M.elems FunDefs Exp1
fundefs

  -- Handle main expression.
  -- Run the typechecker on the expression, and update it's type in the program
  -- (the parser initializes the main expression with the void type).
  Maybe (Exp1, Ty1)
mainExp' <- case Maybe (Exp1, TyOf Exp1)
mainExp of
                Maybe (Exp1, TyOf Exp1)
Nothing -> Maybe (Exp1, Ty1) -> PassM (Maybe (Exp1, Ty1))
forall a. a -> PassM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Exp1, Ty1)
forall a. Maybe a
Nothing
                Just (Exp1
e,TyOf Exp1
main_ty) -> do
                  let res :: Either (TCError Exp1) Ty1
res = TcM Ty1 Exp1 -> Either (TCError Exp1) Ty1
forall e a. Except e a -> Either e a
runExcept (TcM Ty1 Exp1 -> Either (TCError Exp1) Ty1)
-> TcM Ty1 Exp1 -> Either (TCError Exp1) Ty1
forall a b. (a -> b) -> a -> b
$ DDefs1 -> Env2 Ty1 -> Exp1 -> TcM Ty1 Exp1
tcExp DDefs (TyOf Exp1)
DDefs1
ddefs Env2 (TyOf Exp1)
Env2 Ty1
env Exp1
e
                  case Either (TCError Exp1) Ty1
res of
                    Left TCError Exp1
err -> [Char] -> PassM (Maybe (Exp1, Ty1))
forall a. HasCallStack => [Char] -> a
error ([Char] -> PassM (Maybe (Exp1, Ty1)))
-> [Char] -> PassM (Maybe (Exp1, Ty1))
forall a b. (a -> b) -> a -> b
$ TCError Exp1 -> [Char]
forall a. Out a => a -> [Char]
sdoc TCError Exp1
err
                    Right Ty1
ty ->
                      -- The program was just parsed, the type of the
                      -- expression must be *inferred*.
                      -- Otherwise, fail if the types don't match.
                      if TyOf Exp1
Ty1
main_ty Ty1 -> Ty1 -> Bool
forall a. Eq a => a -> a -> Bool
== Ty1
forall loc. UrTy loc
voidTy
                      then Maybe (Exp1, Ty1) -> PassM (Maybe (Exp1, Ty1))
forall a. a -> PassM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Exp1, Ty1) -> PassM (Maybe (Exp1, Ty1)))
-> Maybe (Exp1, Ty1) -> PassM (Maybe (Exp1, Ty1))
forall a b. (a -> b) -> a -> b
$ (Exp1, Ty1) -> Maybe (Exp1, Ty1)
forall a. a -> Maybe a
Just (Exp1
e, Ty1
ty)
                      else if TyOf Exp1
Ty1
main_ty Ty1 -> Ty1 -> Bool
forall a. Eq a => a -> a -> Bool
== Ty1
ty
                           -- Fail if the main expression is packed and we're in packed mode
                           then if (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Ty1 -> Bool
forall a. Show a => UrTy a -> Bool
hasPacked Ty1
ty) Bool -> Bool -> Bool
|| (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_Packed DynFlags
flags)
                                then Maybe (Exp1, Ty1) -> PassM (Maybe (Exp1, Ty1))
forall a. a -> PassM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Exp1, Ty1) -> PassM (Maybe (Exp1, Ty1)))
-> Maybe (Exp1, Ty1) -> PassM (Maybe (Exp1, Ty1))
forall a b. (a -> b) -> a -> b
$ (Exp1, Ty1) -> Maybe (Exp1, Ty1)
forall a. a -> Maybe a
Just (Exp1
e, Ty1
ty)
                                else [Char] -> PassM (Maybe (Exp1, Ty1))
forall a. HasCallStack => [Char] -> a
error ([Char] -> PassM (Maybe (Exp1, Ty1)))
-> [Char] -> PassM (Maybe (Exp1, Ty1))
forall a b. (a -> b) -> a -> b
$ [Char]
"Main expression has type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", but it must be a simple (non-packed) type, such as " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc (Ty1
forall loc. UrTy loc
IntTy :: Ty1)) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"."
                           else [Char] -> PassM (Maybe (Exp1, Ty1))
forall a. HasCallStack => [Char] -> a
error ([Char] -> PassM (Maybe (Exp1, Ty1)))
-> [Char] -> PassM (Maybe (Exp1, Ty1))
forall a b. (a -> b) -> a -> b
$ [Char]
"Expected type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc TyOf Exp1
Ty1
main_ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" but got " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
ty

  Prog1 -> PassM Prog1
forall a. a -> PassM a
forall (m :: * -> *) a. Monad m => a -> m a
return Prog1
prg { mainExp :: Maybe (Exp1, TyOf Exp1)
mainExp = Maybe (Exp1, TyOf Exp1)
Maybe (Exp1, Ty1)
mainExp' }

  where
    env :: Env2 (TyOf Exp1)
env = Prog1 -> Env2 (TyOf Exp1)
forall a. Prog a -> Env2 (TyOf a)
L1.progToEnv Prog1
prg

    checkDDef :: DDef (UrTy a) -> m ()
checkDDef DDef{[([Char], [(Bool, UrTy a)])]
dataCons :: [([Char], [(Bool, UrTy a)])]
dataCons :: forall a. DDef a -> [([Char], [(Bool, a)])]
dataCons} = do
        (([Char], [(Bool, UrTy a)]) -> m ())
-> [([Char], [(Bool, UrTy a)])] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char], [(Bool, UrTy a)]) -> m ()
forall {m :: * -> *} {a} {a}.
Monad m =>
([Char], [(a, UrTy a)]) -> m ()
go [([Char], [(Bool, UrTy a)])]
dataCons
      where
        go :: ([Char], [(a, UrTy a)]) -> m ()
go ([Char]
dcon, [(a, UrTy a)]
tys) = do
          let tys' :: [UrTy a]
tys' = (((a, UrTy a) -> UrTy a) -> [(a, UrTy a)] -> [UrTy a]
forall a b. (a -> b) -> [a] -> [b]
L.map (a, UrTy a) -> UrTy a
forall a b. (a, b) -> b
snd [(a, UrTy a)]
tys)
              mb_firstPacked :: Maybe Int
mb_firstPacked = (UrTy a -> Bool) -> [UrTy a] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
L.findIndex UrTy a -> Bool
forall a. UrTy a -> Bool
isPackedTy [UrTy a]
tys'
              scalars :: [Int]
scalars = (UrTy a -> Bool) -> [UrTy a] -> [Int]
forall a. (a -> Bool) -> [a] -> [Int]
L.findIndices (Bool -> Bool
not (Bool -> Bool) -> (UrTy a -> Bool) -> UrTy a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UrTy a -> Bool
forall a. UrTy a -> Bool
isPackedTy) [UrTy a]
tys'
          case Maybe Int
mb_firstPacked of
            Maybe Int
Nothing -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just Int
fp -> case [Int]
scalars of
                         [] -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                         [Int]
_ -> if ([Int] -> Int
forall a. HasCallStack => [a] -> a
last [Int]
scalars) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
fp
                              then [Char] -> m ()
forall a. HasCallStack => [Char] -> a
error ([Char]
"Gibbon-TODO: Constructor " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
dcon [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                          [Char]
" has a scalar field after a packed field which isn't" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                          [Char]
" allowed at the moment.")
                              else () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


    -- fd :: forall e l . FunDef Ty1 Exp -> SyM ()
    fd :: FunDef Exp1 -> PassM ()
fd FunDef{Var
funName :: Var
funName :: forall ex. FunDef ex -> Var
funName,[Var]
funArgs :: [Var]
funArgs :: forall ex. FunDef ex -> [Var]
funArgs,ArrowTy (TyOf Exp1)
funTy :: ArrowTy (TyOf Exp1)
funTy :: forall ex. FunDef ex -> ArrowTy (TyOf ex)
funTy,Exp1
funBody :: Exp1
funBody :: forall ex. FunDef ex -> ex
funBody} = do
      let ([Ty1]
argTys,Ty1
retty) = ArrowTy (TyOf Exp1)
funTy
          venv :: Map Var Ty1
venv = [(Var, Ty1)] -> Map Var Ty1
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Ty1] -> [(Var, Ty1)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
funArgs [Ty1]
argTys)
          env' :: Env2 Ty1
env' = Map Var Ty1 -> TyEnv (ArrowTy Ty1) -> Env2 Ty1
forall a. TyEnv a -> TyEnv (ArrowTy a) -> Env2 a
Env2 Map Var Ty1
venv (Env2 Ty1 -> TyEnv (ArrowTy Ty1)
forall a. Env2 a -> TyEnv (ArrowTy a)
fEnv Env2 (TyOf Exp1)
Env2 Ty1
env)
          res :: Either (TCError Exp1) Ty1
res  = TcM Ty1 Exp1 -> Either (TCError Exp1) Ty1
forall e a. Except e a -> Either e a
runExcept (TcM Ty1 Exp1 -> Either (TCError Exp1) Ty1)
-> TcM Ty1 Exp1 -> Either (TCError Exp1) Ty1
forall a b. (a -> b) -> a -> b
$ DDefs1 -> Env2 Ty1 -> Exp1 -> TcM Ty1 Exp1
tcExp DDefs (TyOf Exp1)
DDefs1
ddefs Env2 Ty1
env' Exp1
funBody
      DynFlags
dynflags <- PassM DynFlags
forall (m :: * -> *). MonadReader Config m => m DynFlags
getDynFlags
      let isPacked :: Bool
isPacked = GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_Packed DynFlags
dynflags
      case Either (TCError Exp1) Ty1
res of
        Left TCError Exp1
err -> [Char] -> PassM ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> PassM ()) -> [Char] -> PassM ()
forall a b. (a -> b) -> a -> b
$ TCError Exp1 -> [Char]
forall a. Out a => a -> [Char]
sdoc TCError Exp1
err
        Right Ty1
ty -> if Bool
isPacked Bool -> Bool -> Bool
&& ([Ty1] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Ty1] -> Int) -> [Ty1] -> Int
forall a b. (a -> b) -> a -> b
$ Ty1 -> [Ty1]
forall a. Show a => UrTy a -> [UrTy a]
getPackedTys Ty1
retty) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
                    then [Char] -> PassM ()
forall a. HasCallStack => [Char] -> a
error ([Char]
"Gibbon-TODO: Functions cannot return multiple packed values; "
                                [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"check " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Out a => a -> [Char]
sdoc Var
funName)
                    else if Ty1
ty Ty1 -> Ty1 -> Bool
forall a. Eq a => a -> a -> Bool
== Ty1
retty
                    then () -> PassM ()
forall a. a -> PassM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                    else [Char] -> PassM ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> PassM ()) -> [Char] -> PassM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Expected type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
retty)
                              [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" and got type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
ty)
      () -> PassM ()
forall a. a -> PassM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

--------------------------------------------------------------------------------
-- Helpers

data TCError exp = GenericTC String  exp
                 | VarNotFoundTC Var exp
                 | UnsupportedExpTC  exp
  deriving (Int -> TCError exp -> [Char] -> [Char]
[TCError exp] -> [Char] -> [Char]
TCError exp -> [Char]
(Int -> TCError exp -> [Char] -> [Char])
-> (TCError exp -> [Char])
-> ([TCError exp] -> [Char] -> [Char])
-> Show (TCError exp)
forall exp. Show exp => Int -> TCError exp -> [Char] -> [Char]
forall exp. Show exp => [TCError exp] -> [Char] -> [Char]
forall exp. Show exp => TCError exp -> [Char]
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall exp. Show exp => Int -> TCError exp -> [Char] -> [Char]
showsPrec :: Int -> TCError exp -> [Char] -> [Char]
$cshow :: forall exp. Show exp => TCError exp -> [Char]
show :: TCError exp -> [Char]
$cshowList :: forall exp. Show exp => [TCError exp] -> [Char] -> [Char]
showList :: [TCError exp] -> [Char] -> [Char]
Show, TCError exp -> TCError exp -> Bool
(TCError exp -> TCError exp -> Bool)
-> (TCError exp -> TCError exp -> Bool) -> Eq (TCError exp)
forall exp. Eq exp => TCError exp -> TCError exp -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall exp. Eq exp => TCError exp -> TCError exp -> Bool
== :: TCError exp -> TCError exp -> Bool
$c/= :: forall exp. Eq exp => TCError exp -> TCError exp -> Bool
/= :: TCError exp -> TCError exp -> Bool
Eq, Eq (TCError exp)
Eq (TCError exp)
-> (TCError exp -> TCError exp -> Ordering)
-> (TCError exp -> TCError exp -> Bool)
-> (TCError exp -> TCError exp -> Bool)
-> (TCError exp -> TCError exp -> Bool)
-> (TCError exp -> TCError exp -> Bool)
-> (TCError exp -> TCError exp -> TCError exp)
-> (TCError exp -> TCError exp -> TCError exp)
-> Ord (TCError exp)
TCError exp -> TCError exp -> Bool
TCError exp -> TCError exp -> Ordering
TCError exp -> TCError exp -> TCError exp
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {exp}. Ord exp => Eq (TCError exp)
forall exp. Ord exp => TCError exp -> TCError exp -> Bool
forall exp. Ord exp => TCError exp -> TCError exp -> Ordering
forall exp. Ord exp => TCError exp -> TCError exp -> TCError exp
$ccompare :: forall exp. Ord exp => TCError exp -> TCError exp -> Ordering
compare :: TCError exp -> TCError exp -> Ordering
$c< :: forall exp. Ord exp => TCError exp -> TCError exp -> Bool
< :: TCError exp -> TCError exp -> Bool
$c<= :: forall exp. Ord exp => TCError exp -> TCError exp -> Bool
<= :: TCError exp -> TCError exp -> Bool
$c> :: forall exp. Ord exp => TCError exp -> TCError exp -> Bool
> :: TCError exp -> TCError exp -> Bool
$c>= :: forall exp. Ord exp => TCError exp -> TCError exp -> Bool
>= :: TCError exp -> TCError exp -> Bool
$cmax :: forall exp. Ord exp => TCError exp -> TCError exp -> TCError exp
max :: TCError exp -> TCError exp -> TCError exp
$cmin :: forall exp. Ord exp => TCError exp -> TCError exp -> TCError exp
min :: TCError exp -> TCError exp -> TCError exp
Ord, (forall x. TCError exp -> Rep (TCError exp) x)
-> (forall x. Rep (TCError exp) x -> TCError exp)
-> Generic (TCError exp)
forall x. Rep (TCError exp) x -> TCError exp
forall x. TCError exp -> Rep (TCError exp) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall exp x. Rep (TCError exp) x -> TCError exp
forall exp x. TCError exp -> Rep (TCError exp) x
$cfrom :: forall exp x. TCError exp -> Rep (TCError exp) x
from :: forall x. TCError exp -> Rep (TCError exp) x
$cto :: forall exp x. Rep (TCError exp) x -> TCError exp
to :: forall x. Rep (TCError exp) x -> TCError exp
Generic)


instance (Out exp) => Out (TCError exp) where
  doc :: TCError exp -> Doc
doc TCError exp
tce =
    case TCError exp
tce of
      GenericTC [Char]
str exp
ex    -> [Char] -> Doc
text [Char]
str Doc -> Doc -> Doc
$$ Doc
colon Doc -> Doc -> Doc
<+> exp -> Doc
forall a. Out a => a -> Doc
doc exp
ex
      VarNotFoundTC Var
v exp
ex  -> [Char] -> Doc
text [Char]
"Var" Doc -> Doc -> Doc
<+> Var -> Doc
forall a. Out a => a -> Doc
doc Var
v Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"not found. Checking: " Doc -> Doc -> Doc
$$
                             Doc
colon Doc -> Doc -> Doc
<+> exp -> Doc
forall a. Out a => a -> Doc
doc exp
ex
      UnsupportedExpTC exp
ex -> [Char] -> Doc
text [Char]
"Unsupported expression:" Doc -> Doc -> Doc
$$
                             Doc
colon Doc -> Doc -> Doc
<+> exp -> Doc
forall a. Out a => a -> Doc
doc exp
ex

type TcM a exp =  Except (TCError exp) a

extendEnv :: Env2 (UrTy l) -> [(Var, (UrTy l))] -> Env2 (UrTy l)
extendEnv :: forall l. Env2 (UrTy l) -> [(Var, UrTy l)] -> Env2 (UrTy l)
extendEnv (Env2 TyEnv (UrTy l)
vEnv TyEnv (ArrowTy (UrTy l))
fEnv) ((Var
v,UrTy l
ty):[(Var, UrTy l)]
rest) = Env2 (UrTy l) -> [(Var, UrTy l)] -> Env2 (UrTy l)
forall l. Env2 (UrTy l) -> [(Var, UrTy l)] -> Env2 (UrTy l)
extendEnv (TyEnv (UrTy l) -> TyEnv (ArrowTy (UrTy l)) -> Env2 (UrTy l)
forall a. TyEnv a -> TyEnv (ArrowTy a) -> Env2 a
Env2 (Var -> UrTy l -> TyEnv (UrTy l) -> TyEnv (UrTy l)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
v UrTy l
ty TyEnv (UrTy l)
vEnv) TyEnv (ArrowTy (UrTy l))
fEnv) [(Var, UrTy l)]
rest
extendEnv Env2 (UrTy l)
env [] = Env2 (UrTy l)
env


lookupVar :: Env2 (UrTy l) -> Var -> PreExp e () (UrTy ()) -> TcM (UrTy l) (PreExp e () (UrTy ()))
lookupVar :: forall l (e :: * -> * -> *).
Env2 (UrTy l)
-> Var -> PreExp e () Ty1 -> TcM (UrTy l) (PreExp e () Ty1)
lookupVar Env2 (UrTy l)
env Var
var PreExp e () Ty1
exp =
    case Var -> Map Var (UrTy l) -> Maybe (UrTy l)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
var (Map Var (UrTy l) -> Maybe (UrTy l))
-> Map Var (UrTy l) -> Maybe (UrTy l)
forall a b. (a -> b) -> a -> b
$ Env2 (UrTy l) -> Map Var (UrTy l)
forall a. Env2 a -> TyEnv a
vEnv Env2 (UrTy l)
env of
      Maybe (UrTy l)
Nothing -> TCError (PreExp e () Ty1) -> TcM (UrTy l) (PreExp e () Ty1)
forall a.
TCError (PreExp e () Ty1)
-> ExceptT (TCError (PreExp e () Ty1)) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError (PreExp e () Ty1) -> TcM (UrTy l) (PreExp e () Ty1))
-> TCError (PreExp e () Ty1) -> TcM (UrTy l) (PreExp e () Ty1)
forall a b. (a -> b) -> a -> b
$ Var -> PreExp e () Ty1 -> TCError (PreExp e () Ty1)
forall exp. Var -> exp -> TCError exp
VarNotFoundTC Var
var PreExp e () Ty1
exp
      Just UrTy l
ty -> UrTy l -> TcM (UrTy l) (PreExp e () Ty1)
forall a. a -> ExceptT (TCError (PreExp e () Ty1)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return UrTy l
ty


tcProj :: (Out l) => PreExp e () (UrTy ()) -> Int -> (UrTy l) -> TcM (UrTy l) (PreExp e () (UrTy ()))
tcProj :: forall l (e :: * -> * -> *).
Out l =>
PreExp e () Ty1 -> Int -> UrTy l -> TcM (UrTy l) (PreExp e () Ty1)
tcProj PreExp e () Ty1
_ Int
i (ProdTy [UrTy l]
tys) = UrTy l -> ExceptT (TCError (PreExp e () Ty1)) Identity (UrTy l)
forall a. a -> ExceptT (TCError (PreExp e () Ty1)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy l -> ExceptT (TCError (PreExp e () Ty1)) Identity (UrTy l))
-> UrTy l -> ExceptT (TCError (PreExp e () Ty1)) Identity (UrTy l)
forall a b. (a -> b) -> a -> b
$ [UrTy l]
tys [UrTy l] -> Int -> UrTy l
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
i
tcProj PreExp e () Ty1
e Int
_i UrTy l
ty = TCError (PreExp e () Ty1)
-> ExceptT (TCError (PreExp e () Ty1)) Identity (UrTy l)
forall a.
TCError (PreExp e () Ty1)
-> ExceptT (TCError (PreExp e () Ty1)) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError (PreExp e () Ty1)
 -> ExceptT (TCError (PreExp e () Ty1)) Identity (UrTy l))
-> TCError (PreExp e () Ty1)
-> ExceptT (TCError (PreExp e () Ty1)) Identity (UrTy l)
forall a b. (a -> b) -> a -> b
$ [Char] -> PreExp e () Ty1 -> TCError (PreExp e () Ty1)
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Projection from non-tuple type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (UrTy l -> [Char]
forall a. Out a => a -> [Char]
sdoc UrTy l
ty)) PreExp e () Ty1
e


tcCases :: DDefs Ty1 -> Env2 Ty1 -> [(DataCon, [(Var, ())], Exp1)] -> TcM Ty1 Exp1
tcCases :: DDefs1 -> Env2 Ty1 -> [([Char], [(Var, ())], Exp1)] -> TcM Ty1 Exp1
tcCases DDefs1
ddfs Env2 Ty1
env [([Char], [(Var, ())], Exp1)]
cs = do
  [Ty1]
tys <- [([Char], [(Var, ())], Exp1)]
-> (([Char], [(Var, ())], Exp1) -> TcM Ty1 Exp1)
-> ExceptT (TCError Exp1) Identity [Ty1]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [([Char], [(Var, ())], Exp1)]
cs ((([Char], [(Var, ())], Exp1) -> TcM Ty1 Exp1)
 -> ExceptT (TCError Exp1) Identity [Ty1])
-> (([Char], [(Var, ())], Exp1) -> TcM Ty1 Exp1)
-> ExceptT (TCError Exp1) Identity [Ty1]
forall a b. (a -> b) -> a -> b
$ \([Char]
c,[(Var, ())]
args',Exp1
rhs) -> do
           let args :: [Var]
args  = ((Var, ()) -> Var) -> [(Var, ())] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
L.map (Var, ()) -> Var
forall a b. (a, b) -> a
fst [(Var, ())]
args'
               targs :: [Ty1]
targs = DDefs1 -> [Char] -> [Ty1]
forall a. Out a => DDefs a -> [Char] -> [a]
lookupDataCon DDefs1
ddfs [Char]
c
               env' :: Env2 Ty1
env'  = Env2 Ty1 -> [(Var, Ty1)] -> Env2 Ty1
forall l. Env2 (UrTy l) -> [(Var, UrTy l)] -> Env2 (UrTy l)
extendEnv Env2 Ty1
env ([Var] -> [Ty1] -> [(Var, Ty1)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
args [Ty1]
targs)
           DDefs1 -> Env2 Ty1 -> Exp1 -> TcM Ty1 Exp1
tcExp DDefs1
ddfs Env2 Ty1
env' Exp1
rhs
  (Ty1 -> (Exp1, Ty1) -> TcM Ty1 Exp1)
-> Ty1 -> [(Exp1, Ty1)] -> ExceptT (TCError Exp1) Identity ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (\Ty1
acc (Exp1
ex,Ty1
ty) ->
            if Ty1
ty Ty1 -> Ty1 -> Bool
forall a. Eq a => a -> a -> Bool
== Ty1
acc
            then Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
acc
            else TCError Exp1 -> TcM Ty1 Exp1
forall a. TCError Exp1 -> ExceptT (TCError Exp1) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError Exp1 -> TcM Ty1 Exp1) -> TCError Exp1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp1 -> TCError Exp1
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Case branches have mismatched types: "
                                         [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
acc [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
ty) Exp1
ex)
         ([Ty1] -> Ty1
forall a. HasCallStack => [a] -> a
head [Ty1]
tys) ((Ty1 -> ([Char], [(Var, ())], Exp1) -> (Exp1, Ty1))
-> [Ty1] -> [([Char], [(Var, ())], Exp1)] -> [(Exp1, Ty1)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Ty1
ty ([Char]
_,[(Var, ())]
_,Exp1
ex) -> (Exp1
ex,Ty1
ty)) [Ty1]
tys [([Char], [(Var, ())], Exp1)]
cs)
  Ty1 -> TcM Ty1 Exp1
forall a. a -> ExceptT (TCError Exp1) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ty1 -> TcM Ty1 Exp1) -> Ty1 -> TcM Ty1 Exp1
forall a b. (a -> b) -> a -> b
$ [Ty1] -> Ty1
forall a. HasCallStack => [a] -> a
head [Ty1]
tys


checkLen :: (Out op, Out arg) => PreExp e () (UrTy ()) -> op -> Int -> [arg] ->
            TcM () (PreExp e () (UrTy ()))
checkLen :: forall op arg (e :: * -> * -> *).
(Out op, Out arg) =>
PreExp e () Ty1 -> op -> Int -> [arg] -> TcM () (PreExp e () Ty1)
checkLen PreExp e () Ty1
expr op
pr Int
n [arg]
ls =
  if [arg] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [arg]
ls Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n
  then () -> ExceptT (TCError (PreExp e () Ty1)) Identity ()
forall a. a -> ExceptT (TCError (PreExp e () Ty1)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  else TCError (PreExp e () Ty1)
-> ExceptT (TCError (PreExp e () Ty1)) Identity ()
forall a.
TCError (PreExp e () Ty1)
-> ExceptT (TCError (PreExp e () Ty1)) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError (PreExp e () Ty1)
 -> ExceptT (TCError (PreExp e () Ty1)) Identity ())
-> TCError (PreExp e () Ty1)
-> ExceptT (TCError (PreExp e () Ty1)) Identity ()
forall a b. (a -> b) -> a -> b
$ [Char] -> PreExp e () Ty1 -> TCError (PreExp e () Ty1)
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Wrong number of arguments to "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++op -> [Char]
forall a. Out a => a -> [Char]
sdoc op
pr[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                               [Char]
".\nExpected "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Int -> [Char]
forall a. Out a => a -> [Char]
sdoc Int
n[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
", received "
                                [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Int -> [Char]
forall a. Out a => a -> [Char]
sdoc ([arg] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [arg]
ls)[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
":\n  "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[arg] -> [Char]
forall a. Out a => a -> [Char]
sdoc [arg]
ls)
                    PreExp e () Ty1
expr

-- | Ensure that two things are equal.
-- Includes an expression for error reporting.
ensureEqual :: (Eq l) => PreExp e () (UrTy ()) -> String -> (UrTy l) ->
               (UrTy l) -> TcM (UrTy l) (PreExp e () (UrTy ()))
ensureEqual :: forall l (e :: * -> * -> *).
Eq l =>
PreExp e () Ty1
-> [Char] -> UrTy l -> UrTy l -> TcM (UrTy l) (PreExp e () Ty1)
ensureEqual PreExp e () Ty1
exp [Char]
str UrTy l
a UrTy l
b = if UrTy l
a UrTy l -> UrTy l -> Bool
forall a. Eq a => a -> a -> Bool
== UrTy l
b
                          then UrTy l -> ExceptT (TCError (PreExp e () Ty1)) Identity (UrTy l)
forall a. a -> ExceptT (TCError (PreExp e () Ty1)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return UrTy l
a
                          else TCError (PreExp e () Ty1)
-> ExceptT (TCError (PreExp e () Ty1)) Identity (UrTy l)
forall a.
TCError (PreExp e () Ty1)
-> ExceptT (TCError (PreExp e () Ty1)) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError (PreExp e () Ty1)
 -> ExceptT (TCError (PreExp e () Ty1)) Identity (UrTy l))
-> TCError (PreExp e () Ty1)
-> ExceptT (TCError (PreExp e () Ty1)) Identity (UrTy l)
forall a b. (a -> b) -> a -> b
$ [Char] -> PreExp e () Ty1 -> TCError (PreExp e () Ty1)
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
str PreExp e () Ty1
exp


-- | Ensure that two types are equal.
-- Includes an expression for error reporting.
-- ensureEqualTy :: (Eq l, Out l) => PreExp e () (UrTy ()) -> (UrTy l) -> (UrTy l) ->
--                  TcM (UrTy l) PreExp e () (UrTy ())
ensureEqualTy :: PreExp e () (UrTy ()) -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () (UrTy ()))
ensureEqualTy :: forall (e :: * -> * -> *).
PreExp e () Ty1 -> Ty1 -> Ty1 -> TcM Ty1 (PreExp e () Ty1)
ensureEqualTy PreExp e () Ty1
_exp Ty1
CursorTy Ty1
IntTy = Ty1 -> ExceptT (TCError (PreExp e () Ty1)) Identity Ty1
forall a. a -> ExceptT (TCError (PreExp e () Ty1)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
CursorTy
ensureEqualTy PreExp e () Ty1
_exp Ty1
IntTy Ty1
CursorTy = Ty1 -> ExceptT (TCError (PreExp e () Ty1)) Identity Ty1
forall a. a -> ExceptT (TCError (PreExp e () Ty1)) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Ty1
forall loc. UrTy loc
CursorTy
ensureEqualTy PreExp e () Ty1
exp Ty1
a Ty1
b = PreExp e () Ty1
-> [Char]
-> Ty1
-> Ty1
-> ExceptT (TCError (PreExp e () Ty1)) Identity Ty1
forall l (e :: * -> * -> *).
Eq l =>
PreExp e () Ty1
-> [Char] -> UrTy l -> UrTy l -> TcM (UrTy l) (PreExp e () Ty1)
ensureEqual PreExp e () Ty1
exp ([Char]
"Expected these types to be the same: "
                                         [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
a) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Ty1 -> [Char]
forall a. Out a => a -> [Char]
sdoc Ty1
b)) Ty1
a Ty1
b

ensureArenaScope :: MonadError (TCError exp) m => exp -> Env2 a -> Maybe Var -> m ()
ensureArenaScope :: forall exp (m :: * -> *) a.
MonadError (TCError exp) m =>
exp -> Env2 a -> Maybe Var -> m ()
ensureArenaScope exp
exp Env2 a
env Maybe Var
ar =
    case Maybe Var
ar of
      Maybe Var
Nothing -> TCError exp -> m ()
forall a. TCError exp -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError exp -> m ()) -> TCError exp -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> exp -> TCError exp
forall exp. [Char] -> exp -> TCError exp
GenericTC [Char]
"Expected arena annotation" exp
exp
      Just Var
var -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Var
var (Set Var -> Bool) -> (Env2 a -> Set Var) -> Env2 a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Var a -> Set Var
forall k a. Map k a -> Set k
M.keysSet (Map Var a -> Set Var)
-> (Env2 a -> Map Var a) -> Env2 a -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env2 a -> Map Var a
forall a. Env2 a -> TyEnv a
vEnv (Env2 a -> Bool) -> Env2 a -> Bool
forall a b. (a -> b) -> a -> b
$ Env2 a
env) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                  TCError exp -> m ()
forall a. TCError exp -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError exp -> m ()) -> TCError exp -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> exp -> TCError exp
forall exp. [Char] -> exp -> TCError exp
GenericTC ([Char]
"Expected arena in scope: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Out a => a -> [Char]
sdoc Var
var) exp
exp