{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fdefer-typed-holes #-}
{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}

-- |

module Gibbon.L2.Typecheck
    ( tcExp, tcProg, TCError(..)
    , RegionSet(..)
    , LocationTypeState(..)
    , ConstraintSet(..)
    , LocConstraint(..)
    , Aliased, TcM )
    where

import           Control.DeepSeq
import           Control.Monad
import           Control.Monad.Except
import           Data.Foldable ( foldlM )
import qualified Data.Set as S
import qualified Data.List as L
import qualified Data.Map as M
import           Data.Maybe
import           Text.PrettyPrint.GenericPretty

import           Gibbon.Common
import           Gibbon.L2.Syntax as L2
-- import qualified Gibbon.L1.Syntax as L1

-- | Constraints on locations.  Used during typechecking.  Roughly analogous to LocExp.
data LocConstraint = StartOfC LocVar Region -- ^ Location is equal to start of this region.
                   -- Can't attach haddocks to data constructor arguments with < GHC 8.4.2
                   -- See https://github.com/haskell/haddock/pull/709.
                   | AfterConstantC Int     -- Number of bytes after.
                                    LocVar  -- Location which is before
                                    LocVar  -- Location which is after
                   | AfterVariableC Var     -- Name of variable v. This loc is size(v) bytes after.
                                    LocVar  -- Location which is before
                                    LocVar  -- Location which is after
                   | InRegionC LocVar Region -- Location is somewher within this region.
  deriving (ReadPrec [LocConstraint]
ReadPrec LocConstraint
Int -> ReadS LocConstraint
ReadS [LocConstraint]
(Int -> ReadS LocConstraint)
-> ReadS [LocConstraint]
-> ReadPrec LocConstraint
-> ReadPrec [LocConstraint]
-> Read LocConstraint
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS LocConstraint
readsPrec :: Int -> ReadS LocConstraint
$creadList :: ReadS [LocConstraint]
readList :: ReadS [LocConstraint]
$creadPrec :: ReadPrec LocConstraint
readPrec :: ReadPrec LocConstraint
$creadListPrec :: ReadPrec [LocConstraint]
readListPrec :: ReadPrec [LocConstraint]
Read, Int -> LocConstraint -> ShowS
[LocConstraint] -> ShowS
LocConstraint -> String
(Int -> LocConstraint -> ShowS)
-> (LocConstraint -> String)
-> ([LocConstraint] -> ShowS)
-> Show LocConstraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LocConstraint -> ShowS
showsPrec :: Int -> LocConstraint -> ShowS
$cshow :: LocConstraint -> String
show :: LocConstraint -> String
$cshowList :: [LocConstraint] -> ShowS
showList :: [LocConstraint] -> ShowS
Show, LocConstraint -> LocConstraint -> Bool
(LocConstraint -> LocConstraint -> Bool)
-> (LocConstraint -> LocConstraint -> Bool) -> Eq LocConstraint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LocConstraint -> LocConstraint -> Bool
== :: LocConstraint -> LocConstraint -> Bool
$c/= :: LocConstraint -> LocConstraint -> Bool
/= :: LocConstraint -> LocConstraint -> Bool
Eq, Eq LocConstraint
Eq LocConstraint
-> (LocConstraint -> LocConstraint -> Ordering)
-> (LocConstraint -> LocConstraint -> Bool)
-> (LocConstraint -> LocConstraint -> Bool)
-> (LocConstraint -> LocConstraint -> Bool)
-> (LocConstraint -> LocConstraint -> Bool)
-> (LocConstraint -> LocConstraint -> LocConstraint)
-> (LocConstraint -> LocConstraint -> LocConstraint)
-> Ord LocConstraint
LocConstraint -> LocConstraint -> Bool
LocConstraint -> LocConstraint -> Ordering
LocConstraint -> LocConstraint -> LocConstraint
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
$ccompare :: LocConstraint -> LocConstraint -> Ordering
compare :: LocConstraint -> LocConstraint -> Ordering
$c< :: LocConstraint -> LocConstraint -> Bool
< :: LocConstraint -> LocConstraint -> Bool
$c<= :: LocConstraint -> LocConstraint -> Bool
<= :: LocConstraint -> LocConstraint -> Bool
$c> :: LocConstraint -> LocConstraint -> Bool
> :: LocConstraint -> LocConstraint -> Bool
$c>= :: LocConstraint -> LocConstraint -> Bool
>= :: LocConstraint -> LocConstraint -> Bool
$cmax :: LocConstraint -> LocConstraint -> LocConstraint
max :: LocConstraint -> LocConstraint -> LocConstraint
$cmin :: LocConstraint -> LocConstraint -> LocConstraint
min :: LocConstraint -> LocConstraint -> LocConstraint
Ord, (forall x. LocConstraint -> Rep LocConstraint x)
-> (forall x. Rep LocConstraint x -> LocConstraint)
-> Generic LocConstraint
forall x. Rep LocConstraint x -> LocConstraint
forall x. LocConstraint -> Rep LocConstraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LocConstraint -> Rep LocConstraint x
from :: forall x. LocConstraint -> Rep LocConstraint x
$cto :: forall x. Rep LocConstraint x -> LocConstraint
to :: forall x. Rep LocConstraint x -> LocConstraint
Generic, LocConstraint -> ()
(LocConstraint -> ()) -> NFData LocConstraint
forall a. (a -> ()) -> NFData a
$crnf :: LocConstraint -> ()
rnf :: LocConstraint -> ()
NFData, Int -> LocConstraint -> Doc
[LocConstraint] -> Doc
LocConstraint -> Doc
(Int -> LocConstraint -> Doc)
-> (LocConstraint -> Doc)
-> ([LocConstraint] -> Doc)
-> Out LocConstraint
forall a. (Int -> a -> Doc) -> (a -> Doc) -> ([a] -> Doc) -> Out a
$cdocPrec :: Int -> LocConstraint -> Doc
docPrec :: Int -> LocConstraint -> Doc
$cdoc :: LocConstraint -> Doc
doc :: LocConstraint -> Doc
$cdocList :: [LocConstraint] -> Doc
docList :: [LocConstraint] -> Doc
Out)


-- | A set of constraints (which are re-used location expressions)
-- which encode relationships between locations. These are used by the
-- type checker to verify that locations are used correctly.
--
-- The following are valid constraints:
--  * StartOfC LocVar Region
--  * AfterConstantC Int LocVar LocVar
--  * AfterVariableC Var LocVar LocVar
--  * InRegionC LocVar Region
--  * FromEndC
--
-- While the first four can appear in syntax before RouteEnds, the fifth
-- (fromEnd) should only be introduced by the RouteEnds pass.
newtype ConstraintSet = ConstraintSet { ConstraintSet -> Set LocConstraint
constraintSet :: S.Set LocConstraint }
  deriving (ReadPrec [ConstraintSet]
ReadPrec ConstraintSet
Int -> ReadS ConstraintSet
ReadS [ConstraintSet]
(Int -> ReadS ConstraintSet)
-> ReadS [ConstraintSet]
-> ReadPrec ConstraintSet
-> ReadPrec [ConstraintSet]
-> Read ConstraintSet
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS ConstraintSet
readsPrec :: Int -> ReadS ConstraintSet
$creadList :: ReadS [ConstraintSet]
readList :: ReadS [ConstraintSet]
$creadPrec :: ReadPrec ConstraintSet
readPrec :: ReadPrec ConstraintSet
$creadListPrec :: ReadPrec [ConstraintSet]
readListPrec :: ReadPrec [ConstraintSet]
Read, Int -> ConstraintSet -> ShowS
[ConstraintSet] -> ShowS
ConstraintSet -> String
(Int -> ConstraintSet -> ShowS)
-> (ConstraintSet -> String)
-> ([ConstraintSet] -> ShowS)
-> Show ConstraintSet
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConstraintSet -> ShowS
showsPrec :: Int -> ConstraintSet -> ShowS
$cshow :: ConstraintSet -> String
show :: ConstraintSet -> String
$cshowList :: [ConstraintSet] -> ShowS
showList :: [ConstraintSet] -> ShowS
Show, ConstraintSet -> ConstraintSet -> Bool
(ConstraintSet -> ConstraintSet -> Bool)
-> (ConstraintSet -> ConstraintSet -> Bool) -> Eq ConstraintSet
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ConstraintSet -> ConstraintSet -> Bool
== :: ConstraintSet -> ConstraintSet -> Bool
$c/= :: ConstraintSet -> ConstraintSet -> Bool
/= :: ConstraintSet -> ConstraintSet -> Bool
Eq, Eq ConstraintSet
Eq ConstraintSet
-> (ConstraintSet -> ConstraintSet -> Ordering)
-> (ConstraintSet -> ConstraintSet -> Bool)
-> (ConstraintSet -> ConstraintSet -> Bool)
-> (ConstraintSet -> ConstraintSet -> Bool)
-> (ConstraintSet -> ConstraintSet -> Bool)
-> (ConstraintSet -> ConstraintSet -> ConstraintSet)
-> (ConstraintSet -> ConstraintSet -> ConstraintSet)
-> Ord ConstraintSet
ConstraintSet -> ConstraintSet -> Bool
ConstraintSet -> ConstraintSet -> Ordering
ConstraintSet -> ConstraintSet -> ConstraintSet
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
$ccompare :: ConstraintSet -> ConstraintSet -> Ordering
compare :: ConstraintSet -> ConstraintSet -> Ordering
$c< :: ConstraintSet -> ConstraintSet -> Bool
< :: ConstraintSet -> ConstraintSet -> Bool
$c<= :: ConstraintSet -> ConstraintSet -> Bool
<= :: ConstraintSet -> ConstraintSet -> Bool
$c> :: ConstraintSet -> ConstraintSet -> Bool
> :: ConstraintSet -> ConstraintSet -> Bool
$c>= :: ConstraintSet -> ConstraintSet -> Bool
>= :: ConstraintSet -> ConstraintSet -> Bool
$cmax :: ConstraintSet -> ConstraintSet -> ConstraintSet
max :: ConstraintSet -> ConstraintSet -> ConstraintSet
$cmin :: ConstraintSet -> ConstraintSet -> ConstraintSet
min :: ConstraintSet -> ConstraintSet -> ConstraintSet
Ord, (forall x. ConstraintSet -> Rep ConstraintSet x)
-> (forall x. Rep ConstraintSet x -> ConstraintSet)
-> Generic ConstraintSet
forall x. Rep ConstraintSet x -> ConstraintSet
forall x. ConstraintSet -> Rep ConstraintSet x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ConstraintSet -> Rep ConstraintSet x
from :: forall x. ConstraintSet -> Rep ConstraintSet x
$cto :: forall x. Rep ConstraintSet x -> ConstraintSet
to :: forall x. Rep ConstraintSet x -> ConstraintSet
Generic, ConstraintSet -> ()
(ConstraintSet -> ()) -> NFData ConstraintSet
forall a. (a -> ()) -> NFData a
$crnf :: ConstraintSet -> ()
rnf :: ConstraintSet -> ()
NFData, Int -> ConstraintSet -> Doc
[ConstraintSet] -> Doc
ConstraintSet -> Doc
(Int -> ConstraintSet -> Doc)
-> (ConstraintSet -> Doc)
-> ([ConstraintSet] -> Doc)
-> Out ConstraintSet
forall a. (Int -> a -> Doc) -> (a -> Doc) -> ([a] -> Doc) -> Out a
$cdocPrec :: Int -> ConstraintSet -> Doc
docPrec :: Int -> ConstraintSet -> Doc
$cdoc :: ConstraintSet -> Doc
doc :: ConstraintSet -> Doc
$cdocList :: [ConstraintSet] -> Doc
docList :: [ConstraintSet] -> Doc
Out)

-- | A location has been aliased if we have taken an offset of it while introducing a new
-- location. These show up in the LocationTypeState below.
type Aliased = Bool

-- | A map from locations to their type state. This tracks the current state of a location
-- at a certain point in a program. The type checker threads this through by taking an
-- input map that represents the location states before checking a particular expression,
-- and returns an output map that represents the location states after checking that
-- particular expression.
-- All we need to know in this map is whether each location is an input or output location,
-- and whether we've taken an offset of the location in a letloc form.
newtype LocationTypeState = LocationTypeState
    {
      LocationTypeState -> Map LocVar (Modality, Bool)
tsmap :: M.Map LocVar (Modality,Aliased)
      -- ^ Each location has a modality and may have had an offset taken.
    }
    deriving (ReadPrec [LocationTypeState]
ReadPrec LocationTypeState
Int -> ReadS LocationTypeState
ReadS [LocationTypeState]
(Int -> ReadS LocationTypeState)
-> ReadS [LocationTypeState]
-> ReadPrec LocationTypeState
-> ReadPrec [LocationTypeState]
-> Read LocationTypeState
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS LocationTypeState
readsPrec :: Int -> ReadS LocationTypeState
$creadList :: ReadS [LocationTypeState]
readList :: ReadS [LocationTypeState]
$creadPrec :: ReadPrec LocationTypeState
readPrec :: ReadPrec LocationTypeState
$creadListPrec :: ReadPrec [LocationTypeState]
readListPrec :: ReadPrec [LocationTypeState]
Read,Int -> LocationTypeState -> ShowS
[LocationTypeState] -> ShowS
LocationTypeState -> String
(Int -> LocationTypeState -> ShowS)
-> (LocationTypeState -> String)
-> ([LocationTypeState] -> ShowS)
-> Show LocationTypeState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LocationTypeState -> ShowS
showsPrec :: Int -> LocationTypeState -> ShowS
$cshow :: LocationTypeState -> String
show :: LocationTypeState -> String
$cshowList :: [LocationTypeState] -> ShowS
showList :: [LocationTypeState] -> ShowS
Show,LocationTypeState -> LocationTypeState -> Bool
(LocationTypeState -> LocationTypeState -> Bool)
-> (LocationTypeState -> LocationTypeState -> Bool)
-> Eq LocationTypeState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LocationTypeState -> LocationTypeState -> Bool
== :: LocationTypeState -> LocationTypeState -> Bool
$c/= :: LocationTypeState -> LocationTypeState -> Bool
/= :: LocationTypeState -> LocationTypeState -> Bool
Eq,Eq LocationTypeState
Eq LocationTypeState
-> (LocationTypeState -> LocationTypeState -> Ordering)
-> (LocationTypeState -> LocationTypeState -> Bool)
-> (LocationTypeState -> LocationTypeState -> Bool)
-> (LocationTypeState -> LocationTypeState -> Bool)
-> (LocationTypeState -> LocationTypeState -> Bool)
-> (LocationTypeState -> LocationTypeState -> LocationTypeState)
-> (LocationTypeState -> LocationTypeState -> LocationTypeState)
-> Ord LocationTypeState
LocationTypeState -> LocationTypeState -> Bool
LocationTypeState -> LocationTypeState -> Ordering
LocationTypeState -> LocationTypeState -> LocationTypeState
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
$ccompare :: LocationTypeState -> LocationTypeState -> Ordering
compare :: LocationTypeState -> LocationTypeState -> Ordering
$c< :: LocationTypeState -> LocationTypeState -> Bool
< :: LocationTypeState -> LocationTypeState -> Bool
$c<= :: LocationTypeState -> LocationTypeState -> Bool
<= :: LocationTypeState -> LocationTypeState -> Bool
$c> :: LocationTypeState -> LocationTypeState -> Bool
> :: LocationTypeState -> LocationTypeState -> Bool
$c>= :: LocationTypeState -> LocationTypeState -> Bool
>= :: LocationTypeState -> LocationTypeState -> Bool
$cmax :: LocationTypeState -> LocationTypeState -> LocationTypeState
max :: LocationTypeState -> LocationTypeState -> LocationTypeState
$cmin :: LocationTypeState -> LocationTypeState -> LocationTypeState
min :: LocationTypeState -> LocationTypeState -> LocationTypeState
Ord, (forall x. LocationTypeState -> Rep LocationTypeState x)
-> (forall x. Rep LocationTypeState x -> LocationTypeState)
-> Generic LocationTypeState
forall x. Rep LocationTypeState x -> LocationTypeState
forall x. LocationTypeState -> Rep LocationTypeState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LocationTypeState -> Rep LocationTypeState x
from :: forall x. LocationTypeState -> Rep LocationTypeState x
$cto :: forall x. Rep LocationTypeState x -> LocationTypeState
to :: forall x. Rep LocationTypeState x -> LocationTypeState
Generic, LocationTypeState -> ()
(LocationTypeState -> ()) -> NFData LocationTypeState
forall a. (a -> ()) -> NFData a
$crnf :: LocationTypeState -> ()
rnf :: LocationTypeState -> ()
NFData, Int -> LocationTypeState -> Doc
[LocationTypeState] -> Doc
LocationTypeState -> Doc
(Int -> LocationTypeState -> Doc)
-> (LocationTypeState -> Doc)
-> ([LocationTypeState] -> Doc)
-> Out LocationTypeState
forall a. (Int -> a -> Doc) -> (a -> Doc) -> ([a] -> Doc) -> Out a
$cdocPrec :: Int -> LocationTypeState -> Doc
docPrec :: Int -> LocationTypeState -> Doc
$cdoc :: LocationTypeState -> Doc
doc :: LocationTypeState -> Doc
$cdocList :: [LocationTypeState] -> Doc
docList :: [LocationTypeState] -> Doc
Out)

-- | A region set is (as you would expect) a set of regions. They are the
-- regions that are currently live while checking a particular expression.
newtype RegionSet = RegionSet { RegionSet -> Set LocVar
regSet :: S.Set Var }
  deriving (ReadPrec [RegionSet]
ReadPrec RegionSet
Int -> ReadS RegionSet
ReadS [RegionSet]
(Int -> ReadS RegionSet)
-> ReadS [RegionSet]
-> ReadPrec RegionSet
-> ReadPrec [RegionSet]
-> Read RegionSet
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS RegionSet
readsPrec :: Int -> ReadS RegionSet
$creadList :: ReadS [RegionSet]
readList :: ReadS [RegionSet]
$creadPrec :: ReadPrec RegionSet
readPrec :: ReadPrec RegionSet
$creadListPrec :: ReadPrec [RegionSet]
readListPrec :: ReadPrec [RegionSet]
Read, Int -> RegionSet -> ShowS
[RegionSet] -> ShowS
RegionSet -> String
(Int -> RegionSet -> ShowS)
-> (RegionSet -> String)
-> ([RegionSet] -> ShowS)
-> Show RegionSet
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RegionSet -> ShowS
showsPrec :: Int -> RegionSet -> ShowS
$cshow :: RegionSet -> String
show :: RegionSet -> String
$cshowList :: [RegionSet] -> ShowS
showList :: [RegionSet] -> ShowS
Show, RegionSet -> RegionSet -> Bool
(RegionSet -> RegionSet -> Bool)
-> (RegionSet -> RegionSet -> Bool) -> Eq RegionSet
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RegionSet -> RegionSet -> Bool
== :: RegionSet -> RegionSet -> Bool
$c/= :: RegionSet -> RegionSet -> Bool
/= :: RegionSet -> RegionSet -> Bool
Eq, Eq RegionSet
Eq RegionSet
-> (RegionSet -> RegionSet -> Ordering)
-> (RegionSet -> RegionSet -> Bool)
-> (RegionSet -> RegionSet -> Bool)
-> (RegionSet -> RegionSet -> Bool)
-> (RegionSet -> RegionSet -> Bool)
-> (RegionSet -> RegionSet -> RegionSet)
-> (RegionSet -> RegionSet -> RegionSet)
-> Ord RegionSet
RegionSet -> RegionSet -> Bool
RegionSet -> RegionSet -> Ordering
RegionSet -> RegionSet -> RegionSet
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
$ccompare :: RegionSet -> RegionSet -> Ordering
compare :: RegionSet -> RegionSet -> Ordering
$c< :: RegionSet -> RegionSet -> Bool
< :: RegionSet -> RegionSet -> Bool
$c<= :: RegionSet -> RegionSet -> Bool
<= :: RegionSet -> RegionSet -> Bool
$c> :: RegionSet -> RegionSet -> Bool
> :: RegionSet -> RegionSet -> Bool
$c>= :: RegionSet -> RegionSet -> Bool
>= :: RegionSet -> RegionSet -> Bool
$cmax :: RegionSet -> RegionSet -> RegionSet
max :: RegionSet -> RegionSet -> RegionSet
$cmin :: RegionSet -> RegionSet -> RegionSet
min :: RegionSet -> RegionSet -> RegionSet
Ord, (forall x. RegionSet -> Rep RegionSet x)
-> (forall x. Rep RegionSet x -> RegionSet) -> Generic RegionSet
forall x. Rep RegionSet x -> RegionSet
forall x. RegionSet -> Rep RegionSet x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RegionSet -> Rep RegionSet x
from :: forall x. RegionSet -> Rep RegionSet x
$cto :: forall x. Rep RegionSet x -> RegionSet
to :: forall x. Rep RegionSet x -> RegionSet
Generic, RegionSet -> ()
(RegionSet -> ()) -> NFData RegionSet
forall a. (a -> ()) -> NFData a
$crnf :: RegionSet -> ()
rnf :: RegionSet -> ()
NFData)


-- | Shorthand for located expressions
type Exp = Exp2

-- | These are the kinds of errors that the type checker may throw. There are a
-- few named errors that I thought would be common, like variables not being
-- found, locations being used incorrectly, etc. For other errors, there's a
-- GenericTC form that takes some expression and string
-- (containing an error message).
data TCError = GenericTC String Exp
             | VarNotFoundTC Var Exp
             | UnsupportedExpTC Exp
             | LocationTC String Exp LocVar LocVar
             | ModalityTC String Exp LocVar LocationTypeState
               deriving (ReadPrec [TCError]
ReadPrec TCError
Int -> ReadS TCError
ReadS [TCError]
(Int -> ReadS TCError)
-> ReadS [TCError]
-> ReadPrec TCError
-> ReadPrec [TCError]
-> Read TCError
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS TCError
readsPrec :: Int -> ReadS TCError
$creadList :: ReadS [TCError]
readList :: ReadS [TCError]
$creadPrec :: ReadPrec TCError
readPrec :: ReadPrec TCError
$creadListPrec :: ReadPrec [TCError]
readListPrec :: ReadPrec [TCError]
Read,TCError -> TCError -> Bool
(TCError -> TCError -> Bool)
-> (TCError -> TCError -> Bool) -> Eq TCError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TCError -> TCError -> Bool
== :: TCError -> TCError -> Bool
$c/= :: TCError -> TCError -> Bool
/= :: TCError -> TCError -> Bool
Eq,Eq TCError
Eq TCError
-> (TCError -> TCError -> Ordering)
-> (TCError -> TCError -> Bool)
-> (TCError -> TCError -> Bool)
-> (TCError -> TCError -> Bool)
-> (TCError -> TCError -> Bool)
-> (TCError -> TCError -> TCError)
-> (TCError -> TCError -> TCError)
-> Ord TCError
TCError -> TCError -> Bool
TCError -> TCError -> Ordering
TCError -> TCError -> TCError
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
$ccompare :: TCError -> TCError -> Ordering
compare :: TCError -> TCError -> Ordering
$c< :: TCError -> TCError -> Bool
< :: TCError -> TCError -> Bool
$c<= :: TCError -> TCError -> Bool
<= :: TCError -> TCError -> Bool
$c> :: TCError -> TCError -> Bool
> :: TCError -> TCError -> Bool
$c>= :: TCError -> TCError -> Bool
>= :: TCError -> TCError -> Bool
$cmax :: TCError -> TCError -> TCError
max :: TCError -> TCError -> TCError
$cmin :: TCError -> TCError -> TCError
min :: TCError -> TCError -> TCError
Ord,(forall x. TCError -> Rep TCError x)
-> (forall x. Rep TCError x -> TCError) -> Generic TCError
forall x. Rep TCError x -> TCError
forall x. TCError -> Rep TCError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TCError -> Rep TCError x
from :: forall x. TCError -> Rep TCError x
$cto :: forall x. Rep TCError x -> TCError
to :: forall x. Rep TCError x -> TCError
Generic,TCError -> ()
(TCError -> ()) -> NFData TCError
forall a. (a -> ()) -> NFData a
$crnf :: TCError -> ()
rnf :: TCError -> ()
NFData)

instance Show TCError where
    show :: TCError -> String
show (GenericTC String
str Exp
e) = String
"Error typechecking L2 Program\nIn the expression:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Exp -> String
forall a. Out a => a -> String
sdoc Exp
e) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
    show (VarNotFoundTC LocVar
v Exp
e) = String
"Variable not found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocVar -> String
forall a. Show a => a -> String
show LocVar
v) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nIn the expression:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Exp -> String
forall a. Out a => a -> String
sdoc Exp
e) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
    show (UnsupportedExpTC Exp
e) = String
"Unsupported expression:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Exp -> String
forall a. Out a => a -> String
sdoc Exp
e) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
    show (LocationTC String
str Exp
e LocVar
lv1 LocVar
lv2) = String
"Location typechecking error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nIn the expression:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Exp -> String
forall a. Out a => a -> String
sdoc Exp
e)
                                      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nLocations: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocVar -> String
forall a. Show a => a -> String
show LocVar
lv1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocVar -> String
forall a. Show a => a -> String
show LocVar
lv2) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
    show (ModalityTC String
str Exp
e LocVar
lv LocationTypeState
lts) = String
"Modality typechecking error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nIn the expression:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Exp -> String
forall a. Out a => a -> String
sdoc Exp
e)
                                     String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nLocation: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocVar -> String
forall a. Show a => a -> String
show LocVar
lv) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nLocation type state: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocationTypeState -> String
forall a. Show a => a -> String
show LocationTypeState
lts) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"

-- | The type checking monad. Just for throwing errors, but could in the future be parameterized
--   by whatever other logging, etc, monad we want the compiler to use.
type TcM a = (Except TCError) a



-- | Check an expression. Given the data definitions, an general type environment, a function map,
--   a constraint set, a region set, an (input) location state map, and the expression, this function
--   will either throw an error, or return a pair of expression type and new location state map.
tcExp :: DDefs Ty2 -> Env2 Ty2 -> FunDefs2
      -> ConstraintSet -> RegionSet -> LocationTypeState -> Exp
      -> TcM (Ty2, LocationTypeState)
tcExp :: DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein Exp
exp =

    case Exp
exp of

      VarE LocVar
v ->
          -- Look up a variable in the environment
          do UrTy LocVar
ty <- Env2 (UrTy LocVar) -> LocVar -> Exp -> TcM (UrTy LocVar)
lookupVar Env2 (UrTy LocVar)
env LocVar
v Exp
exp
             (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty, LocationTypeState
tstatein)

      LitE Int
_i -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
IntTy, LocationTypeState
tstatein)

      CharE Char
_i -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
CharTy, LocationTypeState
tstatein)

      FloatE Double
_i -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
FloatTy, LocationTypeState
tstatein)

      LitSymE LocVar
_v -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
SymTy, LocationTypeState
tstatein)

      AppE LocVar
v [LocVar]
ls [Exp]
args ->
          -- Checking function application involves a few steps:
          --  (1) We need to make sure the inputs/ouptuts line up with the expected
          --      types for the function.
          --  (2) We need to update the location state map with information about what output
          --      locations have been written to by the called function and must now be input
          --      locations.
          --  (3) We need to make sure that if we pass a packed structure as an argument, its
          --      location is among the passed-in locations.
          do let (ArrowTy2 [LRM]
locVars [UrTy LocVar]
arrIns Set Effect
_arrEffs UrTy LocVar
arrOut [LocRet]
_locRets Bool
_isPar) =
                     case LocVar -> FunDefs2 -> Maybe (FunDef Exp)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup LocVar
v FunDefs2
funs of
                       Just FunDef Exp
f -> FunDef Exp -> ArrowTy (TyOf Exp)
forall ex. FunDef ex -> ArrowTy (TyOf ex)
funTy FunDef Exp
f
                       Maybe (FunDef Exp)
Nothing -> String -> ArrowTy2 (UrTy LocVar)
forall a. HasCallStack => String -> a
error (String -> ArrowTy2 (UrTy LocVar))
-> String -> ArrowTy2 (UrTy LocVar)
forall a b. (a -> b) -> a -> b
$ String
"tcExp: Unbound function: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ LocVar -> String
forall a. Out a => a -> String
sdoc LocVar
v

             -- Get types of arguments
             ([UrTy LocVar]
in_tys, LocationTypeState
tstate) <- (([UrTy LocVar], LocationTypeState)
 -> Exp
 -> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState))
-> ([UrTy LocVar], LocationTypeState)
-> [Exp]
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
                                   (\([UrTy LocVar]
tys, LocationTypeState
st) Exp
a -> do
                                         (UrTy LocVar
ty, LocationTypeState
st') <- LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
st Exp
a
                                         ([UrTy LocVar], LocationTypeState)
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([UrTy LocVar]
tys [UrTy LocVar] -> [UrTy LocVar] -> [UrTy LocVar]
forall a. [a] -> [a] -> [a]
++ [UrTy LocVar
ty], LocationTypeState
st'))
                                   ([],LocationTypeState
tstatein) [Exp]
args

             -- Check arity
             if ([Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp]
args) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= ([UrTy LocVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [UrTy LocVar]
in_tys)
               then TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Arity mismatch. Expected:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([UrTy LocVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [UrTy LocVar]
in_tys) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" Got:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp]
args)) Exp
exp
               else () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

             -- (1)
             ((UrTy LocVar, UrTy LocVar) -> TcM (UrTy LocVar))
-> [(UrTy LocVar, UrTy LocVar)]
-> ExceptT TCError Identity [UrTy LocVar]
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 ((UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar))
-> (UrTy LocVar, UrTy LocVar) -> TcM (UrTy LocVar)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar))
 -> (UrTy LocVar, UrTy LocVar) -> TcM (UrTy LocVar))
-> (UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar))
-> (UrTy LocVar, UrTy LocVar)
-> TcM (UrTy LocVar)
forall a b. (a -> b) -> a -> b
$ Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyNoLoc Exp
exp) ([UrTy LocVar] -> [UrTy LocVar] -> [(UrTy LocVar, UrTy LocVar)]
forall a b.
(Show a, Show b, HasCallStack) =>
[a] -> [b] -> [(a, b)]
fragileZip [UrTy LocVar]
in_tys [UrTy LocVar]
arrIns)

             -- (3) Check location of argument
             let tyls :: [LocVar]
tyls = (UrTy LocVar -> [LocVar]) -> [UrTy LocVar] -> [LocVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap UrTy LocVar -> [LocVar]
locsInTy [UrTy LocVar]
in_tys
             case (LocVar -> Bool) -> [LocVar] -> Maybe LocVar
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (\LocVar
loc -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ LocVar -> Set LocVar -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member LocVar
loc ([LocVar] -> Set LocVar
forall a. Ord a => [a] -> Set a
S.fromList [LocVar]
ls)) [LocVar]
tyls of
               Maybe LocVar
Nothing -> () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
               Just LocVar
not_in_ls -> TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Packed argument location expected: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ LocVar -> String
forall a. Show a => a -> String
show LocVar
not_in_ls) Exp
exp
             let handleTS :: LocationTypeState -> (LocVar, Modality) -> TcM LocationTypeState
handleTS LocationTypeState
ts (LocVar
l,Modality
Output) =  Exp -> LocationTypeState -> LocVar -> TcM LocationTypeState
switchOutLoc Exp
exp LocationTypeState
ts LocVar
l
                 handleTS LocationTypeState
ts (LocVar, Modality)
_ = LocationTypeState -> TcM LocationTypeState
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return LocationTypeState
ts
             -- (2)
             LocationTypeState
tstate' <- (LocationTypeState -> (LocVar, Modality) -> TcM LocationTypeState)
-> LocationTypeState
-> [(LocVar, Modality)]
-> TcM LocationTypeState
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM LocationTypeState -> (LocVar, Modality) -> TcM LocationTypeState
handleTS LocationTypeState
tstate ([(LocVar, Modality)] -> TcM LocationTypeState)
-> [(LocVar, Modality)] -> TcM LocationTypeState
forall a b. (a -> b) -> a -> b
$ [LocVar] -> [Modality] -> [(LocVar, Modality)]
forall a b. [a] -> [b] -> [(a, b)]
zip [LocVar]
ls ([Modality] -> [(LocVar, Modality)])
-> [Modality] -> [(LocVar, Modality)]
forall a b. (a -> b) -> a -> b
$ (LRM -> Modality) -> [LRM] -> [Modality]
forall a b. (a -> b) -> [a] -> [b]
L.map (\(LRM LocVar
_ Region
_ Modality
m) -> Modality
m) [LRM]
locVars
             -- Use locVars used at call-site in the returned type
             let arrOutMp :: Map LocVar LocVar
arrOutMp = [(LocVar, LocVar)] -> Map LocVar LocVar
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(LocVar, LocVar)] -> Map LocVar LocVar)
-> [(LocVar, LocVar)] -> Map LocVar LocVar
forall a b. (a -> b) -> a -> b
$ [LocVar] -> [LocVar] -> [(LocVar, LocVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((LRM -> LocVar) -> [LRM] -> [LocVar]
forall a b. (a -> b) -> [a] -> [b]
L.map (\(LRM LocVar
l Region
_ Modality
_) -> LocVar
l) [LRM]
locVars) [LocVar]
ls
                 arrOut' :: UrTy LocVar
arrOut'  = Map LocVar LocVar -> UrTy LocVar -> UrTy LocVar
substLoc Map LocVar LocVar
arrOutMp UrTy LocVar
arrOut

             (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
arrOut',LocationTypeState
tstate')

      PrimAppE Prim (UrTy LocVar)
pr [Exp]
es -> do
               -- Special case because we can't lookup the type of the function pointer
               let es' :: [Exp]
es' = case Prim (UrTy LocVar)
pr of
                           VSortP{} -> [Exp] -> [Exp]
forall a. HasCallStack => [a] -> [a]
init [Exp]
es
                           InplaceVSortP{} -> [Exp] -> [Exp]
forall a. HasCallStack => [a] -> [a]
init [Exp]
es
                           Prim (UrTy LocVar)
_        -> [Exp]
es
               ([UrTy LocVar]
tys,LocationTypeState
tstate) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> [Exp]
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
tcExps DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein [Exp]
es'

               -- Pattern matches would be one way to check length safely, but then the
               -- error would not go through our monad:
               let len2 :: ExceptT TCError Identity ()
len2 = Exp
-> Prim (UrTy LocVar)
-> Int
-> [Exp]
-> ExceptT TCError Identity ()
forall op arg.
(Show op, Show arg) =>
Exp -> op -> Int -> [arg] -> ExceptT TCError Identity ()
checkLen Exp
exp Prim (UrTy LocVar)
pr Int
2 [Exp]
es
                   len1 :: ExceptT TCError Identity ()
len1 = Exp
-> Prim (UrTy LocVar)
-> Int
-> [Exp]
-> ExceptT TCError Identity ()
forall op arg.
(Show op, Show arg) =>
Exp -> op -> Int -> [arg] -> ExceptT TCError Identity ()
checkLen Exp
exp Prim (UrTy LocVar)
pr Int
1 [Exp]
es
                   len0 :: ExceptT TCError Identity ()
len0 = Exp
-> Prim (UrTy LocVar)
-> Int
-> [Exp]
-> ExceptT TCError Identity ()
forall op arg.
(Show op, Show arg) =>
Exp -> op -> Int -> [arg] -> ExceptT TCError Identity ()
checkLen Exp
exp Prim (UrTy LocVar)
pr Int
0 [Exp]
es
                   len3 :: ExceptT TCError Identity ()
len3 = Exp
-> Prim (UrTy LocVar)
-> Int
-> [Exp]
-> ExceptT TCError Identity ()
forall op arg.
(Show op, Show arg) =>
Exp -> op -> Int -> [arg] -> ExceptT TCError Identity ()
checkLen Exp
exp Prim (UrTy LocVar)
pr Int
3 [Exp]
es
                   len4 :: ExceptT TCError Identity ()
len4 = Exp
-> Prim (UrTy LocVar)
-> Int
-> [Exp]
-> ExceptT TCError Identity ()
forall op arg.
(Show op, Show arg) =>
Exp -> op -> Int -> [arg] -> ExceptT TCError Identity ()
checkLen Exp
exp Prim (UrTy LocVar)
pr Int
4 [Exp]
es

                   mk_bools :: TcM (UrTy LocVar, LocationTypeState)
mk_bools = do
                     ExceptT TCError Identity ()
len0
                     (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
BoolTy, LocationTypeState
tstate)

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

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

                   float_ops :: TcM (UrTy LocVar, LocationTypeState)
float_ops = do
                     ExceptT TCError Identity ()
len2
                     UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) UrTy LocVar
forall loc. UrTy loc
FloatTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
                     UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) UrTy LocVar
forall loc. UrTy loc
FloatTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                     (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
FloatTy, LocationTypeState
tstate)

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

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

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

               case Prim (UrTy LocVar)
pr of
                 Prim (UrTy LocVar)
MkTrue  -> TcM (UrTy LocVar, LocationTypeState)
mk_bools
                 Prim (UrTy LocVar)
MkFalse -> TcM (UrTy LocVar, LocationTypeState)
mk_bools
                 Prim (UrTy LocVar)
AddP    -> TcM (UrTy LocVar, LocationTypeState)
int_ops
                 Prim (UrTy LocVar)
SubP    -> TcM (UrTy LocVar, LocationTypeState)
int_ops
                 Prim (UrTy LocVar)
MulP    -> TcM (UrTy LocVar, LocationTypeState)
int_ops
                 Prim (UrTy LocVar)
DivP    -> TcM (UrTy LocVar, LocationTypeState)
int_ops
                 Prim (UrTy LocVar)
ModP    -> TcM (UrTy LocVar, LocationTypeState)
int_ops
                 Prim (UrTy LocVar)
ExpP    -> TcM (UrTy LocVar, LocationTypeState)
int_ops
                 Prim (UrTy LocVar)
FAddP   -> TcM (UrTy LocVar, LocationTypeState)
float_ops
                 Prim (UrTy LocVar)
FSubP   -> TcM (UrTy LocVar, LocationTypeState)
float_ops
                 Prim (UrTy LocVar)
FMulP   -> TcM (UrTy LocVar, LocationTypeState)
float_ops
                 Prim (UrTy LocVar)
FDivP   -> TcM (UrTy LocVar, LocationTypeState)
float_ops
                 Prim (UrTy LocVar)
FExpP   -> TcM (UrTy LocVar, LocationTypeState)
float_ops
                 Prim (UrTy LocVar)
EqIntP  -> TcM (UrTy LocVar, LocationTypeState)
int_cmps
                 Prim (UrTy LocVar)
LtP     -> TcM (UrTy LocVar, LocationTypeState)
int_cmps
                 Prim (UrTy LocVar)
GtP     -> TcM (UrTy LocVar, LocationTypeState)
int_cmps
                 Prim (UrTy LocVar)
LtEqP   -> TcM (UrTy LocVar, LocationTypeState)
int_cmps
                 Prim (UrTy LocVar)
GtEqP   -> TcM (UrTy LocVar, LocationTypeState)
int_cmps
                 Prim (UrTy LocVar)
EqFloatP -> TcM (UrTy LocVar, LocationTypeState)
float_cmps
                 Prim (UrTy LocVar)
EqCharP  -> TcM (UrTy LocVar, LocationTypeState)
char_cmps
                 Prim (UrTy LocVar)
FLtP     -> TcM (UrTy LocVar, LocationTypeState)
float_cmps
                 Prim (UrTy LocVar)
FGtP     -> TcM (UrTy LocVar, LocationTypeState)
float_cmps
                 Prim (UrTy LocVar)
FLtEqP   -> TcM (UrTy LocVar, LocationTypeState)
float_cmps
                 Prim (UrTy LocVar)
FGtEqP   -> TcM (UrTy LocVar, LocationTypeState)
float_cmps
                 Prim (UrTy LocVar)
OrP     -> TcM (UrTy LocVar, LocationTypeState)
bool_ops
                 Prim (UrTy LocVar)
AndP    -> TcM (UrTy LocVar, LocationTypeState)
bool_ops

                 Prim (UrTy LocVar)
RandP -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
IntTy, LocationTypeState
tstate)
                 Prim (UrTy LocVar)
FRandP -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
FloatTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
FloatToIntP -> do
                   ExceptT TCError Identity ()
len1
                   Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
FloatTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
IntTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
IntToFloatP -> do
                   ExceptT TCError Identity ()
len1
                   Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
IntTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
FloatTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
FSqrtP -> do
                   ExceptT TCError Identity ()
len1
                   Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
FloatTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
FloatTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
FTanP -> do
                   ExceptT TCError Identity ()
len1
                   Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
FloatTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
FloatTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
Gensym -> ExceptT TCError Identity ()
len0 ExceptT TCError Identity ()
-> (() -> TcM (UrTy LocVar, LocationTypeState))
-> TcM (UrTy LocVar, LocationTypeState)
forall a b.
ExceptT TCError Identity a
-> (a -> ExceptT TCError Identity b) -> ExceptT TCError Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \()
_ -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
SymTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
EqSymP -> do
                   ExceptT TCError Identity ()
len2
                   Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
                   Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
BoolTy,LocationTypeState
tstate)

                 EqBenchProgP String
_ -> do
                   ExceptT TCError Identity ()
len0
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
BoolTy,LocationTypeState
tstate)

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

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

                 DictLookupP UrTy LocVar
ty -> do
                   ExceptT TCError Identity ()
len2
                   let [UrTy LocVar
d,UrTy LocVar
k]  = [UrTy LocVar]
tys
                   case UrTy LocVar
d of
                     SymDictTy Maybe LocVar
ar UrTy ()
_ty ->
                         do UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
SymTy UrTy LocVar
k
                            Exp
-> Env2 (UrTy LocVar)
-> Maybe LocVar
-> ExceptT TCError Identity ()
forall (m :: * -> *) a.
MonadError TCError m =>
Exp -> Env2 a -> Maybe LocVar -> m ()
ensureArenaScope Exp
exp Env2 (UrTy LocVar)
env Maybe LocVar
ar
                            (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty, LocationTypeState
tstate)
                     UrTy LocVar
_ -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC String
"Expected SymDictTy" Exp
exp

                 DictHasKeyP UrTy LocVar
_ty -> do
                   ExceptT TCError Identity ()
len2
                   let [UrTy LocVar
d,UrTy LocVar
k]  = [UrTy LocVar]
tys
                   case UrTy LocVar
d of
                     SymDictTy Maybe LocVar
ar UrTy ()
_ty -> do UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
SymTy UrTy LocVar
k
                                            Exp
-> Env2 (UrTy LocVar)
-> Maybe LocVar
-> ExceptT TCError Identity ()
forall (m :: * -> *) a.
MonadError TCError m =>
Exp -> Env2 a -> Maybe LocVar -> m ()
ensureArenaScope Exp
exp Env2 (UrTy LocVar)
env Maybe LocVar
ar
                                            (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
BoolTy, LocationTypeState
tstate)
                     UrTy LocVar
_ -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC String
"Expected SymDictTy" Exp
exp

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

                 Prim (UrTy LocVar)
IsBig -> do
                   ExceptT TCError Identity ()
len2
                   let [UrTy LocVar
ity, UrTy LocVar
ety] = [UrTy LocVar]
tys
                   Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
ity UrTy LocVar
forall loc. UrTy loc
IntTy
                   if UrTy LocVar -> Bool
forall a. UrTy a -> Bool
isPackedTy UrTy LocVar
ety
                   then (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
BoolTy, LocationTypeState
tstate)
                   else String -> TcM (UrTy LocVar, LocationTypeState)
forall a. HasCallStack => String -> a
error String
"L1.Typecheck: IsBig expects a Packed value."

                 ErrorP String
_str UrTy LocVar
ty -> do
                   ExceptT TCError Identity ()
len0
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty, LocationTypeState
tstate)

                 ReadPackedFile Maybe String
_fp String
_tycon Maybe LocVar
_reg UrTy LocVar
ty -> do
                   ExceptT TCError Identity ()
len0
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty, LocationTypeState
tstate)

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

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

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

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

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

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

                 VLengthP UrTy LocVar
elty -> do
                   let [UrTy LocVar
ls] = [UrTy LocVar]
tys
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp (UrTy LocVar -> UrTy LocVar
forall loc. UrTy loc -> UrTy loc
VectorTy UrTy LocVar
elty) UrTy LocVar
ls
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
IntTy, LocationTypeState
tstate)

                 VNthP UrTy LocVar
elty -> do
                   let [UrTy LocVar
ls, UrTy LocVar
i] = [UrTy LocVar]
tys
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp (UrTy LocVar -> UrTy LocVar
forall loc. UrTy loc -> UrTy loc
VectorTy UrTy LocVar
elty) UrTy LocVar
ls
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
IntTy UrTy LocVar
i
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
elty, LocationTypeState
tstate)

                 VSliceP UrTy LocVar
elty   -> do
                   let [UrTy LocVar
from,UrTy LocVar
to,UrTy LocVar
ls] = [UrTy LocVar]
tys
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
IntTy UrTy LocVar
from
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
IntTy UrTy LocVar
to
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp (UrTy LocVar -> UrTy LocVar
forall loc. UrTy loc -> UrTy loc
VectorTy UrTy LocVar
elty) UrTy LocVar
ls
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar -> UrTy LocVar
forall loc. UrTy loc -> UrTy loc
VectorTy UrTy LocVar
elty, LocationTypeState
tstate)

                 InplaceVUpdateP UrTy LocVar
elty -> do
                   let [UrTy LocVar
ls,UrTy LocVar
i,UrTy LocVar
val] = [UrTy LocVar]
tys
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp (UrTy LocVar -> UrTy LocVar
forall loc. UrTy loc -> UrTy loc
VectorTy UrTy LocVar
elty) UrTy LocVar
ls
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
forall loc. UrTy loc
IntTy UrTy LocVar
i
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
elty UrTy LocVar
val
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar -> UrTy LocVar
forall loc. UrTy loc -> UrTy loc
VectorTy UrTy LocVar
elty, LocationTypeState
tstate)

                 VConcatP UrTy LocVar
elty -> do
                   ExceptT TCError Identity ()
len1
                   let [UrTy LocVar
ls] = [UrTy LocVar]
tys
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (UrTy LocVar -> UrTy LocVar
forall loc. UrTy loc -> UrTy loc
VectorTy (UrTy LocVar -> UrTy LocVar
forall loc. UrTy loc -> UrTy loc
VectorTy UrTy LocVar
elty)) UrTy LocVar
ls
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar -> UrTy LocVar
forall loc. UrTy loc -> UrTy loc
VectorTy UrTy LocVar
elty, LocationTypeState
tstate)


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

                 InplaceVSortP UrTy LocVar
elty -> LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
tstatein (Prim (UrTy LocVar) -> [Exp] -> Exp
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE (UrTy LocVar -> Prim (UrTy LocVar)
forall ty. ty -> Prim ty
VSortP UrTy LocVar
elty) [Exp]
es)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                 Prim (UrTy LocVar)
PrintInt -> do
                   ExceptT TCError Identity ()
len1
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
IntTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [], LocationTypeState
tstate)

                 Prim (UrTy LocVar)
PrintChar -> do
                   ExceptT TCError Identity ()
len1
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
CharTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [], LocationTypeState
tstate)

                 Prim (UrTy LocVar)
PrintFloat -> do
                   ExceptT TCError Identity ()
len1
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
FloatTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [], LocationTypeState
tstate)

                 Prim (UrTy LocVar)
PrintBool -> do
                   ExceptT TCError Identity ()
len1
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
BoolTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [], LocationTypeState
tstate)

                 Prim (UrTy LocVar)
PrintSym -> do
                   ExceptT TCError Identity ()
len1
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [], LocationTypeState
tstate)

                 Prim (UrTy LocVar)
ReadInt  -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC String
"ReadInt not handled" Exp
exp

                 Prim (UrTy LocVar)
SymSetEmpty -> do
                   ExceptT TCError Identity ()
len0
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
SymSetTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
SymSetInsert -> do
                   ExceptT TCError Identity ()
len2
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
SymSetTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
SymSetTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
SymSetContains -> do
                   ExceptT TCError Identity ()
len2
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
SymSetTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
BoolTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
SymHashEmpty -> do
                   ExceptT TCError Identity ()
len0
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
SymHashTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
SymHashInsert -> do
                   ExceptT TCError Identity ()
len3
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
SymHashTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
2) UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
2)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
SymHashTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
SymHashLookup -> do
                   ExceptT TCError Identity ()
len2
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
SymHashTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
SymTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
SymHashContains -> do
                   ExceptT TCError Identity ()
len2
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
SymHashTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
BoolTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
IntHashEmpty -> do
                   ExceptT TCError Identity ()
len0
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
IntHashTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
IntHashInsert -> do
                   ExceptT TCError Identity ()
len3
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
IntHashTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
2) UrTy LocVar
forall loc. UrTy loc
IntTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
2)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
IntHashTy, LocationTypeState
tstate)

                 Prim (UrTy LocVar)
IntHashLookup -> do
                   ExceptT TCError Identity ()
len2
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0) UrTy LocVar
forall loc. UrTy loc
IntHashTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
0)
                   UrTy LocVar
_ <- Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy ([Exp]
es [Exp] -> Int -> Exp
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1) UrTy LocVar
forall loc. UrTy loc
SymTy ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. (Out a, HasCallStack) => [a] -> Int -> a
!!! Int
1)
                   (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
IntTy, LocationTypeState
tstate)

                 Write3dPpmFile{} -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC String
"Write3dPpmFile not handled yet" Exp
exp

                 RequestEndOf{} -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC  String
"tcExp of PrimAppE: RequestEndOf not handled yet" Exp
exp


      LetE (LocVar
v,[LocVar]
_ls,UrTy LocVar
ty,Exp
e1) Exp
e2 -> do

               -- We get the type and new location state from e1
               (UrTy LocVar
ty1,LocationTypeState
tstate1) <- LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
tstatein Exp
e1
               Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyNoLoc Exp
exp UrTy LocVar
ty1 UrTy LocVar
ty
               let env' :: Env2 (UrTy LocVar)
env' = LocVar -> UrTy LocVar -> Env2 (UrTy LocVar) -> Env2 (UrTy LocVar)
forall a. LocVar -> a -> Env2 a -> Env2 a
extendVEnv LocVar
v UrTy LocVar
ty Env2 (UrTy LocVar)
env

               -- Then we check e1 with that location state
               DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env' FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstate1 Exp
e2

      IfE Exp
e1 Exp
e2 Exp
e3 -> do

               -- Handle condition
               (UrTy LocVar
ty1,LocationTypeState
tstate1) <- LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
tstatein Exp
e1
               Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyModCursor Exp
exp UrTy LocVar
ty1 UrTy LocVar
forall loc. UrTy loc
BoolTy

               -- Check both branches
               (UrTy LocVar
ty2,LocationTypeState
tstate2) <- LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
tstate1 Exp
e2
               (UrTy LocVar
ty3,LocationTypeState
tstate3) <- LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
tstate1 Exp
e3

               -- Combine the type states somehow (TODO: audit this)
               LocationTypeState
tstate <- Exp
-> LocationTypeState -> LocationTypeState -> TcM LocationTypeState
combineTStates Exp
exp LocationTypeState
tstate2 LocationTypeState
tstate3

               Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyModCursor Exp
exp UrTy LocVar
ty2 UrTy LocVar
ty3
               (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty2,LocationTypeState
tstate)

      MkProdE [Exp]
es -> do
               ([UrTy LocVar]
tys,LocationTypeState
tstate) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> [Exp]
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
tcExps DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein [Exp]
es
               (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [UrTy LocVar]
tys,LocationTypeState
tstate)

      ProjE Int
i Exp
e -> do

               (UrTy LocVar
ty,LocationTypeState
tstate) <- LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
tstatein Exp
e
               UrTy LocVar
tyi <- Exp -> Int -> UrTy LocVar -> TcM (UrTy LocVar)
tcProj Exp
exp Int
i UrTy LocVar
ty
               (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
tyi, LocationTypeState
tstate)

      CaseE Exp
e [(String, [(LocVar, LocVar)], Exp)]
brs -> do

               (UrTy LocVar
ty,LocationTypeState
tstate) <- LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
tstatein Exp
e
               case UrTy LocVar
ty of
                 PackedTy String
_dc LocVar
lin -> do
                         -- We need to know the "region" of all the vars (and locations) pattern matched by this case expresssion.
                         -- The "region" is the same as that of the case scrutinee.
                         Region
reg <- Exp -> ConstraintSet -> LocVar -> TcM Region
getRegion Exp
e ConstraintSet
constrs LocVar
lin
                         DDefs (UrTy LocVar)
-> Exp
-> UrTy LocVar
-> [(String, [(LocVar, LocVar)], Exp)]
-> ExceptT TCError Identity ()
ensureMatchCases DDefs (UrTy LocVar)
ddfs Exp
exp UrTy LocVar
ty [(String, [(LocVar, LocVar)], Exp)]
brs
                         ([UrTy LocVar]
tys,LocationTypeState
tstate') <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> LocVar
-> Region
-> [(String, [(LocVar, LocVar)], Exp)]
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
tcCases DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstate LocVar
lin Region
reg [(String, [(LocVar, LocVar)], Exp)]
brs
                         (UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar))
-> UrTy LocVar -> [UrTy LocVar] -> ExceptT TCError Identity ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyModCursor Exp
exp) ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) ([UrTy LocVar] -> [UrTy LocVar]
forall a. HasCallStack => [a] -> [a]
tail [UrTy LocVar]
tys)
                         (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
0,LocationTypeState
tstate')
                 UrTy LocVar
_ -> String -> TcM (UrTy LocVar, LocationTypeState)
forall a. HasCallStack => String -> a
error (String
"Expected packed type, got " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UrTy LocVar -> String
forall a. Show a => a -> String
show UrTy LocVar
ty)

      DataConE LocVar
l String
dc [Exp]
es -> do
               let dcty :: String
dcty = DDefs (UrTy LocVar) -> ShowS
forall a. Out a => DDefs a -> ShowS
getTyOfDataCon DDefs (UrTy LocVar)
ddfs String
dc
               ([UrTy LocVar]
tys,LocationTypeState
tstate1) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> [Exp]
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
tcExps DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein [Exp]
es
               let args :: [UrTy LocVar]
args = DDefs (UrTy LocVar) -> String -> [UrTy LocVar]
forall a. Out a => DDefs a -> String -> [a]
lookupDataCon DDefs (UrTy LocVar)
ddfs String
dc

               if [UrTy LocVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [UrTy LocVar]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp]
es
               then TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC String
"Invalid argument length" Exp
exp
               else do
                 [TcM (UrTy LocVar)] -> ExceptT TCError Identity ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyNoLoc Exp
exp UrTy LocVar
ty1 UrTy LocVar
ty2
                           | (UrTy LocVar
ty1,UrTy LocVar
ty2) <- [UrTy LocVar] -> [UrTy LocVar] -> [(UrTy LocVar, UrTy LocVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip [UrTy LocVar]
args [UrTy LocVar]
tys ]
                 -- -- TODO: need to fix this check
                 Exp
-> LocVar
-> [UrTy LocVar]
-> ConstraintSet
-> ExceptT TCError Identity ()
ensureDataCon Exp
exp LocVar
l [UrTy LocVar]
tys ConstraintSet
constrs
                 LocationTypeState
tstate2 <- Exp -> LocationTypeState -> LocVar -> TcM LocationTypeState
switchOutLoc Exp
exp LocationTypeState
tstate1 LocVar
l
                 (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> LocVar -> UrTy LocVar
forall loc. String -> loc -> UrTy loc
PackedTy String
dcty LocVar
l, LocationTypeState
tstate2)

      TimeIt Exp
e UrTy LocVar
_ty Bool
_b -> do

               (UrTy LocVar
ty1,LocationTypeState
tstate1) <- LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
tstatein Exp
e
               -- ensureEqualTy exp ty ty1
               (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty1,LocationTypeState
tstate1)

      SpawnE LocVar
f [LocVar]
locs [Exp]
args ->
        DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein (LocVar -> [LocVar] -> [Exp] -> Exp
forall (ext :: * -> * -> *) loc dec.
LocVar -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE LocVar
f [LocVar]
locs [Exp]
args)

      Exp
SyncE -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [], LocationTypeState
tstatein)

      WithArenaE LocVar
v Exp
e -> do
              let env' :: Env2 (UrTy LocVar)
env' = LocVar -> UrTy LocVar -> Env2 (UrTy LocVar) -> Env2 (UrTy LocVar)
forall a. LocVar -> a -> Env2 a -> Env2 a
extendVEnv LocVar
v UrTy LocVar
forall loc. UrTy loc
ArenaTy Env2 (UrTy LocVar)
env
              DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env' FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein Exp
e

      MapE (LocVar, UrTy LocVar, Exp)
_ Exp
_ -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ Exp -> TCError
UnsupportedExpTC Exp
exp

      FoldE (LocVar, UrTy LocVar, Exp)
_ (LocVar, UrTy LocVar, Exp)
_ Exp
_ -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ Exp -> TCError
UnsupportedExpTC Exp
exp

      Ext (LetRegionE Region
r RegionSize
_ Maybe RegionType
_ Exp
e) -> do
               RegionSet
regs' <- Exp -> Region -> RegionSet -> TcM RegionSet
regionInsert Exp
exp Region
r RegionSet
regs
               (UrTy LocVar
ty,LocationTypeState
tstate) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs' LocationTypeState
tstatein Exp
e
               (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty,LocationTypeState
tstate)

      Ext (LetParRegionE Region
r RegionSize
_ Maybe RegionType
_ Exp
e) -> do
               RegionSet
regs' <- Exp -> Region -> RegionSet -> TcM RegionSet
regionInsert Exp
exp Region
r RegionSet
regs
               (UrTy LocVar
ty,LocationTypeState
tstate) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs' LocationTypeState
tstatein Exp
e
               (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty,LocationTypeState
tstate)

      Ext (LetLocE LocVar
v PreLocExp LocVar
c Exp
e) -> do
              let env' :: Env2 (UrTy LocVar)
env' = LocVar -> UrTy LocVar -> Env2 (UrTy LocVar) -> Env2 (UrTy LocVar)
forall a. LocVar -> a -> Env2 a -> Env2 a
extendVEnv LocVar
v UrTy LocVar
forall loc. UrTy loc
CursorTy Env2 (UrTy LocVar)
env
              case PreLocExp LocVar
c of
                StartOfRegionLE Region
r ->
                    do Exp -> Region -> RegionSet -> ExceptT TCError Identity ()
ensureRegion Exp
exp Region
r RegionSet
regs
                       Exp -> ConstraintSet -> Region -> ExceptT TCError Identity ()
absentStart Exp
exp ConstraintSet
constrs Region
r
                       let tstate1 :: LocationTypeState
tstate1 = LocVar
-> (Modality, Bool) -> LocationTypeState -> LocationTypeState
extendTS LocVar
v (Modality
Output,Bool
False) LocationTypeState
tstatein
                       let constrs1 :: ConstraintSet
constrs1 = LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs (LocVar -> Region -> LocConstraint
StartOfC LocVar
v Region
r) (ConstraintSet -> ConstraintSet) -> ConstraintSet -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs (LocVar -> Region -> LocConstraint
InRegionC LocVar
v Region
r) ConstraintSet
constrs
                       (UrTy LocVar
ty,LocationTypeState
tstate2) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env' FunDefs2
funs ConstraintSet
constrs1 RegionSet
regs LocationTypeState
tstate1 Exp
e
                       LocationTypeState
tstate3 <- Exp -> LocationTypeState -> LocVar -> TcM LocationTypeState
removeLoc Exp
exp LocationTypeState
tstate2 LocVar
v
                       (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty,LocationTypeState
tstate3)
                AfterConstantLE Int
i LocVar
l1 ->
                     do Region
r <- Exp -> ConstraintSet -> LocVar -> TcM Region
getRegion Exp
exp ConstraintSet
constrs LocVar
l1
                        let tstate1 :: LocationTypeState
tstate1 = LocVar
-> (Modality, Bool) -> LocationTypeState -> LocationTypeState
extendTS LocVar
v (Modality
Output,Bool
True) (LocationTypeState -> LocationTypeState)
-> LocationTypeState -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ LocVar -> LocationTypeState -> LocationTypeState
setAfter LocVar
l1 LocationTypeState
tstatein
                        let constrs1 :: ConstraintSet
constrs1 = LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs (LocVar -> Region -> LocConstraint
InRegionC LocVar
v Region
r) (ConstraintSet -> ConstraintSet) -> ConstraintSet -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs (Int -> LocVar -> LocVar -> LocConstraint
AfterConstantC Int
i LocVar
l1 LocVar
v) ConstraintSet
constrs
                        (UrTy LocVar
ty,LocationTypeState
tstate2) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env' FunDefs2
funs ConstraintSet
constrs1 RegionSet
regs LocationTypeState
tstate1 Exp
e
                        LocationTypeState
tstate3 <- Exp -> LocationTypeState -> LocVar -> TcM LocationTypeState
removeLoc Exp
exp LocationTypeState
tstate2 LocVar
v
                        (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty,LocationTypeState
tstate3)
                AfterVariableLE LocVar
x LocVar
l1 Bool
_ ->
                    do Region
r <- Exp -> ConstraintSet -> LocVar -> TcM Region
getRegion Exp
exp ConstraintSet
constrs LocVar
l1
                       (UrTy LocVar
_xty,LocationTypeState
tstate1) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein (Exp -> TcM (UrTy LocVar, LocationTypeState))
-> Exp -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ LocVar -> Exp
forall (ext :: * -> * -> *) loc dec. LocVar -> PreExp ext loc dec
VarE LocVar
x
                       -- NOTE: We now allow aliases (offsets) from scalar vars too. So we can leave out this check
                       -- ensurePackedLoc exp xty l1
                       let tstate2 :: LocationTypeState
tstate2 = LocVar
-> (Modality, Bool) -> LocationTypeState -> LocationTypeState
extendTS LocVar
v (Modality
Output,Bool
True) (LocationTypeState -> LocationTypeState)
-> LocationTypeState -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ LocVar -> LocationTypeState -> LocationTypeState
setAfter LocVar
l1 LocationTypeState
tstate1
                       let constrs1 :: ConstraintSet
constrs1 = LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs (LocVar -> Region -> LocConstraint
InRegionC LocVar
v Region
r) (ConstraintSet -> ConstraintSet) -> ConstraintSet -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs (LocVar -> LocVar -> LocVar -> LocConstraint
AfterVariableC LocVar
x LocVar
l1 LocVar
v) ConstraintSet
constrs
                       (UrTy LocVar
ty,LocationTypeState
tstate3) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env' FunDefs2
funs ConstraintSet
constrs1 RegionSet
regs LocationTypeState
tstate2 Exp
e
                       LocationTypeState
tstate4 <- Exp -> LocationTypeState -> LocVar -> TcM LocationTypeState
removeLoc Exp
exp LocationTypeState
tstate3 LocVar
v
                       (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty,LocationTypeState
tstate4)
                FromEndLE LocVar
_l1 ->
                    do -- TODO: This is the bare minimum which gets the examples typechecking again.
                       -- Need to figure out if we need to check more things here
                      (UrTy LocVar
ty,LocationTypeState
tstate1) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env' FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein Exp
e
                      (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty,LocationTypeState
tstate1)
                PreLocExp LocVar
FreeLE ->
                    do let constrs1 :: ConstraintSet
constrs1 = LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs (LocVar -> Region -> LocConstraint
InRegionC LocVar
v Region
globalReg) (ConstraintSet -> ConstraintSet) -> ConstraintSet -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ ConstraintSet
constrs
                       (UrTy LocVar
ty,LocationTypeState
tstate1) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env' FunDefs2
funs ConstraintSet
constrs1 RegionSet
regs LocationTypeState
tstatein Exp
e
                       (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty,LocationTypeState
tstate1)

                InRegionLE{} -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"InRegionLE not handled.")  Exp
exp

      Ext (StartOfPkdCursor LocVar
cur) -> do
        case LocVar -> Map LocVar (UrTy LocVar) -> Maybe (UrTy LocVar)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup LocVar
cur (Env2 (UrTy LocVar) -> Map LocVar (UrTy LocVar)
forall a. Env2 a -> TyEnv a
vEnv Env2 (UrTy LocVar)
env) of
          Just (PackedTy{}) -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
CursorTy, LocationTypeState
tstatein)
          Maybe (UrTy LocVar)
ty -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Expected PackedTy, got " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe (UrTy LocVar) -> String
forall a. Out a => a -> String
sdoc Maybe (UrTy LocVar)
ty)  Exp
exp

      Ext (TagCursor LocVar
a LocVar
_b) -> do
        case LocVar -> Map LocVar (UrTy LocVar) -> Maybe (UrTy LocVar)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup LocVar
a (Env2 (UrTy LocVar) -> Map LocVar (UrTy LocVar)
forall a. Env2 a -> TyEnv a
vEnv Env2 (UrTy LocVar)
env) of
          Just (PackedTy{}) -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UrTy LocVar
forall loc. UrTy loc
CursorTy, LocationTypeState
tstatein)
          Maybe (UrTy LocVar)
ty -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Expected PackedTy, got " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe (UrTy LocVar) -> String
forall a. Out a => a -> String
sdoc Maybe (UrTy LocVar)
ty)  Exp
exp


      Ext (FromEndE{}) -> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar, LocationTypeState))
-> TCError -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC String
"FromEndE not handled" Exp
exp
      Ext (AddFixed{}) -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
CursorTy,LocationTypeState
tstatein)

      Ext (RetE [LocVar]
_ls LocVar
v) -> do

               -- skip returned locations for now
               LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
tstatein (Exp -> TcM (UrTy LocVar, LocationTypeState))
-> Exp -> TcM (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ LocVar -> Exp
forall (ext :: * -> * -> *) loc dec. LocVar -> PreExp ext loc dec
VarE LocVar
v

      -- The IntTy is just a placeholder. BoundsCheck is a side-effect
      Ext (BoundsCheck{}) -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
IntTy,LocationTypeState
tstatein)

      Ext (IndirectionE String
tycon String
_ (LocVar
a,LocVar
_) (LocVar, LocVar)
_ Exp
_) -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> LocVar -> UrTy LocVar
forall loc. String -> loc -> UrTy loc
PackedTy String
tycon LocVar
a, LocationTypeState
tstatein)

      Ext E2Ext LocVar (UrTy LocVar)
GetCilkWorkerNum -> (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
forall loc. UrTy loc
IntTy, LocationTypeState
tstatein)

      Ext (LetAvail [LocVar]
_ Exp
e) -> LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
tstatein Exp
e

      Ext (AllocateTagHere{}) -> do
        -- (ty,tstate1) <- recur tstatein (VarE v)
        -- ensureEqualTy (VarE v) ty CursorTy
        (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [], LocationTypeState
tstatein)

      Ext (AllocateScalarsHere{}) -> do
        -- (ty,tstate1) <- recur tstatein (VarE v)
        -- ensureEqualTy (VarE v) ty CursorTy
        (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [], LocationTypeState
tstatein)

      Ext (SSPush{}) -> do
        -- (ty,tstate1) <- recur tstatein (VarE v)
        -- ensureEqualTy (VarE v) ty CursorTy
        (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [], LocationTypeState
tstatein)

      Ext (SSPop{}) -> do
        -- (ty,tstate1) <- recur tstatein (VarE v)
        -- ensureEqualTy (VarE v) ty CursorTy
        (UrTy LocVar, LocationTypeState)
-> TcM (UrTy LocVar, LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UrTy LocVar] -> UrTy LocVar
forall loc. [UrTy loc] -> UrTy loc
ProdTy [], LocationTypeState
tstatein)

    where recur :: LocationTypeState -> Exp -> TcM (UrTy LocVar, LocationTypeState)
recur LocationTypeState
ts Exp
e = DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
ts Exp
e
          checkListElemTy :: UrTy LocVar -> ExceptT TCError Identity ()
checkListElemTy UrTy LocVar
el_ty =
            if UrTy LocVar -> Bool
forall a. UrTy a -> Bool
isValidListElemTy UrTy LocVar
el_ty
            then () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            else TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Gibbon-TODO: Lists of only scalars or flat products of scalars are allowed. Got" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UrTy LocVar -> String
forall a. Out a => a -> String
sdoc UrTy LocVar
el_ty) Exp
exp



-- | Helper function to check case branches.
tcCases :: DDefs Ty2 -> Env2 Ty2 -> FunDefs2
        -> ConstraintSet -> RegionSet -> LocationTypeState -> LocVar
        -> Region -> [(DataCon, [(Var,LocVar)], Exp)]
        -> TcM ([Ty2], LocationTypeState)
tcCases :: DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> LocVar
-> Region
-> [(String, [(LocVar, LocVar)], Exp)]
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
tcCases DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein LocVar
lin Region
reg ((String
dc, [(LocVar, LocVar)]
vs, Exp
e):[(String, [(LocVar, LocVar)], Exp)]
cases) = do

  let argtys :: [((LocVar, LocVar), UrTy LocVar)]
argtys = [(LocVar, LocVar)]
-> [UrTy LocVar] -> [((LocVar, LocVar), UrTy LocVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(LocVar, LocVar)]
vs ([UrTy LocVar] -> [((LocVar, LocVar), UrTy LocVar)])
-> [UrTy LocVar] -> [((LocVar, LocVar), UrTy LocVar)]
forall a b. (a -> b) -> a -> b
$ DDefs (UrTy LocVar) -> String -> [UrTy LocVar]
forall a. Out a => DDefs a -> String -> [a]
lookupDataCon DDefs (UrTy LocVar)
ddfs String
dc
      pairwise :: [(((LocVar, LocVar), UrTy LocVar),
  Maybe ((LocVar, LocVar), UrTy LocVar))]
pairwise = [((LocVar, LocVar), UrTy LocVar)]
-> [Maybe ((LocVar, LocVar), UrTy LocVar)]
-> [(((LocVar, LocVar), UrTy LocVar),
     Maybe ((LocVar, LocVar), UrTy LocVar))]
forall a b. [a] -> [b] -> [(a, b)]
zip [((LocVar, LocVar), UrTy LocVar)]
argtys ([Maybe ((LocVar, LocVar), UrTy LocVar)]
 -> [(((LocVar, LocVar), UrTy LocVar),
      Maybe ((LocVar, LocVar), UrTy LocVar))])
-> [Maybe ((LocVar, LocVar), UrTy LocVar)]
-> [(((LocVar, LocVar), UrTy LocVar),
     Maybe ((LocVar, LocVar), UrTy LocVar))]
forall a b. (a -> b) -> a -> b
$ Maybe ((LocVar, LocVar), UrTy LocVar)
forall a. Maybe a
Nothing Maybe ((LocVar, LocVar), UrTy LocVar)
-> [Maybe ((LocVar, LocVar), UrTy LocVar)]
-> [Maybe ((LocVar, LocVar), UrTy LocVar)]
forall a. a -> [a] -> [a]
: ((((LocVar, LocVar), UrTy LocVar)
 -> Maybe ((LocVar, LocVar), UrTy LocVar))
-> [((LocVar, LocVar), UrTy LocVar)]
-> [Maybe ((LocVar, LocVar), UrTy LocVar)]
forall a b. (a -> b) -> [a] -> [b]
L.map ((LocVar, LocVar), UrTy LocVar)
-> Maybe ((LocVar, LocVar), UrTy LocVar)
forall a. a -> Maybe a
Just [((LocVar, LocVar), UrTy LocVar)]
argtys)

      -- Generate the new constraints to check this branch
      genConstrs :: (((LocVar, LocVar), UrTy LocVar),
 Maybe ((LocVar, LocVar), UrTy LocVar))
-> (LocVar, [LocConstraint]) -> (LocVar, [LocConstraint])
genConstrs (((LocVar
_v1,LocVar
l1),PackedTy String
_ LocVar
_),Maybe ((LocVar, LocVar), UrTy LocVar)
Nothing) (LocVar
lin,[LocConstraint]
lst) =
          (LocVar
l1,[Int -> LocVar -> LocVar -> LocConstraint
AfterConstantC Int
1 LocVar
lin LocVar
l1, LocVar -> Region -> LocConstraint
InRegionC LocVar
l1 Region
reg] [LocConstraint] -> [LocConstraint] -> [LocConstraint]
forall a. [a] -> [a] -> [a]
++ [LocConstraint]
lst)
      genConstrs (((LocVar
_v1,LocVar
l1),PackedTy String
_ LocVar
_),Just ((LocVar
v2,LocVar
l2),PackedTy String
_ LocVar
_)) (LocVar
_lin,[LocConstraint]
lst) =
          (LocVar
l1,[LocVar -> LocVar -> LocVar -> LocConstraint
AfterVariableC LocVar
v2 LocVar
l2 LocVar
l1, LocVar -> Region -> LocConstraint
InRegionC LocVar
l1 Region
reg] [LocConstraint] -> [LocConstraint] -> [LocConstraint]
forall a. [a] -> [a] -> [a]
++ [LocConstraint]
lst)
      genConstrs (((LocVar
_v1,LocVar
l1),PackedTy String
_ LocVar
_),Just ((LocVar
_v2,LocVar
_l2),UrTy LocVar
IntTy)) (LocVar
lin,[LocConstraint]
lst) =
        let sz :: Int
sz = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
1 (UrTy Any -> Maybe Int
forall a. UrTy a -> Maybe Int
sizeOfTy UrTy Any
forall loc. UrTy loc
IntTy)
        in (LocVar
l1, [Int -> LocVar -> LocVar -> LocConstraint
AfterConstantC Int
sz LocVar
lin LocVar
l1, LocVar -> Region -> LocConstraint
InRegionC LocVar
l1 Region
reg] [LocConstraint] -> [LocConstraint] -> [LocConstraint]
forall a. [a] -> [a] -> [a]
++ [LocConstraint]
lst)
      genConstrs (((LocVar
_,LocVar
l1),UrTy LocVar
_),Maybe ((LocVar, LocVar), UrTy LocVar)
_) (LocVar
lin,[LocConstraint]
lst) =
        (LocVar
lin, (LocVar -> Region -> LocConstraint
InRegionC LocVar
l1 Region
reg LocConstraint -> [LocConstraint] -> [LocConstraint]
forall a. a -> [a] -> [a]
: [LocConstraint]
lst))

      -- Generate the new location state map to check this branch
      genTS :: ((a, LocVar), UrTy loc) -> LocationTypeState -> LocationTypeState
genTS ((a
_v,LocVar
l),PackedTy String
_ loc
_) LocationTypeState
ts = LocVar
-> (Modality, Bool) -> LocationTypeState -> LocationTypeState
extendTS LocVar
l (Modality
Input,Bool
False) LocationTypeState
ts
      genTS ((a, LocVar), UrTy loc)
_ LocationTypeState
ts = LocationTypeState
ts
      genEnv :: ((LocVar, loc), UrTy loc) -> Env2 (UrTy loc) -> Env2 (UrTy loc)
genEnv ((LocVar
v,loc
l),PackedTy String
dc loc
_l') Env2 (UrTy loc)
env = LocVar -> UrTy loc -> Env2 (UrTy loc) -> Env2 (UrTy loc)
forall a. LocVar -> a -> Env2 a -> Env2 a
extendVEnv LocVar
v (String -> loc -> UrTy loc
forall loc. String -> loc -> UrTy loc
PackedTy String
dc loc
l) Env2 (UrTy loc)
env
      genEnv ((LocVar
v,loc
_l),UrTy loc
ty) Env2 (UrTy loc)
env = LocVar -> UrTy loc -> Env2 (UrTy loc) -> Env2 (UrTy loc)
forall a. LocVar -> a -> Env2 a -> Env2 a
extendVEnv LocVar
v UrTy loc
ty Env2 (UrTy loc)
env

      -- Remove the pattern-bound location variables from the location state map
      remTS :: ((a, LocVar), UrTy loc) -> LocationTypeState -> LocationTypeState
remTS ((a
_v,LocVar
l),PackedTy String
_ loc
_) LocationTypeState
ts = LocVar -> LocationTypeState -> LocationTypeState
removeTS LocVar
l LocationTypeState
ts
      remTS ((a, LocVar), UrTy loc)
_ LocationTypeState
ts = LocationTypeState
ts

      -- Use these functions with our old friend foldr
      constrs1 :: ConstraintSet
constrs1 = (LocConstraint -> ConstraintSet -> ConstraintSet)
-> ConstraintSet -> [LocConstraint] -> ConstraintSet
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs ConstraintSet
constrs ([LocConstraint] -> ConstraintSet)
-> [LocConstraint] -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ (LocVar, [LocConstraint]) -> [LocConstraint]
forall a b. (a, b) -> b
snd ((LocVar, [LocConstraint]) -> [LocConstraint])
-> (LocVar, [LocConstraint]) -> [LocConstraint]
forall a b. (a -> b) -> a -> b
$ ((((LocVar, LocVar), UrTy LocVar),
  Maybe ((LocVar, LocVar), UrTy LocVar))
 -> (LocVar, [LocConstraint]) -> (LocVar, [LocConstraint]))
-> (LocVar, [LocConstraint])
-> [(((LocVar, LocVar), UrTy LocVar),
     Maybe ((LocVar, LocVar), UrTy LocVar))]
-> (LocVar, [LocConstraint])
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr (((LocVar, LocVar), UrTy LocVar),
 Maybe ((LocVar, LocVar), UrTy LocVar))
-> (LocVar, [LocConstraint]) -> (LocVar, [LocConstraint])
genConstrs (LocVar
lin,[]) [(((LocVar, LocVar), UrTy LocVar),
  Maybe ((LocVar, LocVar), UrTy LocVar))]
pairwise
      tstate1 :: LocationTypeState
tstate1 = (((LocVar, LocVar), UrTy LocVar)
 -> LocationTypeState -> LocationTypeState)
-> LocationTypeState
-> [((LocVar, LocVar), UrTy LocVar)]
-> LocationTypeState
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr ((LocVar, LocVar), UrTy LocVar)
-> LocationTypeState -> LocationTypeState
forall {a} {loc}.
((a, LocVar), UrTy loc) -> LocationTypeState -> LocationTypeState
genTS LocationTypeState
tstatein [((LocVar, LocVar), UrTy LocVar)]
argtys
      env1 :: Env2 (UrTy LocVar)
env1 = (((LocVar, LocVar), UrTy LocVar)
 -> Env2 (UrTy LocVar) -> Env2 (UrTy LocVar))
-> Env2 (UrTy LocVar)
-> [((LocVar, LocVar), UrTy LocVar)]
-> Env2 (UrTy LocVar)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr ((LocVar, LocVar), UrTy LocVar)
-> Env2 (UrTy LocVar) -> Env2 (UrTy LocVar)
forall {loc}.
((LocVar, loc), UrTy loc) -> Env2 (UrTy loc) -> Env2 (UrTy loc)
genEnv Env2 (UrTy LocVar)
env [((LocVar, LocVar), UrTy LocVar)]
argtys

  (UrTy LocVar
ty1,LocationTypeState
tstate2) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env1 FunDefs2
funs ConstraintSet
constrs1 RegionSet
regs LocationTypeState
tstate1 Exp
e
  ([UrTy LocVar]
tyRest,LocationTypeState
tstateRest) <- ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
recur
  LocationTypeState
tstateCombine <- Exp
-> LocationTypeState -> LocationTypeState -> TcM LocationTypeState
combineTStates Exp
e LocationTypeState
tstate2 LocationTypeState
tstateRest
  let tstatee' :: LocationTypeState
tstatee' = (((LocVar, LocVar), UrTy LocVar)
 -> LocationTypeState -> LocationTypeState)
-> LocationTypeState
-> [((LocVar, LocVar), UrTy LocVar)]
-> LocationTypeState
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr ((LocVar, LocVar), UrTy LocVar)
-> LocationTypeState -> LocationTypeState
forall {a} {loc}.
((a, LocVar), UrTy loc) -> LocationTypeState -> LocationTypeState
remTS LocationTypeState
tstateCombine [((LocVar, LocVar), UrTy LocVar)]
argtys
  ([UrTy LocVar], LocationTypeState)
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
ty1UrTy LocVar -> [UrTy LocVar] -> [UrTy LocVar]
forall a. a -> [a] -> [a]
:[UrTy LocVar]
tyRest,LocationTypeState
tstatee')

    where recur :: ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
recur = do
            ([UrTy LocVar]
tys,LocationTypeState
tstate2) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> LocVar
-> Region
-> [(String, [(LocVar, LocVar)], Exp)]
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
tcCases DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein LocVar
lin Region
reg [(String, [(LocVar, LocVar)], Exp)]
cases
            ([UrTy LocVar], LocationTypeState)
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([UrTy LocVar]
tys,LocationTypeState
tstate2)

tcCases DDefs (UrTy LocVar)
_ Env2 (UrTy LocVar)
_ FunDefs2
_ ConstraintSet
_ RegionSet
_ LocationTypeState
ts LocVar
_ Region
_ [] = ([UrTy LocVar], LocationTypeState)
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([],LocationTypeState
ts)

tcProj :: Exp -> Int -> Ty2 -> TcM Ty2
tcProj :: Exp -> Int -> UrTy LocVar -> TcM (UrTy LocVar)
tcProj Exp
_ Int
i (ProdTy [UrTy LocVar]
tys) = UrTy LocVar -> TcM (UrTy LocVar)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar -> TcM (UrTy LocVar))
-> UrTy LocVar -> TcM (UrTy LocVar)
forall a b. (a -> b) -> a -> b
$ [UrTy LocVar]
tys [UrTy LocVar] -> Int -> UrTy LocVar
forall a. HasCallStack => [a] -> Int -> a
!! Int
i
tcProj Exp
e Int
_i UrTy LocVar
ty = TCError -> TcM (UrTy LocVar)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar)) -> TCError -> TcM (UrTy LocVar)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Projection from non-tuple type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (UrTy LocVar -> String
forall a. Show a => a -> String
show UrTy LocVar
ty)) Exp
e

-- | A wrapper for tcExp to check a list of exprs, checking them in order:
-- the order matters because the location state map is threaded through,
-- so this is assuming the list of expressions would have been evaluated
-- in first-to-last order.
tcExps :: DDefs Ty2 -> Env2 Ty2 -> FunDefs2
      -> ConstraintSet -> RegionSet -> LocationTypeState -> [Exp]
      -> TcM ([Ty2], LocationTypeState)
tcExps :: DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> [Exp]
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
tcExps DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein (Exp
exp:[Exp]
exps) =
    do (UrTy LocVar
ty,LocationTypeState
ts) <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstatein Exp
exp
       ([UrTy LocVar]
tys,LocationTypeState
ts') <- DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> [Exp]
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
tcExps DDefs (UrTy LocVar)
ddfs Env2 (UrTy LocVar)
env FunDefs2
funs ConstraintSet
constrs RegionSet
regs LocationTypeState
ts [Exp]
exps
       ([UrTy LocVar], LocationTypeState)
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UrTy LocVar
tyUrTy LocVar -> [UrTy LocVar] -> [UrTy LocVar]
forall a. a -> [a] -> [a]
:[UrTy LocVar]
tys,LocationTypeState
ts')
tcExps DDefs (UrTy LocVar)
_ Env2 (UrTy LocVar)
_ FunDefs2
_ ConstraintSet
_ RegionSet
_ LocationTypeState
ts [] = ([UrTy LocVar], LocationTypeState)
-> ExceptT TCError Identity ([UrTy LocVar], LocationTypeState)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([],LocationTypeState
ts)



-- | Main entry point, checks a whole program (functions and main body).
tcProg :: Prog2 -> PassM Prog2
tcProg :: Prog2 -> PassM Prog2
tcProg prg0 :: Prog2
prg0@Prog{DDefs (TyOf Exp)
ddefs :: DDefs (TyOf Exp)
ddefs :: forall ex. Prog ex -> DDefs (TyOf ex)
ddefs,FunDefs2
fundefs :: FunDefs2
fundefs :: forall ex. Prog ex -> FunDefs ex
fundefs,Maybe (Exp, TyOf Exp)
mainExp :: Maybe (Exp, TyOf Exp)
mainExp :: forall ex. Prog ex -> Maybe (ex, TyOf ex)
mainExp} = do

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

  -- Handle main function
  case Maybe (Exp, TyOf Exp)
mainExp of
    Maybe (Exp, TyOf Exp)
Nothing -> () -> PassM ()
forall a. a -> PassM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just (Exp
e,TyOf Exp
t) ->
        let init_env :: Env2 (TyOf Exp)
init_env = Prog2 -> Env2 (TyOf Exp)
forall a. Prog a -> Env2 (TyOf a)
progToEnv Prog2
prg0
            res :: Either TCError (UrTy LocVar, LocationTypeState)
res = TcM (UrTy LocVar, LocationTypeState)
-> Either TCError (UrTy LocVar, LocationTypeState)
forall e a. Except e a -> Either e a
runExcept (TcM (UrTy LocVar, LocationTypeState)
 -> Either TCError (UrTy LocVar, LocationTypeState))
-> TcM (UrTy LocVar, LocationTypeState)
-> Either TCError (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (TyOf Exp)
DDefs (UrTy LocVar)
ddefs Env2 (TyOf Exp)
Env2 (UrTy LocVar)
init_env FunDefs2
fundefs
                    (Set LocConstraint -> ConstraintSet
ConstraintSet (Set LocConstraint -> ConstraintSet)
-> Set LocConstraint -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ Set LocConstraint
forall a. Set a
S.empty) (Set LocVar -> RegionSet
RegionSet (Set LocVar -> RegionSet) -> Set LocVar -> RegionSet
forall a b. (a -> b) -> a -> b
$ Set LocVar
forall a. Set a
S.empty)
                    (Map LocVar (Modality, Bool) -> LocationTypeState
LocationTypeState (Map LocVar (Modality, Bool) -> LocationTypeState)
-> Map LocVar (Modality, Bool) -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ Map LocVar (Modality, Bool)
forall k a. Map k a
M.empty) Exp
e
        in case Either TCError (UrTy LocVar, LocationTypeState)
res of
             Left TCError
err -> String -> PassM ()
forall a. HasCallStack => String -> a
error (String -> PassM ()) -> String -> PassM ()
forall a b. (a -> b) -> a -> b
$ TCError -> String
forall a. Show a => a -> String
show TCError
err
             Right (UrTy LocVar
t',LocationTypeState
_ts) ->
                 if UrTy LocVar
t' UrTy LocVar -> UrTy LocVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyOf Exp
UrTy LocVar
t then () -> PassM ()
forall a. a -> PassM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 else String -> PassM ()
forall a. HasCallStack => String -> a
error (String -> PassM ()) -> String -> PassM ()
forall a b. (a -> b) -> a -> b
$ String
"Expected type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (UrTy LocVar -> String
forall a. Show a => a -> String
show TyOf Exp
UrTy LocVar
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and got type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (UrTy LocVar -> String
forall a. Show a => a -> String
show UrTy LocVar
t')

  Prog2 -> PassM Prog2
forall a. a -> PassM a
forall (m :: * -> *) a. Monad m => a -> m a
return Prog2
prg0 -- Identity function for now.

  where

    fd :: FunDef2 -> PassM ()
    fd :: FunDef Exp -> PassM ()
fd func :: FunDef Exp
func@FunDef{ArrowTy (TyOf Exp)
funTy :: forall ex. FunDef ex -> ArrowTy (TyOf ex)
funTy :: ArrowTy (TyOf Exp)
funTy,[LocVar]
funArgs :: [LocVar]
funArgs :: forall ex. FunDef ex -> [LocVar]
funArgs,Exp
funBody :: Exp
funBody :: forall ex. FunDef ex -> ex
funBody} = do
        let init_env :: Env2 (TyOf Exp)
init_env = Prog2 -> Env2 (TyOf Exp)
forall a. Prog a -> Env2 (TyOf a)
progToEnv Prog2
prg0
            env :: Env2 (UrTy LocVar)
env = Map LocVar (UrTy LocVar)
-> Env2 (UrTy LocVar) -> Env2 (UrTy LocVar)
forall a. Map LocVar a -> Env2 a -> Env2 a
extendsVEnv ([(LocVar, UrTy LocVar)] -> Map LocVar (UrTy LocVar)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(LocVar, UrTy LocVar)] -> Map LocVar (UrTy LocVar))
-> [(LocVar, UrTy LocVar)] -> Map LocVar (UrTy LocVar)
forall a b. (a -> b) -> a -> b
$ [LocVar] -> [UrTy LocVar] -> [(LocVar, UrTy LocVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip [LocVar]
funArgs (ArrowTy2 (UrTy LocVar) -> [UrTy LocVar]
forall ty2. ArrowTy2 ty2 -> [ty2]
arrIns ArrowTy (TyOf Exp)
ArrowTy2 (UrTy LocVar)
funTy)) Env2 (TyOf Exp)
Env2 (UrTy LocVar)
init_env
            constrs :: ConstraintSet
constrs = [LRM] -> ConstraintSet
funConstrs (ArrowTy2 (UrTy LocVar) -> [LRM]
forall ty2. ArrowTy2 ty2 -> [LRM]
locVars ArrowTy (TyOf Exp)
ArrowTy2 (UrTy LocVar)
funTy)
            regs :: RegionSet
regs = [LRM] -> RegionSet
funRegs (ArrowTy2 (UrTy LocVar) -> [LRM]
forall ty2. ArrowTy2 ty2 -> [LRM]
locVars ArrowTy (TyOf Exp)
ArrowTy2 (UrTy LocVar)
funTy)
            tstate :: LocationTypeState
tstate = [LRM] -> LocationTypeState
funTState (ArrowTy2 (UrTy LocVar) -> [LRM]
forall ty2. ArrowTy2 ty2 -> [LRM]
locVars ArrowTy (TyOf Exp)
ArrowTy2 (UrTy LocVar)
funTy)
            res :: Either TCError (UrTy LocVar, LocationTypeState)
res = TcM (UrTy LocVar, LocationTypeState)
-> Either TCError (UrTy LocVar, LocationTypeState)
forall e a. Except e a -> Either e a
runExcept (TcM (UrTy LocVar, LocationTypeState)
 -> Either TCError (UrTy LocVar, LocationTypeState))
-> TcM (UrTy LocVar, LocationTypeState)
-> Either TCError (UrTy LocVar, LocationTypeState)
forall a b. (a -> b) -> a -> b
$ DDefs (UrTy LocVar)
-> Env2 (UrTy LocVar)
-> FunDefs2
-> ConstraintSet
-> RegionSet
-> LocationTypeState
-> Exp
-> TcM (UrTy LocVar, LocationTypeState)
tcExp DDefs (TyOf Exp)
DDefs (UrTy LocVar)
ddefs Env2 (UrTy LocVar)
env FunDefs2
fundefs ConstraintSet
constrs RegionSet
regs LocationTypeState
tstate Exp
funBody
        case Either TCError (UrTy LocVar, LocationTypeState)
res of
          Left TCError
err -> String -> PassM ()
forall a. HasCallStack => String -> a
error (String -> PassM ()) -> String -> PassM ()
forall a b. (a -> b) -> a -> b
$ TCError -> String
forall a. Show a => a -> String
show TCError
err
          Right (UrTy LocVar
ty,LocationTypeState
_) -> if UrTy LocVar
ty UrTy LocVar -> UrTy LocVar -> Bool
forall a. Eq a => a -> a -> Bool
== (ArrowTy2 (UrTy LocVar) -> UrTy LocVar
forall ty2. ArrowTy2 ty2 -> ty2
arrOut ArrowTy (TyOf Exp)
ArrowTy2 (UrTy LocVar)
funTy)
                          then () -> PassM ()
forall a. a -> PassM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                          else String -> PassM ()
forall a. HasCallStack => String -> a
error (String -> PassM ()) -> String -> PassM ()
forall a b. (a -> b) -> a -> b
$ String
"Expected type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (UrTy LocVar -> String
forall a. Out a => a -> String
sdoc (ArrowTy2 (UrTy LocVar) -> UrTy LocVar
forall ty2. ArrowTy2 ty2 -> ty2
arrOut ArrowTy (TyOf Exp)
ArrowTy2 (UrTy LocVar)
funTy))
                                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and got type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (UrTy LocVar -> String
forall a. Out a => a -> String
sdoc UrTy LocVar
ty)
                                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (FunDef Exp -> String
forall a. Out a => a -> String
sdoc FunDef Exp
func)



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

-- Helper functions


-- | Insert a region into a region set.
-- Includes an expression for error reporting.
regionInsert :: Exp -> Region -> RegionSet -> TcM RegionSet
regionInsert :: Exp -> Region -> RegionSet -> TcM RegionSet
regionInsert Exp
e Region
r (RegionSet Set LocVar
regSet) = do
  if (LocVar -> Set LocVar -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member (Region -> LocVar
regionToVar Region
r) Set LocVar
regSet)
  then TCError -> TcM RegionSet
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM RegionSet) -> TCError -> TcM RegionSet
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC String
"Shadowed regions not allowed" Exp
e
  else RegionSet -> TcM RegionSet
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RegionSet -> TcM RegionSet) -> RegionSet -> TcM RegionSet
forall a b. (a -> b) -> a -> b
$ Set LocVar -> RegionSet
RegionSet (LocVar -> Set LocVar -> Set LocVar
forall a. Ord a => a -> Set a -> Set a
S.insert (Region -> LocVar
regionToVar Region
r) Set LocVar
regSet)

-- | Ask if a region is in the region set.
hasRegion :: Region -> RegionSet -> Bool
hasRegion :: Region -> RegionSet -> Bool
hasRegion Region
r (RegionSet Set LocVar
regSet) = LocVar -> Set LocVar -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member (Region -> LocVar
regionToVar Region
r) Set LocVar
regSet

-- | Ensure that a region is in a region set, reporting an error otherwise.
-- Includes an expression for error reporting.
ensureRegion :: Exp -> Region -> RegionSet -> TcM ()
ensureRegion :: Exp -> Region -> RegionSet -> ExceptT TCError Identity ()
ensureRegion Exp
exp Region
r (RegionSet Set LocVar
regSet) =
    if LocVar -> Set LocVar -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member (Region -> LocVar
regionToVar Region
r) Set LocVar
regSet then () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    else TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Region " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Region -> String
forall a. Show a => a -> String
show Region
r) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in scope") Exp
exp

-- | Get the region of a location variable.
-- Includes an expression for error reporting.
getRegion :: Exp -> ConstraintSet -> LocVar -> TcM Region
getRegion :: Exp -> ConstraintSet -> LocVar -> TcM Region
getRegion Exp
exp (ConstraintSet Set LocConstraint
cs) LocVar
l = [LocConstraint] -> TcM Region
go ([LocConstraint] -> TcM Region) -> [LocConstraint] -> TcM Region
forall a b. (a -> b) -> a -> b
$ Set LocConstraint -> [LocConstraint]
forall a. Set a -> [a]
S.toList Set LocConstraint
cs
    where go :: [LocConstraint] -> TcM Region
go ((InRegionC LocVar
l1 Region
r):[LocConstraint]
cs) = if LocVar
l1 LocVar -> LocVar -> Bool
forall a. Eq a => a -> a -> Bool
== LocVar
l then Region -> TcM Region
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Region
r
                                     else [LocConstraint] -> TcM Region
go [LocConstraint]
cs
          go (LocConstraint
_:[LocConstraint]
cs) = [LocConstraint] -> TcM Region
go [LocConstraint]
cs
          go [] = TCError -> TcM Region
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM Region) -> TCError -> TcM Region
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Location " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocVar -> String
forall a. Show a => a -> String
show LocVar
l) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" has no region") Exp
exp

-- | Get the regions mentioned in the location bindings in a function type.
funRegs :: [LRM] -> RegionSet
funRegs :: [LRM] -> RegionSet
funRegs ((LRM LocVar
_l Region
r Modality
_m):[LRM]
lrms) =
    let (RegionSet Set LocVar
rs) = [LRM] -> RegionSet
funRegs [LRM]
lrms
    in Set LocVar -> RegionSet
RegionSet (Set LocVar -> RegionSet) -> Set LocVar -> RegionSet
forall a b. (a -> b) -> a -> b
$ LocVar -> Set LocVar -> Set LocVar
forall a. Ord a => a -> Set a -> Set a
S.insert (Region -> LocVar
regionToVar Region
r) Set LocVar
rs
funRegs [] = Set LocVar -> RegionSet
RegionSet (Set LocVar -> RegionSet) -> Set LocVar -> RegionSet
forall a b. (a -> b) -> a -> b
$ Set LocVar
forall a. Set a
S.empty

globalReg :: Region
globalReg :: Region
globalReg = LocVar -> Multiplicity -> Region
GlobR LocVar
"GLOBAL" Multiplicity
BigInfinite

-- | Get the constraints from the location bindings in a function type.
funConstrs :: [LRM] -> ConstraintSet
funConstrs :: [LRM] -> ConstraintSet
funConstrs ((LRM LocVar
l Region
r Modality
_m):[LRM]
lrms) =
    LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs (LocVar -> Region -> LocConstraint
InRegionC LocVar
l Region
r) (ConstraintSet -> ConstraintSet) -> ConstraintSet -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ [LRM] -> ConstraintSet
funConstrs [LRM]
lrms
funConstrs [] = Set LocConstraint -> ConstraintSet
ConstraintSet (Set LocConstraint -> ConstraintSet)
-> Set LocConstraint -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ Set LocConstraint
forall a. Set a
S.empty

-- | Get the type state implied by the location bindings in a function type.
funTState :: [LRM] -> LocationTypeState
funTState :: [LRM] -> LocationTypeState
funTState ((LRM LocVar
l Region
_r Modality
m):[LRM]
lrms) =
    LocVar
-> (Modality, Bool) -> LocationTypeState -> LocationTypeState
extendTS LocVar
l (Modality
m,Bool
False) (LocationTypeState -> LocationTypeState)
-> LocationTypeState -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ [LRM] -> LocationTypeState
funTState [LRM]
lrms
funTState [] = Map LocVar (Modality, Bool) -> LocationTypeState
LocationTypeState (Map LocVar (Modality, Bool) -> LocationTypeState)
-> Map LocVar (Modality, Bool) -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ Map LocVar (Modality, Bool)
forall k a. Map k a
M.empty

-- | Look up the type of a variable from the environment
-- Includes an expression for error reporting.
lookupVar :: Env2 Ty2 -> Var -> Exp -> TcM Ty2
lookupVar :: Env2 (UrTy LocVar) -> LocVar -> Exp -> TcM (UrTy LocVar)
lookupVar Env2 (UrTy LocVar)
env LocVar
var Exp
exp =
    case LocVar -> Map LocVar (UrTy LocVar) -> Maybe (UrTy LocVar)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup LocVar
var (Map LocVar (UrTy LocVar) -> Maybe (UrTy LocVar))
-> Map LocVar (UrTy LocVar) -> Maybe (UrTy LocVar)
forall a b. (a -> b) -> a -> b
$ Env2 (UrTy LocVar) -> Map LocVar (UrTy LocVar)
forall a. Env2 a -> TyEnv a
vEnv Env2 (UrTy LocVar)
env of
      Maybe (UrTy LocVar)
Nothing -> TCError -> TcM (UrTy LocVar)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (UrTy LocVar)) -> TCError -> TcM (UrTy LocVar)
forall a b. (a -> b) -> a -> b
$ LocVar -> Exp -> TCError
VarNotFoundTC LocVar
var Exp
exp
      Just UrTy LocVar
ty -> UrTy LocVar -> TcM (UrTy LocVar)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return UrTy LocVar
ty

-- | Combine two location state maps.
-- Currently just uses a naive union, which will not verify that different branches do the same
-- things.
-- TODO: Fix this!
combineTStates :: Exp -> LocationTypeState -> LocationTypeState -> TcM LocationTypeState
combineTStates :: Exp
-> LocationTypeState -> LocationTypeState -> TcM LocationTypeState
combineTStates Exp
_exp (LocationTypeState Map LocVar (Modality, Bool)
ts1) (LocationTypeState Map LocVar (Modality, Bool)
ts2) =
    LocationTypeState -> TcM LocationTypeState
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LocationTypeState -> TcM LocationTypeState)
-> LocationTypeState -> TcM LocationTypeState
forall a b. (a -> b) -> a -> b
$ Map LocVar (Modality, Bool) -> LocationTypeState
LocationTypeState (Map LocVar (Modality, Bool) -> LocationTypeState)
-> Map LocVar (Modality, Bool) -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ Map LocVar (Modality, Bool)
-> Map LocVar (Modality, Bool) -> Map LocVar (Modality, Bool)
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map LocVar (Modality, Bool)
ts1 Map LocVar (Modality, Bool)
ts2
    -- throwError $ DivergingEffectsTC exp ts1 ts2

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

-- | Ensure that the number of arguments to an operation is correct.
checkLen :: (Show op, Show arg) => Exp -> op -> Int -> [arg] -> TcM ()
checkLen :: forall op arg.
(Show op, Show arg) =>
Exp -> op -> Int -> [arg] -> ExceptT TCError Identity ()
checkLen Exp
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 Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  else TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Wrong number of arguments to "String -> ShowS
forall a. [a] -> [a] -> [a]
++op -> String
forall a. Show a => a -> String
show op
prString -> ShowS
forall a. [a] -> [a] -> [a]
++
                               String
".\nExpected "String -> ShowS
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
nString -> ShowS
forall a. [a] -> [a] -> [a]
++String
", received "
                                String -> ShowS
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show ([arg] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [arg]
ls)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
":\n  "String -> ShowS
forall a. [a] -> [a] -> [a]
++[arg] -> String
forall a. Show a => a -> String
show [arg]
ls) Exp
expr

-- | Ensure that two types are equal.
-- Includes an expression for error reporting.
ensureEqualTy :: Exp -> Ty2 -> Ty2 -> TcM Ty2
ensureEqualTy :: Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
_ UrTy LocVar
CursorTy UrTy LocVar
IntTy = UrTy LocVar -> TcM (UrTy LocVar)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return UrTy LocVar
forall loc. UrTy loc
CursorTy
ensureEqualTy Exp
_ UrTy LocVar
IntTy UrTy LocVar
CursorTy = UrTy LocVar -> TcM (UrTy LocVar)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return UrTy LocVar
forall loc. UrTy loc
CursorTy
ensureEqualTy Exp
exp UrTy LocVar
a UrTy LocVar
b = Exp -> String -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
forall a. Eq a => Exp -> String -> a -> a -> TcM a
ensureEqual Exp
exp (String
"Expected these types to be the same: "
                                         String -> ShowS
forall a. [a] -> [a] -> [a]
++ (UrTy LocVar -> String
forall a. Show a => a -> String
show UrTy LocVar
a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (UrTy LocVar -> String
forall a. Show a => a -> String
show UrTy LocVar
b)) UrTy LocVar
a UrTy LocVar
b

ensureEqualTyModCursor :: Exp -> Ty2 -> Ty2 -> TcM Ty2
ensureEqualTyModCursor :: Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyModCursor Exp
_exp UrTy LocVar
CursorTy (PackedTy String
_ LocVar
_) = UrTy LocVar -> TcM (UrTy LocVar)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return UrTy LocVar
forall loc. UrTy loc
CursorTy
ensureEqualTyModCursor Exp
_exp (PackedTy String
_ LocVar
_) UrTy LocVar
CursorTy = UrTy LocVar -> TcM (UrTy LocVar)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return UrTy LocVar
forall loc. UrTy loc
CursorTy
ensureEqualTyModCursor Exp
exp UrTy LocVar
a UrTy LocVar
b = Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
a UrTy LocVar
b

-- | Ensure that two types are equal, ignoring the locations if they are packed.
-- Includes an expression for error reporting.
ensureEqualTyNoLoc :: Exp -> Ty2 -> Ty2 -> TcM Ty2
ensureEqualTyNoLoc :: Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyNoLoc Exp
exp UrTy LocVar
ty1 UrTy LocVar
ty2 =
  case (UrTy LocVar
ty1,UrTy LocVar
ty2) of
    (SymDictTy Maybe LocVar
_ar1 UrTy ()
ty1, SymDictTy Maybe LocVar
_ar2 UrTy ()
ty2) ->
        do UrTy LocVar
ty1' <- UrTy () -> TcM (UrTy LocVar)
forall (f :: * -> *). Applicative f => UrTy () -> f (UrTy LocVar)
dummyTyLocs UrTy ()
ty1
           UrTy LocVar
ty2' <- UrTy () -> TcM (UrTy LocVar)
forall (f :: * -> *). Applicative f => UrTy () -> f (UrTy LocVar)
dummyTyLocs UrTy ()
ty2
           Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyNoLoc Exp
exp UrTy LocVar
ty1' UrTy LocVar
ty2'
    (PackedTy String
dc1 LocVar
_, PackedTy String
dc2 LocVar
_) -> if String
dc1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
dc2
                                        then UrTy LocVar -> TcM (UrTy LocVar)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return UrTy LocVar
ty1
                                        else Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTy Exp
exp UrTy LocVar
ty1 UrTy LocVar
ty2
    (ProdTy [UrTy LocVar]
tys1, ProdTy [UrTy LocVar]
tys2) -> do
        [TcM (UrTy LocVar)]
checks <- [TcM (UrTy LocVar)] -> ExceptT TCError Identity [TcM (UrTy LocVar)]
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcM (UrTy LocVar)]
 -> ExceptT TCError Identity [TcM (UrTy LocVar)])
-> [TcM (UrTy LocVar)]
-> ExceptT TCError Identity [TcM (UrTy LocVar)]
forall a b. (a -> b) -> a -> b
$ ((UrTy LocVar, UrTy LocVar) -> TcM (UrTy LocVar))
-> [(UrTy LocVar, UrTy LocVar)] -> [TcM (UrTy LocVar)]
forall a b. (a -> b) -> [a] -> [b]
L.map (\(UrTy LocVar
ty1,UrTy LocVar
ty2) -> Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyNoLoc Exp
exp UrTy LocVar
ty1 UrTy LocVar
ty2) ([UrTy LocVar] -> [UrTy LocVar] -> [(UrTy LocVar, UrTy LocVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip [UrTy LocVar]
tys1 [UrTy LocVar]
tys2)
        -- TODO: avoid runExcept here
        [TcM (UrTy LocVar)]
-> (TcM (UrTy LocVar) -> ExceptT TCError Identity ())
-> ExceptT TCError Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [TcM (UrTy LocVar)]
checks ((TcM (UrTy LocVar) -> ExceptT TCError Identity ())
 -> ExceptT TCError Identity ())
-> (TcM (UrTy LocVar) -> ExceptT TCError Identity ())
-> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ \TcM (UrTy LocVar)
c -> do
            let c' :: Either TCError (UrTy LocVar)
c' = TcM (UrTy LocVar) -> Either TCError (UrTy LocVar)
forall e a. Except e a -> Either e a
runExcept TcM (UrTy LocVar)
c
            case Either TCError (UrTy LocVar)
c' of
              Left TCError
err -> TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCError
err
              Right UrTy LocVar
_  -> () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        UrTy LocVar -> TcM (UrTy LocVar)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return UrTy LocVar
ty1
    (UrTy LocVar, UrTy LocVar)
_ -> Exp -> UrTy LocVar -> UrTy LocVar -> TcM (UrTy LocVar)
ensureEqualTyModCursor Exp
exp UrTy LocVar
ty1 UrTy LocVar
ty2


-- | Ensure that match cases make sense.
-- Includes an expression for error reporting.
ensureMatchCases :: DDefs Ty2 -> Exp -> Ty2 -> [(DataCon, [(Var,LocVar)], Exp)] -> TcM ()
ensureMatchCases :: DDefs (UrTy LocVar)
-> Exp
-> UrTy LocVar
-> [(String, [(LocVar, LocVar)], Exp)]
-> ExceptT TCError Identity ()
ensureMatchCases DDefs (UrTy LocVar)
ddfs Exp
exp UrTy LocVar
ty [(String, [(LocVar, LocVar)], Exp)]
cs = do
  case UrTy LocVar
ty of
    PackedTy String
tc LocVar
_l -> do
            let cons :: Set String
cons = [String] -> Set String
forall a. Ord a => [a] -> Set a
S.fromList ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$ ((String, [(Bool, UrTy LocVar)]) -> String)
-> [(String, [(Bool, UrTy LocVar)])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
L.map (String, [(Bool, UrTy LocVar)]) -> String
forall a b. (a, b) -> a
fst ([(String, [(Bool, UrTy LocVar)])] -> [String])
-> [(String, [(Bool, UrTy LocVar)])] -> [String]
forall a b. (a -> b) -> a -> b
$ DDef (UrTy LocVar) -> [(String, [(Bool, UrTy LocVar)])]
forall a. DDef a -> [(String, [(Bool, a)])]
dataCons (DDef (UrTy LocVar) -> [(String, [(Bool, UrTy LocVar)])])
-> DDef (UrTy LocVar) -> [(String, [(Bool, UrTy LocVar)])]
forall a b. (a -> b) -> a -> b
$ DDefs (UrTy LocVar) -> String -> DDef (UrTy LocVar)
forall a. Out a => DDefs a -> String -> DDef a
lookupDDef DDefs (UrTy LocVar)
ddfs String
tc
            [(String, [(LocVar, LocVar)], Exp)]
-> ((String, [(LocVar, LocVar)], Exp)
    -> ExceptT TCError Identity ())
-> ExceptT TCError Identity [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(String, [(LocVar, LocVar)], Exp)]
cs (((String, [(LocVar, LocVar)], Exp) -> ExceptT TCError Identity ())
 -> ExceptT TCError Identity [()])
-> ((String, [(LocVar, LocVar)], Exp)
    -> ExceptT TCError Identity ())
-> ExceptT TCError Identity [()]
forall a b. (a -> b) -> a -> b
$ \(String
dc,[(LocVar, LocVar)]
_,Exp
_) ->
                do if String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member String
dc Set String
cons
                   then () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                   else TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC String
"Invalid case statement" Exp
exp
            () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    UrTy LocVar
_ -> TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC String
"Cannot case on non-packed type" Exp
exp

-- | Ensure a type is at a particular location.
-- Includes an expression for error reporting.
ensurePackedLoc :: Exp -> Ty2 -> LocVar -> TcM ()
ensurePackedLoc :: Exp -> UrTy LocVar -> LocVar -> ExceptT TCError Identity ()
ensurePackedLoc Exp
exp UrTy LocVar
ty LocVar
l =
    case UrTy LocVar
ty of
      PackedTy String
_ LocVar
l1 -> if LocVar
l1 LocVar -> LocVar -> Bool
forall a. Eq a => a -> a -> Bool
== LocVar
l then () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                       else TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Wrong location in type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (UrTy LocVar -> String
forall a. Show a => a -> String
show UrTy LocVar
ty)) Exp
exp
      UrTy LocVar
_ -> TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC String
"Expected a packed type" Exp
exp

-- need to check chain of aliased locations
-- linit is the location in the type i.e lout653
-- ensureAfterConstant expects l664 to be after lout653

-- | Ensure the locations all line up with the constraints in a data constructor application.
-- Includes an expression for error reporting.
ensureDataCon :: Exp -> LocVar -> [Ty2] -> ConstraintSet -> TcM ()
ensureDataCon :: Exp
-> LocVar
-> [UrTy LocVar]
-> ConstraintSet
-> ExceptT TCError Identity ()
ensureDataCon Exp
exp LocVar
linit0 [UrTy LocVar]
tys ConstraintSet
cs = (Maybe (UrTy LocVar)
-> LocVar -> [UrTy LocVar] -> ExceptT TCError Identity ()
go Maybe (UrTy LocVar)
forall a. Maybe a
Nothing LocVar
linit0 [UrTy LocVar]
tys)
    where go :: Maybe (UrTy LocVar)
-> LocVar -> [UrTy LocVar] -> ExceptT TCError Identity ()
go Maybe (UrTy LocVar)
Nothing LocVar
linit ((PackedTy String
dc LocVar
l):[UrTy LocVar]
tys) = do
            Exp
-> ConstraintSet -> LocVar -> LocVar -> ExceptT TCError Identity ()
ensureAfterConstant Exp
exp ConstraintSet
cs LocVar
linit LocVar
l
            Maybe (UrTy LocVar)
-> LocVar -> [UrTy LocVar] -> ExceptT TCError Identity ()
go (UrTy LocVar -> Maybe (UrTy LocVar)
forall a. a -> Maybe a
Just (String -> LocVar -> UrTy LocVar
forall loc. String -> loc -> UrTy loc
PackedTy String
dc LocVar
l)) LocVar
l [UrTy LocVar]
tys

          go Maybe (UrTy LocVar)
Nothing LocVar
linit (UrTy LocVar
_ty:[UrTy LocVar]
tys) = do
            case ConstraintSet -> LocVar -> Maybe LocVar
getAfterConstant ConstraintSet
cs LocVar
linit of
              Maybe LocVar
Nothing     -> Maybe (UrTy LocVar)
-> LocVar -> [UrTy LocVar] -> ExceptT TCError Identity ()
go Maybe (UrTy LocVar)
forall a. Maybe a
Nothing LocVar
linit [UrTy LocVar]
tys
              Just LocVar
linit' -> Maybe (UrTy LocVar)
-> LocVar -> [UrTy LocVar] -> ExceptT TCError Identity ()
go Maybe (UrTy LocVar)
forall a. Maybe a
Nothing LocVar
linit' [UrTy LocVar]
tys

          go (Just (PackedTy String
_dc1 LocVar
l1)) LocVar
_linit ((PackedTy String
dc2 LocVar
l2):[UrTy LocVar]
tys) = do
            Exp
-> ConstraintSet -> LocVar -> LocVar -> ExceptT TCError Identity ()
ensureAfterPacked Exp
exp ConstraintSet
cs LocVar
l1 LocVar
l2
            Maybe (UrTy LocVar)
-> LocVar -> [UrTy LocVar] -> ExceptT TCError Identity ()
go (UrTy LocVar -> Maybe (UrTy LocVar)
forall a. a -> Maybe a
Just (String -> LocVar -> UrTy LocVar
forall loc. String -> loc -> UrTy loc
PackedTy String
dc2 LocVar
l2)) LocVar
l2 [UrTy LocVar]
tys

          go (Just (PackedTy String
_dc LocVar
_l1)) LocVar
linit (UrTy LocVar
_ty:[UrTy LocVar]
tys) =
              Maybe (UrTy LocVar)
-> LocVar -> [UrTy LocVar] -> ExceptT TCError Identity ()
go Maybe (UrTy LocVar)
forall a. Maybe a
Nothing LocVar
linit [UrTy LocVar]
tys
          go Maybe (UrTy LocVar)
_ LocVar
_ [] = () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          go Maybe (UrTy LocVar)
_ LocVar
_ [UrTy LocVar]
_  = String -> ExceptT TCError Identity ()
forall a. HasCallStack => String -> a
internalError String
"Unxpected case reached: L2:ensureDataCon"


-- | Ensure that one location is +c after another location in the constraint set.
-- Includes an expression for error reporting.
ensureAfterConstant :: Exp -> ConstraintSet -> LocVar -> LocVar -> TcM ()
ensureAfterConstant :: Exp
-> ConstraintSet -> LocVar -> LocVar -> ExceptT TCError Identity ()
ensureAfterConstant Exp
exp (ConstraintSet Set LocConstraint
cs) LocVar
l1 LocVar
l2 =
    if (LocConstraint -> Bool) -> [LocConstraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
L.any LocConstraint -> Bool
f ([LocConstraint] -> Bool) -> [LocConstraint] -> Bool
forall a b. (a -> b) -> a -> b
$ Set LocConstraint -> [LocConstraint]
forall a. Set a -> [a]
S.toList Set LocConstraint
cs then () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    else TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> LocVar -> LocVar -> TCError
LocationTC String
"Expected after constant relationship" Exp
exp LocVar
l1 LocVar
l2
    -- l1 is before l2
    where f :: LocConstraint -> Bool
f (AfterConstantC Int
_i LocVar
l1' LocVar
l2') = LocVar
l1' LocVar -> LocVar -> Bool
forall a. Eq a => a -> a -> Bool
== LocVar
l1 Bool -> Bool -> Bool
&& LocVar
l2' LocVar -> LocVar -> Bool
forall a. Eq a => a -> a -> Bool
== LocVar
l2
          f LocConstraint
_ = Bool
False

-- | Ensure that one location is a variable size after another location in the constraint set.
-- Includes an expression for error reporting.
ensureAfterPacked :: Exp -> ConstraintSet -> LocVar -> LocVar -> TcM ()
ensureAfterPacked :: Exp
-> ConstraintSet -> LocVar -> LocVar -> ExceptT TCError Identity ()
ensureAfterPacked  Exp
exp (ConstraintSet Set LocConstraint
cs) LocVar
l1 LocVar
l2 =
    if (LocConstraint -> Bool) -> [LocConstraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
L.any LocConstraint -> Bool
f ([LocConstraint] -> Bool) -> [LocConstraint] -> Bool
forall a b. (a -> b) -> a -> b
$ Set LocConstraint -> [LocConstraint]
forall a. Set a -> [a]
S.toList Set LocConstraint
cs then () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    else TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> LocVar -> LocVar -> TCError
LocationTC String
"Expected after packed relationship" Exp
exp LocVar
l1 LocVar
l2
    where f :: LocConstraint -> Bool
f (AfterVariableC LocVar
_v LocVar
l1' LocVar
l2') = LocVar
l1' LocVar -> LocVar -> Bool
forall a. Eq a => a -> a -> Bool
== LocVar
l1 Bool -> Bool -> Bool
&& LocVar
l2' LocVar -> LocVar -> Bool
forall a. Eq a => a -> a -> Bool
== LocVar
l2
          f LocConstraint
_ = Bool
False

getAfterConstant :: ConstraintSet -> LocVar -> Maybe LocVar
getAfterConstant :: ConstraintSet -> LocVar -> Maybe LocVar
getAfterConstant (ConstraintSet Set LocConstraint
cs) LocVar
l0 =
  let mb_cs :: Maybe LocConstraint
mb_cs = (LocConstraint -> Bool) -> Set LocConstraint -> Maybe LocConstraint
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (\LocConstraint
c -> case LocConstraint
c of
                         AfterConstantC Int
_i LocVar
l1 LocVar
_l2 | LocVar
l1 LocVar -> LocVar -> Bool
forall a. Eq a => a -> a -> Bool
== LocVar
l0 -> Bool
True
                         LocConstraint
_ -> Bool
False)
              Set LocConstraint
cs
  in case Maybe LocConstraint
mb_cs of
       Just (AfterConstantC Int
_i LocVar
_l1 LocVar
l2) -> LocVar -> Maybe LocVar
forall a. a -> Maybe a
Just LocVar
l2
       Maybe LocConstraint
_ -> Maybe LocVar
forall a. Maybe a
Nothing


extendTS
  :: LocVar
     -> (Modality, Aliased) -> LocationTypeState -> LocationTypeState
extendTS :: LocVar
-> (Modality, Bool) -> LocationTypeState -> LocationTypeState
extendTS LocVar
v (Modality, Bool)
d (LocationTypeState Map LocVar (Modality, Bool)
ls) = Map LocVar (Modality, Bool) -> LocationTypeState
LocationTypeState (Map LocVar (Modality, Bool) -> LocationTypeState)
-> Map LocVar (Modality, Bool) -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ LocVar
-> (Modality, Bool)
-> Map LocVar (Modality, Bool)
-> Map LocVar (Modality, Bool)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert LocVar
v (Modality, Bool)
d Map LocVar (Modality, Bool)
ls

removeTS :: LocVar -> LocationTypeState -> LocationTypeState
removeTS :: LocVar -> LocationTypeState -> LocationTypeState
removeTS LocVar
l (LocationTypeState Map LocVar (Modality, Bool)
ls) = Map LocVar (Modality, Bool) -> LocationTypeState
LocationTypeState (Map LocVar (Modality, Bool) -> LocationTypeState)
-> Map LocVar (Modality, Bool) -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ LocVar
-> Map LocVar (Modality, Bool) -> Map LocVar (Modality, Bool)
forall k a. Ord k => k -> Map k a -> Map k a
M.delete LocVar
l Map LocVar (Modality, Bool)
ls

setAfter :: LocVar -> LocationTypeState -> LocationTypeState
setAfter :: LocVar -> LocationTypeState -> LocationTypeState
setAfter LocVar
l (LocationTypeState Map LocVar (Modality, Bool)
ls) = Map LocVar (Modality, Bool) -> LocationTypeState
LocationTypeState (Map LocVar (Modality, Bool) -> LocationTypeState)
-> Map LocVar (Modality, Bool) -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ ((Modality, Bool) -> (Modality, Bool))
-> LocVar
-> Map LocVar (Modality, Bool)
-> Map LocVar (Modality, Bool)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust (\(Modality
m,Bool
_) -> (Modality
m,Bool
True)) LocVar
l Map LocVar (Modality, Bool)
ls

_lookupTS :: Exp -> LocVar -> LocationTypeState -> TcM (Modality,Bool)
_lookupTS :: Exp -> LocVar -> LocationTypeState -> TcM (Modality, Bool)
_lookupTS Exp
exp LocVar
l (LocationTypeState Map LocVar (Modality, Bool)
ls) =
    case LocVar -> Map LocVar (Modality, Bool) -> Maybe (Modality, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup LocVar
l Map LocVar (Modality, Bool)
ls of
      Maybe (Modality, Bool)
Nothing -> TCError -> TcM (Modality, Bool)
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM (Modality, Bool))
-> TCError -> TcM (Modality, Bool)
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Failed lookup of location " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocVar -> String
forall a. Show a => a -> String
show LocVar
l)) Exp
exp
      Just (Modality, Bool)
d -> (Modality, Bool) -> TcM (Modality, Bool)
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Modality, Bool)
d

extendConstrs :: LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs :: LocConstraint -> ConstraintSet -> ConstraintSet
extendConstrs LocConstraint
c (ConstraintSet Set LocConstraint
cs) = Set LocConstraint -> ConstraintSet
ConstraintSet (Set LocConstraint -> ConstraintSet)
-> Set LocConstraint -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ LocConstraint -> Set LocConstraint -> Set LocConstraint
forall a. Ord a => a -> Set a -> Set a
S.insert LocConstraint
c Set LocConstraint
cs

switchOutLoc :: Exp -> LocationTypeState -> LocVar -> TcM LocationTypeState
switchOutLoc :: Exp -> LocationTypeState -> LocVar -> TcM LocationTypeState
switchOutLoc Exp
exp ts :: LocationTypeState
ts@(LocationTypeState Map LocVar (Modality, Bool)
ls) LocVar
l =
    case LocVar -> Map LocVar (Modality, Bool) -> Maybe (Modality, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup LocVar
l Map LocVar (Modality, Bool)
ls of
      Maybe (Modality, Bool)
Nothing -> TCError -> TcM LocationTypeState
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM LocationTypeState)
-> TCError -> TcM LocationTypeState
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Unknown location " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocVar -> String
forall a. Show a => a -> String
show LocVar
l)) Exp
exp
      Just (Modality
Output,Bool
a) -> LocationTypeState -> TcM LocationTypeState
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LocationTypeState -> TcM LocationTypeState)
-> LocationTypeState -> TcM LocationTypeState
forall a b. (a -> b) -> a -> b
$ Map LocVar (Modality, Bool) -> LocationTypeState
LocationTypeState (Map LocVar (Modality, Bool) -> LocationTypeState)
-> Map LocVar (Modality, Bool) -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ ((Modality, Bool) -> Maybe (Modality, Bool))
-> LocVar
-> Map LocVar (Modality, Bool)
-> Map LocVar (Modality, Bool)
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
M.update (\(Modality, Bool)
_ -> (Modality, Bool) -> Maybe (Modality, Bool)
forall a. a -> Maybe a
Just (Modality
Input,Bool
a)) LocVar
l Map LocVar (Modality, Bool)
ls
      Just (Modality
Input,Bool
_a) -> LocationTypeState -> TcM LocationTypeState
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return LocationTypeState
ts

_absentAfter :: Exp -> LocationTypeState -> LocVar -> TcM ()
_absentAfter :: Exp -> LocationTypeState -> LocVar -> ExceptT TCError Identity ()
_absentAfter Exp
exp (LocationTypeState Map LocVar (Modality, Bool)
ls) LocVar
l =
    case LocVar -> Map LocVar (Modality, Bool) -> Maybe (Modality, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup LocVar
l Map LocVar (Modality, Bool)
ls of
      Maybe (Modality, Bool)
Nothing -> TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Unknown location " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocVar -> String
forall a. Show a => a -> String
show LocVar
l)) Exp
exp
      Just (Modality
_m,Bool
False) -> () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just (Modality
_m,Bool
True) -> TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Alias of location " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocVar -> String
forall a. Show a => a -> String
show LocVar
l)) Exp
exp

-- | Ensure that a location is not already "defined" by a start constraint.
absentStart :: Exp -> ConstraintSet -> Region -> TcM ()
absentStart :: Exp -> ConstraintSet -> Region -> ExceptT TCError Identity ()
absentStart Exp
exp (ConstraintSet Set LocConstraint
cs) Region
r = [LocConstraint] -> ExceptT TCError Identity ()
go ([LocConstraint] -> ExceptT TCError Identity ())
-> [LocConstraint] -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ Set LocConstraint -> [LocConstraint]
forall a. Set a -> [a]
S.toList Set LocConstraint
cs
    where go :: [LocConstraint] -> ExceptT TCError Identity ()
go ((StartOfC LocVar
_l Region
r'):[LocConstraint]
cs) =
              if Region
r Region -> Region -> Bool
forall a. Eq a => a -> a -> Bool
== Region
r'
              then TCError -> ExceptT TCError Identity ()
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ExceptT TCError Identity ())
-> TCError -> ExceptT TCError Identity ()
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Repeated start of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Region -> String
forall a. Show a => a -> String
show Region
r)) Exp
exp
              else [LocConstraint] -> ExceptT TCError Identity ()
go [LocConstraint]
cs
          go (LocConstraint
_:[LocConstraint]
cs) = [LocConstraint] -> ExceptT TCError Identity ()
go [LocConstraint]
cs
          go [] = () -> ExceptT TCError Identity ()
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


removeLoc :: Exp -> LocationTypeState -> LocVar -> TcM LocationTypeState
removeLoc :: Exp -> LocationTypeState -> LocVar -> TcM LocationTypeState
removeLoc Exp
exp (LocationTypeState Map LocVar (Modality, Bool)
ls) LocVar
l =
    if LocVar -> Map LocVar (Modality, Bool) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
M.member LocVar
l Map LocVar (Modality, Bool)
ls
    then LocationTypeState -> TcM LocationTypeState
forall a. a -> ExceptT TCError Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LocationTypeState -> TcM LocationTypeState)
-> LocationTypeState -> TcM LocationTypeState
forall a b. (a -> b) -> a -> b
$ Map LocVar (Modality, Bool) -> LocationTypeState
LocationTypeState (Map LocVar (Modality, Bool) -> LocationTypeState)
-> Map LocVar (Modality, Bool) -> LocationTypeState
forall a b. (a -> b) -> a -> b
$ LocVar
-> Map LocVar (Modality, Bool) -> Map LocVar (Modality, Bool)
forall k a. Ord k => k -> Map k a -> Map k a
M.delete LocVar
l Map LocVar (Modality, Bool)
ls
    else TCError -> TcM LocationTypeState
forall a. TCError -> ExceptT TCError Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TcM LocationTypeState)
-> TCError -> TcM LocationTypeState
forall a b. (a -> b) -> a -> b
$ String -> Exp -> TCError
GenericTC (String
"Cannot remove location " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LocVar -> String
forall a. Show a => a -> String
show LocVar
l)) Exp
exp

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