{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Typechecking and elaboration for the Swarm world DSL. For more
-- information, see:
--
--   https://byorgey.wordpress.com/2023/07/13/compiling-to-intrinsically-typed-combinators/
module Swarm.Game.World.Typecheck where

import Control.Algebra (Has)
import Control.Effect.Reader (Reader, ask)
import Control.Effect.Throw (Throw, throwError)
import Data.Foldable (Foldable (..))
import Data.Foldable qualified as F
import Data.Functor.Const qualified as F
import Data.Kind (Type)
import Data.List.Extra (enumerate)
import Data.List.NonEmpty qualified as NE
import Data.Map (Map)
import Data.Map qualified as M
import Data.Semigroup (Last (..))
import Data.Text (Text)
import Data.Type.Equality (TestEquality (..), type (:~:) (Refl))
import Prettyprinter
import Swarm.Game.Entity (lookupEntityName)
import Swarm.Game.Land
import Swarm.Game.Terrain
import Swarm.Game.World.Syntax
import Swarm.Pretty (PrettyPrec (..), pparens, ppr)
import Swarm.Util (showT)
import Swarm.Util.Erasable
import Prelude hiding (Foldable (..), lookup)

------------------------------------------------------------
-- Type classes for monoidal world values

-- We could use Semigroup and Monoid, but we want to use the two
-- classes separately and make instances for base types, so it's
-- cleaner to just make our own classes (the instances would be
-- orphans if we used Semigroup and Monoid).

class Empty e where
  empty :: e

instance Empty CellVal where
  empty :: CellVal
empty = TerrainType -> Erasable (Last Entity) -> [TRobot] -> CellVal
CellVal TerrainType
forall a. Monoid a => a
mempty Erasable (Last Entity)
forall a. Monoid a => a
mempty [TRobot]
forall a. Monoid a => a
mempty

class Over m where
  (<!>) :: m -> m -> m

instance Over Bool where
  Bool
_ <!> :: Bool -> Bool -> Bool
<!> Bool
x = Bool
x

instance Over Integer where
  Integer
_ <!> :: Integer -> Integer -> Integer
<!> Integer
x = Integer
x

instance Over Double where
  Double
_ <!> :: Double -> Double -> Double
<!> Double
x = Double
x

instance Over CellVal where
  CellVal TerrainType
t1 Erasable (Last Entity)
e1 [TRobot]
r1 <!> :: CellVal -> CellVal -> CellVal
<!> CellVal TerrainType
t2 Erasable (Last Entity)
e2 [TRobot]
r2 = TerrainType -> Erasable (Last Entity) -> [TRobot] -> CellVal
CellVal (TerrainType
t1 TerrainType -> TerrainType -> TerrainType
forall a. Semigroup a => a -> a -> a
<> TerrainType
t2) (Erasable (Last Entity)
e1 Erasable (Last Entity)
-> Erasable (Last Entity) -> Erasable (Last Entity)
forall a. Semigroup a => a -> a -> a
<> Erasable (Last Entity)
e2) ([TRobot]
r1 [TRobot] -> [TRobot] -> [TRobot]
forall a. Semigroup a => a -> a -> a
<> [TRobot]
r2)

------------------------------------------------------------
-- Type class for type-indexed application

infixl 1 $$
class Applicable t where
  ($$) :: t (a -> b) -> t a -> t b

------------------------------------------------------------
-- Distinguishing functions and non-functions at the type level

-- In several places, for efficiency we will require something to be
-- not a function, which we can enforce using the 'NotFun' constraint.

type family IsFun a where
  IsFun (_ -> _) = 'True
  IsFun _ = 'False

type NotFun a = IsFun a ~ 'False

------------------------------------------------------------
-- Type-indexed constants

-- | Type-indexed constants.  These include both language built-ins
--   (@if@, arithmetic, comparison, @<>@, etc.) as well as combinators
--   (@S@, @I@, @C@, @K@, @B@, @Φ@) we will use both for elaboration
--   and later as a compilation target.
data Const :: Type -> Type where
  CLit :: (Show a, NotFun a) => a -> Const a
  CCell :: CellVal -> Const CellVal
  -- We have a separate CCell instead of using CLit for cells so that we can
  -- later extract all the entities from a world expression.
  CFI :: Const (Integer -> Double)
  CIf :: Const (Bool -> a -> a -> a)
  CNot :: Const (Bool -> Bool)
  CNeg :: (Num a, NotFun a) => Const (a -> a)
  CAbs :: (Num a, NotFun a) => Const (a -> a)
  CAnd :: Const (Bool -> Bool -> Bool)
  COr :: Const (Bool -> Bool -> Bool)
  CAdd :: (Num a, NotFun a) => Const (a -> a -> a)
  CSub :: (Num a, NotFun a) => Const (a -> a -> a)
  CMul :: (Num a, NotFun a) => Const (a -> a -> a)
  CDiv :: (Fractional a, NotFun a) => Const (a -> a -> a)
  CIDiv :: (Integral a, NotFun a) => Const (a -> a -> a)
  CMod :: (Integral a, NotFun a) => Const (a -> a -> a)
  CEq :: (Eq a, NotFun a) => Const (a -> a -> Bool)
  CNeq :: (Eq a, NotFun a) => Const (a -> a -> Bool)
  CLt :: (Ord a, NotFun a) => Const (a -> a -> Bool)
  CLeq :: (Ord a, NotFun a) => Const (a -> a -> Bool)
  CGt :: (Ord a, NotFun a) => Const (a -> a -> Bool)
  CGeq :: (Ord a, NotFun a) => Const (a -> a -> Bool)
  CMask :: (Empty a, NotFun a) => Const (World Bool -> World a -> World a)
  CSeed :: Const Integer
  CCoord :: Axis -> Const (World Integer)
  CHash :: Const (World Integer)
  CPerlin :: Const (Integer -> Integer -> Double -> Double -> World Double)
  COver :: (Over a, NotFun a) => Const (a -> a -> a)
  CIMap :: NotFun a => Const (World Integer -> World Integer -> World a -> World a)
  -- Combinators generated during elaboration + variable abstraction
  K :: Const (a -> b -> a)
  S :: Const ((a -> b -> c) -> (a -> b) -> a -> c)
  I :: Const (a -> a)
  B :: Const ((b -> c) -> (a -> b) -> a -> c)
  C :: Const ((a -> b -> c) -> b -> a -> c)
  -- Phoenix combinator, aka liftA2.  Including this combinator in the
  -- target set is not typical, but it turns out to be very helpful in
  -- elaborating the "over" operation.
  Φ :: Const ((a -> b -> c) -> (d -> a) -> (d -> b) -> (d -> c))

deriving instance Show (Const ty)

class HasConst t where
  embed :: Const a -> t a

infixl 1 .$$
(.$$) :: (HasConst t, Applicable t) => Const (a -> b) -> t a -> t b
Const (a -> b)
c .$$ :: forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ t a
t = Const (a -> b) -> t (a -> b)
forall a. Const a -> t a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (a -> b)
c t (a -> b) -> t a -> t b
forall a b. t (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ t a
t

infixl 1 $$.
($$.) :: (HasConst t, Applicable t) => t (a -> b) -> Const a -> t b
t (a -> b)
t $$. :: forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
t (a -> b) -> Const a -> t b
$$. Const a
c = t (a -> b)
t t (a -> b) -> t a -> t b
forall a b. t (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ Const a -> t a
forall a. Const a -> t a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const a
c

infixl 1 .$$.
(.$$.) :: (HasConst t, Applicable t) => Const (a -> b) -> Const a -> t b
Const (a -> b)
c1 .$$. :: forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> Const a -> t b
.$$. Const a
c2 = Const (a -> b) -> t (a -> b)
forall a. Const a -> t a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (a -> b)
c1 t (a -> b) -> t a -> t b
forall a b. t (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ Const a -> t a
forall a. Const a -> t a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const a
c2

instance PrettyPrec (Const α) where
  prettyPrec :: forall ann. Int -> Const α -> Doc ann
prettyPrec Int
_ = \case
    CLit α
a -> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (α -> Text
forall a. Show a => a -> Text
showT α
a)
    CCell CellVal
c -> CellVal -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr CellVal
c
    Const α
CFI -> Doc ann
"fromIntegral"
    Const α
CIf -> Doc ann
"if"
    Const α
CNot -> Doc ann
"not"
    Const α
CNeg -> Doc ann
"negate"
    Const α
CAbs -> Doc ann
"abs"
    Const α
CAnd -> Doc ann
"and"
    Const α
COr -> Doc ann
"or"
    Const α
CAdd -> Doc ann
"add"
    Const α
CSub -> Doc ann
"sub"
    Const α
CMul -> Doc ann
"mul"
    Const α
CDiv -> Doc ann
"div"
    Const α
CIDiv -> Doc ann
"idiv"
    Const α
CMod -> Doc ann
"mod"
    Const α
CEq -> Doc ann
"eq"
    Const α
CNeq -> Doc ann
"neq"
    Const α
CLt -> Doc ann
"lt"
    Const α
CLeq -> Doc ann
"leq"
    Const α
CGt -> Doc ann
"gt"
    Const α
CGeq -> Doc ann
"geq"
    Const α
CMask -> Doc ann
"mask"
    Const α
CSeed -> Doc ann
"seed"
    CCoord Axis
ax -> Axis -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Axis
ax
    Const α
CHash -> Doc ann
"hash"
    Const α
CPerlin -> Doc ann
"perlin"
    Const α
COver -> Doc ann
"over"
    Const α
CIMap -> Doc ann
"imap"
    Const α
K -> Doc ann
"K"
    Const α
S -> Doc ann
"S"
    Const α
I -> Doc ann
"I"
    Const α
B -> Doc ann
"B"
    Const α
C -> Doc ann
"C"
    Const α
Φ -> Doc ann
"Φ"

------------------------------------------------------------
-- Intrinsically typed core language

-- | Type-level list append.
type family Append (xs :: [k]) (ys :: [k]) :: [k] where
  Append '[] ys = ys
  Append (x ': xs) ys = x ': Append xs ys

-- | Type- and context-indexed de Bruijn indices. (v :: Idx g a) means
--   v represents a variable with type a in a type context g.
data Idx :: [Type] -> Type -> Type where
  VZ :: Idx (ty ': g) ty
  VS :: Idx g ty -> Idx (x ': g) ty

deriving instance Show (Idx g ty)

idxToNat :: Idx g a -> Int
idxToNat :: forall (g :: [*]) a. Idx g a -> Int
idxToNat Idx g a
VZ = Int
0
idxToNat (VS Idx g a
x) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Idx g a -> Int
forall (g :: [*]) a. Idx g a -> Int
idxToNat Idx g a
x

-- | A variable valid in one context is also valid in another extended
--   context with additional variables.
weakenVar :: forall h g a. Idx g a -> Idx (Append g h) a
weakenVar :: forall (h :: [*]) (g :: [*]) a. Idx g a -> Idx (Append g h) a
weakenVar Idx g a
VZ = Idx (a : Append g h) a
Idx (Append g h) a
forall ty (a :: [*]). Idx (ty : a) ty
VZ
weakenVar (VS Idx g a
x) = Idx (Append g h) a -> Idx (x : Append g h) a
forall (a :: [*]) ty b. Idx a ty -> Idx (b : a) ty
VS (forall (h :: [*]) (g :: [*]) a. Idx g a -> Idx (Append g h) a
weakenVar @h Idx g a
x)

-- | Type-indexed terms.  Note this is a stripped-down core language,
--   with only variables, lambdas, application, and constants.
data TTerm :: [Type] -> Type -> Type where
  TVar :: Idx g a -> TTerm g a
  TLam :: TTerm (ty1 ': g) ty2 -> TTerm g (ty1 -> ty2)
  TApp :: TTerm g (a -> b) -> TTerm g a -> TTerm g b
  TConst :: Const a -> TTerm g a

deriving instance Show (TTerm g ty)

instance Applicable (TTerm g) where
  TConst Const (a -> b)
I $$ :: forall a b. TTerm g (a -> b) -> TTerm g a -> TTerm g b
$$ TTerm g a
x = TTerm g a
TTerm g b
x
  TTerm g (a -> b)
f $$ TTerm g a
x = TTerm g (a -> b) -> TTerm g a -> TTerm g b
forall (g :: [*]) a b. TTerm g (a -> b) -> TTerm g a -> TTerm g b
TApp TTerm g (a -> b)
f TTerm g a
x

instance HasConst (TTerm g) where
  embed :: forall a. Const a -> TTerm g a
embed = Const a -> TTerm g a
forall a (g :: [*]). Const a -> TTerm g a
TConst

instance PrettyPrec (TTerm g α) where
  prettyPrec :: Int -> TTerm g α -> Doc ann
  prettyPrec :: forall ann. Int -> TTerm g α -> Doc ann
prettyPrec Int
p = \case
    TVar Idx g α
ix -> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Idx g α -> Int
forall (g :: [*]) a. Idx g a -> Int
idxToNat Idx g α
ix)
    TLam TTerm (ty1 : g) ty2
t ->
      Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
        Doc ann
"λ." Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TTerm (ty1 : g) ty2 -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TTerm (ty1 : g) ty2
t
    TApp TTerm g (a -> α)
t1 TTerm g a
t2 ->
      Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
        Int -> TTerm g (a -> α) -> Doc ann
forall ann. Int -> TTerm g (a -> α) -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
1 TTerm g (a -> α)
t1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> TTerm g a -> Doc ann
forall ann. Int -> TTerm g a -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
2 TTerm g a
t2
    TConst Const α
c -> Const α -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Const α
c

-- | A term valid in one context is also valid in another extended
--   context with additional variables (which the term does not use).
weaken :: forall h g a. TTerm g a -> TTerm (Append g h) a
weaken :: forall (h :: [*]) (g :: [*]) a. TTerm g a -> TTerm (Append g h) a
weaken (TVar Idx g a
x) = Idx (Append g h) a -> TTerm (Append g h) a
forall (g :: [*]) a. Idx g a -> TTerm g a
TVar (forall (h :: [*]) (g :: [*]) a. Idx g a -> Idx (Append g h) a
weakenVar @h Idx g a
x)
weaken (TLam TTerm (ty1 : g) ty2
t) = TTerm (ty1 : Append g h) ty2 -> TTerm (Append g h) (ty1 -> ty2)
forall a (g :: [*]) b. TTerm (a : g) b -> TTerm g (a -> b)
TLam (forall (h :: [*]) (g :: [*]) a. TTerm g a -> TTerm (Append g h) a
weaken @h TTerm (ty1 : g) ty2
t)
weaken (TApp TTerm g (a -> a)
t1 TTerm g a
t2) = TTerm (Append g h) (a -> a)
-> TTerm (Append g h) a -> TTerm (Append g h) a
forall (g :: [*]) a b. TTerm g (a -> b) -> TTerm g a -> TTerm g b
TApp (forall (h :: [*]) (g :: [*]) a. TTerm g a -> TTerm (Append g h) a
weaken @h TTerm g (a -> a)
t1) (forall (h :: [*]) (g :: [*]) a. TTerm g a -> TTerm (Append g h) a
weaken @h TTerm g a
t2)
weaken (TConst Const a
c) = Const a -> TTerm (Append g h) a
forall a (g :: [*]). Const a -> TTerm g a
TConst Const a
c

------------------------------------------------------------
-- Errors

-- | Errors that can occur during typechecking/elaboration.
data CheckErr where
  ApplyErr :: Some (TTerm g) -> Some (TTerm g) -> CheckErr
  NoInstance :: Text -> TTy a -> CheckErr
  Unbound :: Text -> CheckErr
  BadType :: Some (TTerm g) -> TTy b -> CheckErr
  BadDivType :: TTy a -> CheckErr
  BadInferOp :: [SomeTy] -> Op -> CheckErr
  UnknownImport :: Text -> CheckErr
  NotAThing :: Text -> CellTag -> CheckErr
  NotAnything :: Text -> CheckErr

deriving instance Show CheckErr

instance PrettyPrec CheckErr where
  prettyPrec :: forall ann. Int -> CheckErr -> Doc ann
prettyPrec Int
_ = \case
    ApplyErr (Some TTy α
ty1 TTerm g α
t1) (Some TTy α
ty2 TTerm g α
t2) ->
      Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc ann -> Doc ann)
-> ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$
        [ Doc ann
"Error in application:"
        , Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (TTerm g α -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TTerm g α
t1) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" has type " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (TTy α -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy α
ty1)
        , Doc ann
"and cannot be applied to"
        , Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (TTerm g α -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TTerm g α
t2) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" which has type " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (TTy α -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy α
ty2)
        ]
    NoInstance Text
cls TTy a
ty -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (TTy a -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy a
ty) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not an instance of" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
cls
    Unbound Text
x -> Doc ann
"Undefined variable" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
x
    BadType (Some TTy α
tty TTerm g α
t) TTy b
ty ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep
        [Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (TTerm g α -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TTerm g α
t), Doc ann
"has type", Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (TTy α -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy α
tty), Doc ann
"and cannot be given type", Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (TTy b -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy b
ty)]
    BadDivType TTy a
ty -> Doc ann
"Division operator used at type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (TTy a -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy a
ty)
    BadInferOp [SomeTy]
tys Op
op -> Doc ann
"Bad call to inferOp" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([SomeTy] -> String
forall a. Show a => a -> String
show [SomeTy]
tys) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Op -> String
forall a. Show a => a -> String
show Op
op)
    UnknownImport Text
key -> Doc ann
"Import" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
key) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"not found"
    NotAThing Text
item CellTag
tag -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
item) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> CellTag -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr CellTag
tag
    NotAnything Text
item -> Doc ann
"Cannot resolve cell item" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
item)

------------------------------------------------------------
-- Type representations

-- | Base types.
data Base :: Type -> Type where
  BInt :: Base Integer
  BFloat :: Base Double
  BBool :: Base Bool
  BCell :: Base CellVal

deriving instance Show (Base ty)

-- | Testing base type representations for equality to yield reflected
--   type-level equalities.
instance TestEquality Base where
  testEquality :: forall a b. Base a -> Base b -> Maybe (a :~: b)
testEquality Base a
BInt Base b
BInt = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality Base a
BFloat Base b
BFloat = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality Base a
BBool Base b
BBool = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality Base a
BCell Base b
BCell = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality Base a
_ Base b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance PrettyPrec (Base α) where
  prettyPrec :: forall ann. Int -> Base α -> Doc ann
prettyPrec Int
_ = \case
    Base α
BInt -> Doc ann
"int"
    Base α
BFloat -> Doc ann
"float"
    Base α
BBool -> Doc ann
"bool"
    Base α
BCell -> Doc ann
"cell"

-- | Type representations indexed by the corresponding host language
--   type.
data TTy :: Type -> Type where
  TTyBase :: Base t -> TTy t
  (:->:) :: TTy a -> TTy b -> TTy (a -> b)
  TTyWorld :: TTy t -> TTy (World t)

infixr 0 :->:

pattern TTyBool :: TTy Bool
pattern $mTTyBool :: forall {r}. TTy Bool -> ((# #) -> r) -> ((# #) -> r) -> r
$bTTyBool :: TTy Bool
TTyBool = TTyBase BBool

pattern TTyInt :: TTy Integer
pattern $mTTyInt :: forall {r}. TTy Integer -> ((# #) -> r) -> ((# #) -> r) -> r
$bTTyInt :: TTy Integer
TTyInt = TTyBase BInt

pattern TTyFloat :: TTy Double
pattern $mTTyFloat :: forall {r}. TTy Double -> ((# #) -> r) -> ((# #) -> r) -> r
$bTTyFloat :: TTy Double
TTyFloat = TTyBase BFloat

pattern TTyCell :: TTy CellVal
pattern $mTTyCell :: forall {r}. TTy CellVal -> ((# #) -> r) -> ((# #) -> r) -> r
$bTTyCell :: TTy CellVal
TTyCell = TTyBase BCell

deriving instance Show (TTy ty)

-- | Testing type representations for equality to yield reflected
--   type-level equalities.
instance TestEquality TTy where
  testEquality :: forall a b. TTy a -> TTy b -> Maybe (a :~: b)
testEquality (TTyBase Base a
b1) (TTyBase Base b
b2) = Base a -> Base b -> Maybe (a :~: b)
forall a b. Base a -> Base b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Base a
b1 Base b
b2
  testEquality (TTyWorld TTy t
b1) (TTyWorld TTy t
b2) =
    case TTy t -> TTy t -> Maybe (t :~: t)
forall a b. TTy a -> TTy b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy t
b1 TTy t
b2 of
      Just t :~: t
Refl -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      Maybe (t :~: t)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
  testEquality TTy a
_ TTy b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance PrettyPrec (TTy ty) where
  prettyPrec :: Int -> TTy ty -> Doc ann
  prettyPrec :: forall ann. Int -> TTy ty -> Doc ann
prettyPrec Int
_ (TTyBase Base ty
b) = Base ty -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Base ty
b
  prettyPrec Int
p (TTy a
α :->: TTy b
β) =
    Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
      Int -> TTy a -> Doc ann
forall ann. Int -> TTy a -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
1 TTy a
α Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"->" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> TTy b -> Doc ann
forall ann. Int -> TTy b -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
0 TTy b
β
  prettyPrec Int
p (TTyWorld TTy t
t) =
    Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
      Doc ann
"World" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> TTy t -> Doc ann
forall ann. Int -> TTy t -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
2 TTy t
t

------------------------------------------------------------
-- Instance checking

-- | Check that a particular type has an 'GHC.Classes.Eq' instance, and run a
--   computation in a context provided with an 'GHC.Classes.Eq' constraint. The
--   other @checkX@ functions are similar.
checkEq :: (Has (Throw CheckErr) sig m) => TTy ty -> ((Eq ty, NotFun ty) => m a) -> m a
checkEq :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Eq ty, NotFun ty) => m a) -> m a
checkEq (TTyBase Base ty
BBool) (Eq ty, NotFun ty) => m a
a = m a
(Eq ty, NotFun ty) => m a
a
checkEq (TTyBase Base ty
BInt) (Eq ty, NotFun ty) => m a
a = m a
(Eq ty, NotFun ty) => m a
a
checkEq (TTyBase Base ty
BFloat) (Eq ty, NotFun ty) => m a
a = m a
(Eq ty, NotFun ty) => m a
a
checkEq TTy ty
ty (Eq ty, NotFun ty) => m a
_ = CheckErr -> m a
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m a) -> CheckErr -> m a
forall a b. (a -> b) -> a -> b
$ Text -> TTy ty -> CheckErr
forall a. Text -> TTy a -> CheckErr
NoInstance Text
"Eq" TTy ty
ty

checkOrd :: (Has (Throw CheckErr) sig m) => TTy ty -> ((Ord ty, NotFun ty) => m a) -> m a
checkOrd :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Ord ty, NotFun ty) => m a) -> m a
checkOrd (TTyBase Base ty
BBool) (Ord ty, NotFun ty) => m a
a = m a
(Ord ty, NotFun ty) => m a
a
checkOrd (TTyBase Base ty
BInt) (Ord ty, NotFun ty) => m a
a = m a
(Ord ty, NotFun ty) => m a
a
checkOrd (TTyBase Base ty
BFloat) (Ord ty, NotFun ty) => m a
a = m a
(Ord ty, NotFun ty) => m a
a
checkOrd TTy ty
ty (Ord ty, NotFun ty) => m a
_ = CheckErr -> m a
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m a) -> CheckErr -> m a
forall a b. (a -> b) -> a -> b
$ Text -> TTy ty -> CheckErr
forall a. Text -> TTy a -> CheckErr
NoInstance Text
"Ord" TTy ty
ty

checkNum :: (Has (Throw CheckErr) sig m) => TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum (TTyBase Base ty
BInt) (Num ty, NotFun ty) => m a
a = m a
(Num ty, NotFun ty) => m a
a
checkNum (TTyBase Base ty
BFloat) (Num ty, NotFun ty) => m a
a = m a
(Num ty, NotFun ty) => m a
a
checkNum TTy ty
ty (Num ty, NotFun ty) => m a
_ = CheckErr -> m a
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m a) -> CheckErr -> m a
forall a b. (a -> b) -> a -> b
$ Text -> TTy ty -> CheckErr
forall a. Text -> TTy a -> CheckErr
NoInstance Text
"Num" TTy ty
ty

checkIntegral :: (Has (Throw CheckErr) sig m) => TTy ty -> ((Integral ty, NotFun ty) => m a) -> m a
checkIntegral :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Integral ty, NotFun ty) => m a) -> m a
checkIntegral (TTyBase Base ty
BInt) (Integral ty, NotFun ty) => m a
a = m a
(Integral ty, NotFun ty) => m a
a
checkIntegral TTy ty
ty (Integral ty, NotFun ty) => m a
_ = CheckErr -> m a
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m a) -> CheckErr -> m a
forall a b. (a -> b) -> a -> b
$ Text -> TTy ty -> CheckErr
forall a. Text -> TTy a -> CheckErr
NoInstance Text
"Integral" TTy ty
ty

checkEmpty :: (Has (Throw CheckErr) sig m) => TTy ty -> ((Empty ty, NotFun ty) => m a) -> m a
checkEmpty :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Empty ty, NotFun ty) => m a) -> m a
checkEmpty (TTyBase Base ty
BCell) (Empty ty, NotFun ty) => m a
a = m a
(Empty ty, NotFun ty) => m a
a
checkEmpty TTy ty
ty (Empty ty, NotFun ty) => m a
_ = CheckErr -> m a
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m a) -> CheckErr -> m a
forall a b. (a -> b) -> a -> b
$ Text -> TTy ty -> CheckErr
forall a. Text -> TTy a -> CheckErr
NoInstance Text
"Empty" TTy ty
ty

checkOver :: (Has (Throw CheckErr) sig m) => TTy ty -> ((Over ty, NotFun ty) => m a) -> m a
checkOver :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Over ty, NotFun ty) => m a) -> m a
checkOver (TTyBase Base ty
BBool) (Over ty, NotFun ty) => m a
a = m a
(Over ty, NotFun ty) => m a
a
checkOver (TTyBase Base ty
BInt) (Over ty, NotFun ty) => m a
a = m a
(Over ty, NotFun ty) => m a
a
checkOver (TTyBase Base ty
BFloat) (Over ty, NotFun ty) => m a
a = m a
(Over ty, NotFun ty) => m a
a
checkOver (TTyBase Base ty
BCell) (Over ty, NotFun ty) => m a
a = m a
(Over ty, NotFun ty) => m a
a
checkOver TTy ty
ty (Over ty, NotFun ty) => m a
_ = CheckErr -> m a
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m a) -> CheckErr -> m a
forall a b. (a -> b) -> a -> b
$ Text -> TTy ty -> CheckErr
forall a. Text -> TTy a -> CheckErr
NoInstance Text
"Over" TTy ty
ty

checkNotFun :: (Has (Throw CheckErr) sig m) => TTy ty -> (NotFun ty => m a) -> m a
checkNotFun :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> (NotFun ty => m a) -> m a
checkNotFun (TTyBase Base ty
BBool) NotFun ty => m a
a = m a
NotFun ty => m a
a
checkNotFun (TTyBase Base ty
BInt) NotFun ty => m a
a = m a
NotFun ty => m a
a
checkNotFun (TTyBase Base ty
BFloat) NotFun ty => m a
a = m a
NotFun ty => m a
a
checkNotFun (TTyBase Base ty
BCell) NotFun ty => m a
a = m a
NotFun ty => m a
a
checkNotFun TTy ty
ty NotFun ty => m a
_ = CheckErr -> m a
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m a) -> CheckErr -> m a
forall a b. (a -> b) -> a -> b
$ Text -> TTy ty -> CheckErr
forall a. Text -> TTy a -> CheckErr
NoInstance Text
"NotFun" TTy ty
ty

------------------------------------------------------------
-- Existential wrappers

-- | Wrap up a type-indexed thing to hide the type index, but package
--   it with a 'TTy' which we can pattern-match on to recover the type
--   later.
data Some :: (Type -> Type) -> Type where
  Some :: TTy α -> t α -> Some t

deriving instance (forall α. Show (t α)) => Show (Some t)

mapSome :: (forall α. s α -> t α) -> Some s -> Some t
mapSome :: forall (s :: * -> *) (t :: * -> *).
(forall α. s α -> t α) -> Some s -> Some t
mapSome forall α. s α -> t α
f (Some TTy α
ty s α
t) = TTy α -> t α -> Some t
forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy α
ty (s α -> t α
forall α. s α -> t α
f s α
t)

type SomeTy = Some (F.Const ())

pattern SomeTy :: TTy α -> SomeTy
pattern $mSomeTy :: forall {r}. SomeTy -> (forall {α}. TTy α -> r) -> ((# #) -> r) -> r
$bSomeTy :: forall α. TTy α -> SomeTy
SomeTy α = Some α (F.Const ())
{-# COMPLETE SomeTy #-}

------------------------------------------------------------
-- Type inference/checking + elaboration

type WorldMap = Map Text (Some (TTerm '[]))

-- | Type contexts, indexed by a type-level list of types of all the
--   variables in the context.
data Ctx :: [Type] -> Type where
  CNil :: Ctx '[]
  CCons :: Text -> TTy ty -> Ctx g -> Ctx (ty ': g)

-- | Look up a variable name in the context, returning a type-indexed
--   de Bruijn index.
lookup :: (Has (Throw CheckErr) sig m) => Text -> Ctx g -> m (Some (Idx g))
lookup :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Text -> Ctx g -> m (Some (Idx g))
lookup Text
x Ctx g
CNil = CheckErr -> m (Some (Idx g))
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m (Some (Idx g))) -> CheckErr -> m (Some (Idx g))
forall a b. (a -> b) -> a -> b
$ Text -> CheckErr
Unbound Text
x
lookup Text
x (CCons Text
y TTy ty
ty Ctx g
ctx)
  | Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
y = Some (Idx g) -> m (Some (Idx g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (Idx g) -> m (Some (Idx g)))
-> Some (Idx g) -> m (Some (Idx g))
forall a b. (a -> b) -> a -> b
$ TTy ty -> Idx g ty -> Some (Idx g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy ty
ty Idx g ty
Idx (ty : g) ty
forall ty (a :: [*]). Idx (ty : a) ty
VZ
  | Bool
otherwise = (forall α. Idx g α -> Idx g α) -> Some (Idx g) -> Some (Idx g)
forall (s :: * -> *) (t :: * -> *).
(forall α. s α -> t α) -> Some s -> Some t
mapSome Idx g α -> Idx g α
Idx g α -> Idx (ty : g) α
forall (a :: [*]) ty b. Idx a ty -> Idx (b : a) ty
forall α. Idx g α -> Idx g α
VS (Some (Idx g) -> Some (Idx g))
-> m (Some (Idx g)) -> m (Some (Idx g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Ctx g -> m (Some (Idx g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Text -> Ctx g -> m (Some (Idx g))
lookup Text
x Ctx g
ctx

-- | Check that a term has a given type, and if so, return a
--   corresponding elaborated and type-indexed term.  Note that this
--   also deals with subtyping: for example, if we check that the term
--   @3@ has type @World Int@, we will get back a suitably lifted
--   value (/i.e./ @const 3@).
check ::
  ( Has (Throw CheckErr) sig m
  , Has (Reader TerrainEntityMaps) sig m
  , Has (Reader WorldMap) sig m
  ) =>
  Ctx g ->
  TTy t ->
  WExp ->
  m (TTerm g t)
check :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]) t.
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> TTy t -> WExp -> m (TTerm g t)
check Ctx g
e TTy t
ty WExp
t = do
  Some (TTerm g)
t1 <- Ctx g -> WExp -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> WExp -> m (Some (TTerm g))
infer Ctx g
e WExp
t
  Some TTy α
ty' TTerm g α
t' <- Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
apply (TTy (t -> t) -> TTerm g (t -> t) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy t
ty TTy t -> TTy t -> TTy (t -> t)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy t
ty) (Const (t -> t) -> TTerm g (t -> t)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (t -> t)
forall a. Const (a -> a)
I)) Some (TTerm g)
t1
  case TTy t -> TTy α -> Maybe (t :~: α)
forall a b. TTy a -> TTy b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy t
ty TTy α
ty' of
    Maybe (t :~: α)
Nothing -> CheckErr -> m (TTerm g t)
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m (TTerm g t)) -> CheckErr -> m (TTerm g t)
forall a b. (a -> b) -> a -> b
$ Some (TTerm g) -> TTy t -> CheckErr
forall (a :: [*]) b. Some (TTerm a) -> TTy b -> CheckErr
BadType Some (TTerm g)
t1 TTy t
ty
    Just t :~: α
Refl -> TTerm g t -> m (TTerm g t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm g t
TTerm g α
t'

-- | Get the underlying base type of a term which either has a base
--   type or a World type.
getBaseType :: Some (TTerm g) -> SomeTy
getBaseType :: forall (g :: [*]). Some (TTerm g) -> SomeTy
getBaseType (Some (TTyWorld TTy t
ty) TTerm g α
_) = TTy t -> SomeTy
forall α. TTy α -> SomeTy
SomeTy TTy t
ty
getBaseType (Some TTy α
ty TTerm g α
_) = TTy α -> SomeTy
forall α. TTy α -> SomeTy
SomeTy TTy α
ty

-- | Apply one term to another term, automatically handling promotion
--   and lifting, via the fact that World is Applicative.  That is,
--   (1) if a term of type T is used where a term of type World T is
--   expected, it will automatically be promoted (by an application of
--   const); (2) if a function of type (T1 -> T2 -> ... -> Tn) is
--   applied to any arguments of type (World Ti), the function will be
--   lifted to (World T1 -> World T2 -> ... -> World Tn).
apply :: (Has (Throw CheckErr) sig m) => Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
-- Normal function application
apply :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
apply (Some (TTy a
ty11 :->: TTy b
ty12) TTerm g α
t1) (Some TTy α
ty2 TTerm g α
t2)
  | Just a :~: α
Refl <- TTy a -> TTy α -> Maybe (a :~: α)
forall a b. TTy a -> TTy b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy a
ty11 TTy α
ty2 = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy b -> TTerm g b -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy b
ty12 (TTerm g α
TTerm g (α -> b)
t1 TTerm g (α -> b) -> TTerm g α -> TTerm g b
forall a b. TTerm g (a -> b) -> TTerm g a -> TTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ TTerm g α
t2)
-- (World T -> ...) applied to T: promote the argument to (World T) with const
apply (Some (TTyWorld TTy t
ty11 :->: TTy b
ty12) TTerm g α
t1) (Some TTy α
ty2 TTerm g α
t2)
  | Just t :~: α
Refl <- TTy t -> TTy α -> Maybe (t :~: α)
forall a b. TTy a -> TTy b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy t
ty11 TTy α
ty2 = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy b -> TTerm g b -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy b
ty12 (TTerm g α
TTerm g ((Coords -> α) -> b)
t1 TTerm g ((Coords -> α) -> b) -> TTerm g (Coords -> α) -> TTerm g b
forall a b. TTerm g (a -> b) -> TTerm g a -> TTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ (Const (α -> Coords -> α)
forall a b. Const (a -> b -> a)
K Const (α -> Coords -> α) -> TTerm g α -> TTerm g (Coords -> α)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ TTerm g α
t2))
-- (S -> T) applied to (World S): lift the function to (World S -> World T).
apply (Some (TTy a
ty11 :->: TTy b
ty12) TTerm g α
t1) (Some (TTyWorld TTy t
ty2) TTerm g α
t2)
  | Just a :~: t
Refl <- TTy a -> TTy t -> Maybe (a :~: t)
forall a b. TTy a -> TTy b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy a
ty11 TTy t
ty2 = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (World b) -> TTerm g (World b) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy b -> TTy (World b)
forall a. TTy a -> TTy (World a)
TTyWorld TTy b
ty12) (Const ((a -> b) -> (Coords -> a) -> World b)
forall a b c. Const ((a -> b) -> (c -> a) -> c -> b)
B Const ((a -> b) -> (Coords -> a) -> World b)
-> TTerm g (a -> b) -> TTerm g ((Coords -> a) -> World b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ TTerm g α
TTerm g (a -> b)
t1 TTerm g ((Coords -> a) -> World b)
-> TTerm g (Coords -> a) -> TTerm g (World b)
forall a b. TTerm g (a -> b) -> TTerm g a -> TTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ TTerm g α
TTerm g (Coords -> a)
t2)
-- World (S -> T) applied to S.  Note this case and the next are
-- needed because in the previous case, when (S -> T) is lifted to
-- (World S -> World T), T may itself be a function type.
apply (Some (TTyWorld (TTy a
ty11 :->: TTy b
ty12)) TTerm g α
t1) (Some TTy α
ty2 TTerm g α
t2)
  | Just a :~: α
Refl <- TTy a -> TTy α -> Maybe (a :~: α)
forall a b. TTy a -> TTy b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy a
ty11 TTy α
ty2 = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (World b) -> TTerm g (World b) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy b -> TTy (World b)
forall a. TTy a -> TTy (World a)
TTyWorld TTy b
ty12) (Const ((Coords -> α -> b) -> (Coords -> α) -> World b)
forall a b c. Const ((a -> b -> c) -> (a -> b) -> a -> c)
S Const ((Coords -> α -> b) -> (Coords -> α) -> World b)
-> TTerm g (Coords -> α -> b) -> TTerm g ((Coords -> α) -> World b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ TTerm g α
TTerm g (Coords -> α -> b)
t1 TTerm g ((Coords -> α) -> World b)
-> TTerm g (Coords -> α) -> TTerm g (World b)
forall a b. TTerm g (a -> b) -> TTerm g a -> TTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ (Const (α -> Coords -> α)
forall a b. Const (a -> b -> a)
K Const (α -> Coords -> α) -> TTerm g α -> TTerm g (Coords -> α)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ TTerm g α
t2))
-- World (S -> T) applied to (World S)
apply (Some (TTyWorld (TTy a
ty11 :->: TTy b
ty12)) TTerm g α
t1) (Some (TTyWorld TTy t
ty2) TTerm g α
t2)
  | Just a :~: t
Refl <- TTy a -> TTy t -> Maybe (a :~: t)
forall a b. TTy a -> TTy b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy a
ty11 TTy t
ty2 = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (World b) -> TTerm g (World b) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy b -> TTy (World b)
forall a. TTy a -> TTy (World a)
TTyWorld TTy b
ty12) (Const ((Coords -> a -> b) -> (Coords -> a) -> World b)
forall a b c. Const ((a -> b -> c) -> (a -> b) -> a -> c)
S Const ((Coords -> a -> b) -> (Coords -> a) -> World b)
-> TTerm g (Coords -> a -> b) -> TTerm g ((Coords -> a) -> World b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ TTerm g α
TTerm g (Coords -> a -> b)
t1 TTerm g ((Coords -> a) -> World b)
-> TTerm g (Coords -> a) -> TTerm g (World b)
forall a b. TTerm g (a -> b) -> TTerm g a -> TTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ TTerm g α
TTerm g (Coords -> a)
t2)
apply Some (TTerm g)
t1 Some (TTerm g)
t2 = CheckErr -> m (Some (TTerm g))
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m (Some (TTerm g))) -> CheckErr -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ Some (TTerm g) -> Some (TTerm g) -> CheckErr
forall (a :: [*]). Some (TTerm a) -> Some (TTerm a) -> CheckErr
ApplyErr Some (TTerm g)
t1 Some (TTerm g)
t2

applyTo :: (Has (Throw CheckErr) sig m) => Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
applyTo :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
applyTo = (Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
forall a b c. (a -> b -> c) -> b -> a -> c
flip Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
apply

-- | Infer the type of an operator: turn a raw operator into a
--   type-indexed constant.  However, some operators are polymorphic,
--   so we also provide a list of type arguments.  For example, the
--   type of the negation operator can be either (Int -> Int) or
--   (Float -> Float) so we provide it as an argument.
--
--   Currently, all operators take at most one type argument, so
--   (Maybe SomeTy) might seem more appropriate than [SomeTy], but
--   that is just a coincidence; in general one can easily imagine
--   operators that are polymorphic in more than one type variable,
--   and we may wish to add such in the future.
inferOp :: (Has (Throw CheckErr) sig m) => [SomeTy] -> Op -> m (Some (TTerm g))
inferOp :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
[SomeTy] -> Op -> m (Some (TTerm g))
inferOp [SomeTy]
_ Op
Not = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (Bool -> Bool) -> TTerm g (Bool -> Bool) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Bool
TTyBool TTy Bool -> TTy Bool -> TTy (Bool -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (Const (Bool -> Bool) -> TTerm g (Bool -> Bool)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Bool -> Bool)
CNot)
inferOp [SomeTy TTy α
tyA] Op
Neg = TTy (α -> α) -> TTerm g (α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (TTerm g (α -> α) -> Some (TTerm g))
-> m (TTerm g (α -> α)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Num α, NotFun α) => m (TTerm g (α -> α)))
-> m (TTerm g (α -> α))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum TTy α
tyA (TTerm g (α -> α) -> m (TTerm g (α -> α))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α) -> m (TTerm g (α -> α)))
-> TTerm g (α -> α) -> m (TTerm g (α -> α))
forall a b. (a -> b) -> a -> b
$ Const (α -> α) -> TTerm g (α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α)
forall a. (Num a, NotFun a) => Const (a -> a)
CNeg)
inferOp [SomeTy]
_ Op
And = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (Bool -> Bool -> Bool)
-> TTerm g (Bool -> Bool -> Bool) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Bool
TTyBool TTy Bool -> TTy (Bool -> Bool) -> TTy (Bool -> Bool -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool TTy Bool -> TTy Bool -> TTy (Bool -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (Const (Bool -> Bool -> Bool) -> TTerm g (Bool -> Bool -> Bool)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Bool -> Bool -> Bool)
CAnd)
inferOp [SomeTy]
_ Op
Or = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (Bool -> Bool -> Bool)
-> TTerm g (Bool -> Bool -> Bool) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Bool
TTyBool TTy Bool -> TTy (Bool -> Bool) -> TTy (Bool -> Bool -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool TTy Bool -> TTy Bool -> TTy (Bool -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (Const (Bool -> Bool -> Bool) -> TTerm g (Bool -> Bool -> Bool)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Bool -> Bool -> Bool)
COr)
inferOp [SomeTy TTy α
tyA] Op
Abs = TTy (α -> α) -> TTerm g (α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (TTerm g (α -> α) -> Some (TTerm g))
-> m (TTerm g (α -> α)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Num α, NotFun α) => m (TTerm g (α -> α)))
-> m (TTerm g (α -> α))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum TTy α
tyA (TTerm g (α -> α) -> m (TTerm g (α -> α))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α) -> m (TTerm g (α -> α)))
-> TTerm g (α -> α) -> m (TTerm g (α -> α))
forall a b. (a -> b) -> a -> b
$ Const (α -> α) -> TTerm g (α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α)
forall a. (Num a, NotFun a) => Const (a -> a)
CAbs)
inferOp [SomeTy TTy α
tyA] Op
Add = TTy (α -> α -> α) -> TTerm g (α -> α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> α) -> TTy (α -> α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (TTerm g (α -> α -> α) -> Some (TTerm g))
-> m (TTerm g (α -> α -> α)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Num α, NotFun α) => m (TTerm g (α -> α -> α)))
-> m (TTerm g (α -> α -> α))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum TTy α
tyA (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α)))
-> TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> α) -> TTerm g (α -> α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> α)
forall a. (Num a, NotFun a) => Const (a -> a -> a)
CAdd)
inferOp [SomeTy TTy α
tyA] Op
Sub = TTy (α -> α -> α) -> TTerm g (α -> α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> α) -> TTy (α -> α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (TTerm g (α -> α -> α) -> Some (TTerm g))
-> m (TTerm g (α -> α -> α)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Num α, NotFun α) => m (TTerm g (α -> α -> α)))
-> m (TTerm g (α -> α -> α))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum TTy α
tyA (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α)))
-> TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> α) -> TTerm g (α -> α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> α)
forall a. (Num a, NotFun a) => Const (a -> a -> a)
CSub)
inferOp [SomeTy TTy α
tyA] Op
Mul = TTy (α -> α -> α) -> TTerm g (α -> α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> α) -> TTy (α -> α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (TTerm g (α -> α -> α) -> Some (TTerm g))
-> m (TTerm g (α -> α -> α)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Num α, NotFun α) => m (TTerm g (α -> α -> α)))
-> m (TTerm g (α -> α -> α))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum TTy α
tyA (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α)))
-> TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> α) -> TTerm g (α -> α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> α)
forall a. (Num a, NotFun a) => Const (a -> a -> a)
CMul)
inferOp [SomeTy TTy α
tyA] Op
Div = case TTy α
tyA of
  TTyBase Base α
BInt -> Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (α -> α -> α) -> TTerm g (α -> α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> α) -> TTy (α -> α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (Const (α -> α -> α) -> TTerm g (α -> α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> α)
forall a. (Integral a, NotFun a) => Const (a -> a -> a)
CIDiv)
  TTyBase Base α
BFloat -> Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (α -> α -> α) -> TTerm g (α -> α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> α) -> TTy (α -> α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (Const (α -> α -> α) -> TTerm g (α -> α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> α)
forall a. (Fractional a, NotFun a) => Const (a -> a -> a)
CDiv)
  TTy α
_ -> CheckErr -> m (Some (TTerm g))
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m (Some (TTerm g))) -> CheckErr -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy α -> CheckErr
forall a. TTy a -> CheckErr
BadDivType TTy α
tyA
inferOp [SomeTy TTy α
tyA] Op
Mod = TTy (α -> α -> α) -> TTerm g (α -> α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> α) -> TTy (α -> α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (TTerm g (α -> α -> α) -> Some (TTerm g))
-> m (TTerm g (α -> α -> α)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Integral α, NotFun α) => m (TTerm g (α -> α -> α)))
-> m (TTerm g (α -> α -> α))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Integral ty, NotFun ty) => m a) -> m a
checkIntegral TTy α
tyA (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α)))
-> TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> α) -> TTerm g (α -> α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> α)
forall a. (Integral a, NotFun a) => Const (a -> a -> a)
CMod)
inferOp [SomeTy TTy α
tyA] Op
Eq = TTy (α -> α -> Bool) -> TTerm g (α -> α -> Bool) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> Bool) -> TTy (α -> α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy Bool -> TTy (α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (TTerm g (α -> α -> Bool) -> Some (TTerm g))
-> m (TTerm g (α -> α -> Bool)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Eq α, NotFun α) => m (TTerm g (α -> α -> Bool)))
-> m (TTerm g (α -> α -> Bool))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Eq ty, NotFun ty) => m a) -> m a
checkEq TTy α
tyA (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool)))
-> TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> Bool) -> TTerm g (α -> α -> Bool)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> Bool)
forall a. (Eq a, NotFun a) => Const (a -> a -> Bool)
CEq)
inferOp [SomeTy TTy α
tyA] Op
Neq = TTy (α -> α -> Bool) -> TTerm g (α -> α -> Bool) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> Bool) -> TTy (α -> α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy Bool -> TTy (α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (TTerm g (α -> α -> Bool) -> Some (TTerm g))
-> m (TTerm g (α -> α -> Bool)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Eq α, NotFun α) => m (TTerm g (α -> α -> Bool)))
-> m (TTerm g (α -> α -> Bool))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Eq ty, NotFun ty) => m a) -> m a
checkEq TTy α
tyA (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool)))
-> TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> Bool) -> TTerm g (α -> α -> Bool)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> Bool)
forall a. (Eq a, NotFun a) => Const (a -> a -> Bool)
CNeq)
inferOp [SomeTy TTy α
tyA] Op
Lt = TTy (α -> α -> Bool) -> TTerm g (α -> α -> Bool) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> Bool) -> TTy (α -> α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy Bool -> TTy (α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (TTerm g (α -> α -> Bool) -> Some (TTerm g))
-> m (TTerm g (α -> α -> Bool)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Ord α, NotFun α) => m (TTerm g (α -> α -> Bool)))
-> m (TTerm g (α -> α -> Bool))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Ord ty, NotFun ty) => m a) -> m a
checkOrd TTy α
tyA (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool)))
-> TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> Bool) -> TTerm g (α -> α -> Bool)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> Bool)
forall a. (Ord a, NotFun a) => Const (a -> a -> Bool)
CLt)
inferOp [SomeTy TTy α
tyA] Op
Leq = TTy (α -> α -> Bool) -> TTerm g (α -> α -> Bool) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> Bool) -> TTy (α -> α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy Bool -> TTy (α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (TTerm g (α -> α -> Bool) -> Some (TTerm g))
-> m (TTerm g (α -> α -> Bool)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Ord α, NotFun α) => m (TTerm g (α -> α -> Bool)))
-> m (TTerm g (α -> α -> Bool))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Ord ty, NotFun ty) => m a) -> m a
checkOrd TTy α
tyA (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool)))
-> TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> Bool) -> TTerm g (α -> α -> Bool)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> Bool)
forall a. (Ord a, NotFun a) => Const (a -> a -> Bool)
CLeq)
inferOp [SomeTy TTy α
tyA] Op
Gt = TTy (α -> α -> Bool) -> TTerm g (α -> α -> Bool) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> Bool) -> TTy (α -> α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy Bool -> TTy (α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (TTerm g (α -> α -> Bool) -> Some (TTerm g))
-> m (TTerm g (α -> α -> Bool)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Ord α, NotFun α) => m (TTerm g (α -> α -> Bool)))
-> m (TTerm g (α -> α -> Bool))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Ord ty, NotFun ty) => m a) -> m a
checkOrd TTy α
tyA (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool)))
-> TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> Bool) -> TTerm g (α -> α -> Bool)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> Bool)
forall a. (Ord a, NotFun a) => Const (a -> a -> Bool)
CGt)
inferOp [SomeTy TTy α
tyA] Op
Geq = TTy (α -> α -> Bool) -> TTerm g (α -> α -> Bool) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> Bool) -> TTy (α -> α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy Bool -> TTy (α -> Bool)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (TTerm g (α -> α -> Bool) -> Some (TTerm g))
-> m (TTerm g (α -> α -> Bool)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Ord α, NotFun α) => m (TTerm g (α -> α -> Bool)))
-> m (TTerm g (α -> α -> Bool))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Ord ty, NotFun ty) => m a) -> m a
checkOrd TTy α
tyA (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool)))
-> TTerm g (α -> α -> Bool) -> m (TTerm g (α -> α -> Bool))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> Bool) -> TTerm g (α -> α -> Bool)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> Bool)
forall a. (Ord a, NotFun a) => Const (a -> a -> Bool)
CGeq)
inferOp [SomeTy TTy α
tyA] Op
If = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (Bool -> α -> α -> α)
-> TTerm g (Bool -> α -> α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Bool
TTyBool TTy Bool -> TTy (α -> α -> α) -> TTy (Bool -> α -> α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy (α -> α) -> TTy (α -> α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (Const (Bool -> α -> α -> α) -> TTerm g (Bool -> α -> α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Bool -> α -> α -> α)
forall a. Const (Bool -> a -> a -> a)
CIf)
inferOp [SomeTy]
_ Op
Perlin = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (Integer -> Integer -> Double -> Double -> World Double)
-> TTerm g (Integer -> Integer -> Double -> Double -> World Double)
-> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Integer
TTyInt TTy Integer
-> TTy (Integer -> Double -> Double -> World Double)
-> TTy (Integer -> Integer -> Double -> Double -> World Double)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Integer
TTyInt TTy Integer
-> TTy (Double -> Double -> World Double)
-> TTy (Integer -> Double -> Double -> World Double)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Double
TTyFloat TTy Double
-> TTy (Double -> World Double)
-> TTy (Double -> Double -> World Double)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Double
TTyFloat TTy Double -> TTy (World Double) -> TTy (Double -> World Double)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Double -> TTy (World Double)
forall a. TTy a -> TTy (World a)
TTyWorld TTy Double
TTyFloat) (Const (Integer -> Integer -> Double -> Double -> World Double)
-> TTerm g (Integer -> Integer -> Double -> Double -> World Double)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Integer -> Integer -> Double -> Double -> World Double)
CPerlin)
inferOp [SomeTy TTy α
tyA] Op
Mask = TTy (World Bool -> World α -> World α)
-> TTerm g (World Bool -> World α -> World α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Bool -> TTy (World Bool)
forall a. TTy a -> TTy (World a)
TTyWorld TTy Bool
TTyBool TTy (World Bool)
-> TTy (World α -> World α)
-> TTy (World Bool -> World α -> World α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α -> TTy (World α)
forall a. TTy a -> TTy (World a)
TTyWorld TTy α
tyA TTy (World α) -> TTy (World α) -> TTy (World α -> World α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α -> TTy (World α)
forall a. TTy a -> TTy (World a)
TTyWorld TTy α
tyA) (TTerm g (World Bool -> World α -> World α) -> Some (TTerm g))
-> m (TTerm g (World Bool -> World α -> World α))
-> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Empty α, NotFun α) =>
    m (TTerm g (World Bool -> World α -> World α)))
-> m (TTerm g (World Bool -> World α -> World α))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Empty ty, NotFun ty) => m a) -> m a
checkEmpty TTy α
tyA (TTerm g (World Bool -> World α -> World α)
-> m (TTerm g (World Bool -> World α -> World α))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (World Bool -> World α -> World α)
 -> m (TTerm g (World Bool -> World α -> World α)))
-> TTerm g (World Bool -> World α -> World α)
-> m (TTerm g (World Bool -> World α -> World α))
forall a b. (a -> b) -> a -> b
$ Const (World Bool -> World α -> World α)
-> TTerm g (World Bool -> World α -> World α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (World Bool -> World α -> World α)
forall a.
(Empty a, NotFun a) =>
Const (World Bool -> World a -> World a)
CMask)
inferOp [SomeTy TTy α
tyA] Op
Overlay = TTy (α -> α -> α) -> TTerm g (α -> α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA TTy α -> TTy (α -> α) -> TTy (α -> α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (TTerm g (α -> α -> α) -> Some (TTerm g))
-> m (TTerm g (α -> α -> α)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> ((Over α, NotFun α) => m (TTerm g (α -> α -> α)))
-> m (TTerm g (α -> α -> α))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Over ty, NotFun ty) => m a) -> m a
checkOver TTy α
tyA (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α)))
-> TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> α) -> TTerm g (α -> α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> α)
forall a. (Over a, NotFun a) => Const (a -> a -> a)
COver)
inferOp [SomeTy TTy α
tyA] Op
IMap = TTy
  ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α)
-> TTerm
     g
     ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α)
-> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Integer -> TTy (Coords -> Integer)
forall a. TTy a -> TTy (World a)
TTyWorld TTy Integer
TTyInt TTy (Coords -> Integer)
-> TTy ((Coords -> Integer) -> World α -> World α)
-> TTy
     ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Integer -> TTy (Coords -> Integer)
forall a. TTy a -> TTy (World a)
TTyWorld TTy Integer
TTyInt TTy (Coords -> Integer)
-> TTy (World α -> World α)
-> TTy ((Coords -> Integer) -> World α -> World α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α -> TTy (World α)
forall a. TTy a -> TTy (World a)
TTyWorld TTy α
tyA TTy (World α) -> TTy (World α) -> TTy (World α -> World α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α -> TTy (World α)
forall a. TTy a -> TTy (World a)
TTyWorld TTy α
tyA) (TTerm
   g
   ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α)
 -> Some (TTerm g))
-> m (TTerm
        g
        ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α))
-> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTy α
-> (NotFun α =>
    m (TTerm
         g
         ((Coords -> Integer)
          -> (Coords -> Integer) -> World α -> World α)))
-> m (TTerm
        g
        ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> (NotFun ty => m a) -> m a
checkNotFun TTy α
tyA (TTerm
  g
  ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α)
-> m (TTerm
        g
        ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm
   g
   ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α)
 -> m (TTerm
         g
         ((Coords -> Integer)
          -> (Coords -> Integer) -> World α -> World α)))
-> TTerm
     g
     ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α)
-> m (TTerm
        g
        ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α))
forall a b. (a -> b) -> a -> b
$ Const
  ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α)
-> TTerm
     g
     ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const
  ((Coords -> Integer) -> (Coords -> Integer) -> World α -> World α)
forall a.
NotFun a =>
Const
  ((Coords -> Integer) -> (Coords -> Integer) -> World a -> World a)
CIMap)
-- In theory, this last case should never happen.
inferOp [SomeTy]
tys Op
op = CheckErr -> m (Some (TTerm g))
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m (Some (TTerm g))) -> CheckErr -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ [SomeTy] -> Op -> CheckErr
BadInferOp [SomeTy]
tys Op
op

-- | Given a raw operator and the terms the operator is applied to,
--   select which types should be supplied as the type arguments to
--   the operator.  For example, for an operator like @+@ we can just
--   select the type of its first argument; for an operator like @if@,
--   we must select the type of its second argument, since @if : Bool
--   -> a -> a -> a@.  In all cases we must also select the underlying
--   base type in case the argument has a @World@ type.  For example
--   if @+@ is applied to an argument of type @World Int@ we still
--   want to give @+@ the type @Int -> Int -> Int@.  It can be lifted
--   to have type @World Int -> World Int -> World Int@ but that will
--   be taken care of by application, which will insert the right
--   combinators to do the lifting.
typeArgsFor :: Op -> [Some (TTerm g)] -> [SomeTy]
typeArgsFor :: forall (g :: [*]). Op -> [Some (TTerm g)] -> [SomeTy]
typeArgsFor Op
op (Some (TTerm g)
t : [Some (TTerm g)]
_)
  | Op
op Op -> [Op] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Op
Neg, Op
Abs, Op
Add, Op
Sub, Op
Mul, Op
Div, Op
Mod, Op
Eq, Op
Neq, Op
Lt, Op
Leq, Op
Gt, Op
Geq] = [Some (TTerm g) -> SomeTy
forall (g :: [*]). Some (TTerm g) -> SomeTy
getBaseType Some (TTerm g)
t]
typeArgsFor Op
op (Some (TTerm g)
_ : Some (TTerm g)
t : [Some (TTerm g)]
_)
  | Op
op Op -> [Op] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Op
If, Op
Mask, Op
Overlay] = [Some (TTerm g) -> SomeTy
forall (g :: [*]). Some (TTerm g) -> SomeTy
getBaseType Some (TTerm g)
t]
typeArgsFor Op
IMap (Some (TTerm g)
_ : Some (TTerm g)
_ : Some (TTerm g)
t : [Some (TTerm g)]
_) = [Some (TTerm g) -> SomeTy
forall (g :: [*]). Some (TTerm g) -> SomeTy
getBaseType Some (TTerm g)
t]
typeArgsFor Op
_ [Some (TTerm g)]
_ = []

-- | Typecheck the application of an operator to some terms, returning
--   a typed, elaborated version of the application.
applyOp ::
  ( Has (Throw CheckErr) sig m
  , Has (Reader TerrainEntityMaps) sig m
  , Has (Reader WorldMap) sig m
  ) =>
  Ctx g ->
  Op ->
  [WExp] ->
  m (Some (TTerm g))
applyOp :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> Op -> [WExp] -> m (Some (TTerm g))
applyOp Ctx g
ctx Op
op [WExp]
ts = do
  [Some (TTerm g)]
tts <- (WExp -> m (Some (TTerm g))) -> [WExp] -> m [Some (TTerm g)]
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 (Ctx g -> WExp -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> WExp -> m (Some (TTerm g))
infer Ctx g
ctx) [WExp]
ts
  (m (Some (TTerm g)) -> Some (TTerm g) -> m (Some (TTerm g)))
-> m (Some (TTerm g)) -> [Some (TTerm g)] -> m (Some (TTerm g))
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\m (Some (TTerm g))
r -> (m (Some (TTerm g))
r m (Some (TTerm g))
-> (Some (TTerm g) -> m (Some (TTerm g))) -> m (Some (TTerm g))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=) ((Some (TTerm g) -> m (Some (TTerm g))) -> m (Some (TTerm g)))
-> (Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g)
-> m (Some (TTerm g))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
applyTo) ([SomeTy] -> Op -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
[SomeTy] -> Op -> m (Some (TTerm g))
inferOp (Op -> [Some (TTerm g)] -> [SomeTy]
forall (g :: [*]). Op -> [Some (TTerm g)] -> [SomeTy]
typeArgsFor Op
op [Some (TTerm g)]
tts) Op
op) [Some (TTerm g)]
tts

-- | Infer the type of a term, and elaborate along the way.
infer ::
  forall sig m g.
  ( Has (Throw CheckErr) sig m
  , Has (Reader TerrainEntityMaps) sig m
  , Has (Reader WorldMap) sig m
  ) =>
  Ctx g ->
  WExp ->
  m (Some (TTerm g))
infer :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> WExp -> m (Some (TTerm g))
infer Ctx g
_ (WInt Integer
i) = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy Integer -> TTerm g Integer -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (Base Integer -> TTy Integer
forall t. Base t -> TTy t
TTyBase Base Integer
BInt) (Const Integer -> TTerm g Integer
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (Integer -> Const Integer
forall a. (Show a, NotFun a) => a -> Const a
CLit Integer
i))
infer Ctx g
_ (WFloat Double
f) = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy Double -> TTerm g Double -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (Base Double -> TTy Double
forall t. Base t -> TTy t
TTyBase Base Double
BFloat) (Const Double -> TTerm g Double
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (Double -> Const Double
forall a. (Show a, NotFun a) => a -> Const a
CLit Double
f))
infer Ctx g
_ (WBool Bool
b) = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy Bool -> TTerm g Bool -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (Base Bool -> TTy Bool
forall t. Base t -> TTy t
TTyBase Base Bool
BBool) (Const Bool -> TTerm g Bool
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (Bool -> Const Bool
forall a. (Show a, NotFun a) => a -> Const a
CLit Bool
b))
infer Ctx g
_ (WCell RawCellVal
c) = do
  CellVal
c' <- RawCellVal -> m CellVal
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Throw CheckErr) sig m,
 Has (Reader TerrainEntityMaps) sig m) =>
RawCellVal -> m CellVal
resolveCell RawCellVal
c
  Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy CellVal -> TTerm g CellVal -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy CellVal
TTyCell (Const CellVal -> TTerm g CellVal
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (CellVal -> Const CellVal
CCell CellVal
c'))
infer Ctx g
ctx (WVar Text
x) = (forall α. Idx g α -> TTerm g α) -> Some (Idx g) -> Some (TTerm g)
forall (s :: * -> *) (t :: * -> *).
(forall α. s α -> t α) -> Some s -> Some t
mapSome Idx g α -> TTerm g α
forall (g :: [*]) a. Idx g a -> TTerm g a
forall α. Idx g α -> TTerm g α
TVar (Some (Idx g) -> Some (TTerm g))
-> m (Some (Idx g)) -> m (Some (TTerm g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Ctx g -> m (Some (Idx g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Text -> Ctx g -> m (Some (Idx g))
lookup Text
x Ctx g
ctx
infer Ctx g
ctx (WOp Op
op [WExp]
ts) = Ctx g -> Op -> [WExp] -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> Op -> [WExp] -> m (Some (TTerm g))
applyOp Ctx g
ctx Op
op [WExp]
ts
infer Ctx g
_ WExp
WSeed = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy Integer -> TTerm g Integer -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy Integer
TTyInt (Const Integer -> TTerm g Integer
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const Integer
CSeed)
infer Ctx g
_ (WCoord Axis
ax) = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (Coords -> Integer)
-> TTerm g (Coords -> Integer) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Integer -> TTy (Coords -> Integer)
forall a. TTy a -> TTy (World a)
TTyWorld TTy Integer
TTyInt) (Const (Coords -> Integer) -> TTerm g (Coords -> Integer)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (Axis -> Const (Coords -> Integer)
CCoord Axis
ax))
infer Ctx g
_ WExp
WHash = Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (TTerm g) -> m (Some (TTerm g)))
-> Some (TTerm g) -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ TTy (Coords -> Integer)
-> TTerm g (Coords -> Integer) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Integer -> TTy (Coords -> Integer)
forall a. TTy a -> TTy (World a)
TTyWorld TTy Integer
TTyInt) (Const (Coords -> Integer) -> TTerm g (Coords -> Integer)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Coords -> Integer)
CHash)
infer Ctx g
ctx (WLet [(Text, WExp)]
defs WExp
body) = Ctx g -> [(Text, WExp)] -> WExp -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> [(Text, WExp)] -> WExp -> m (Some (TTerm g))
inferLet Ctx g
ctx [(Text, WExp)]
defs WExp
body
infer Ctx g
ctx (WOverlay NonEmpty WExp
ts) = Ctx g -> NonEmpty WExp -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> NonEmpty WExp -> m (Some (TTerm g))
inferOverlay Ctx g
ctx NonEmpty WExp
ts
infer Ctx g
_ctx (WImport Text
key) = do
  WorldMap
worldMap <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @WorldMap
  case Text -> WorldMap -> Maybe (Some (TTerm '[]))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
key WorldMap
worldMap of
    Just (Some TTy α
ty TTerm '[] α
t) -> Some (TTerm g) -> m (Some (TTerm g))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTy α -> TTerm g α -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy α
ty (forall (h :: [*]) (g :: [*]) a. TTerm g a -> TTerm (Append g h) a
weaken @g TTerm '[] α
t))
    Maybe (Some (TTerm '[]))
Nothing -> CheckErr -> m (Some (TTerm g))
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m (Some (TTerm g))) -> CheckErr -> m (Some (TTerm g))
forall a b. (a -> b) -> a -> b
$ Text -> CheckErr
UnknownImport Text
key

-- | Try to resolve a 'RawCellVal'---containing only 'Text' names for
--   terrain, entities, and robots---into a real 'CellVal' with
--   references to actual terrain, entities, and robots.
resolveCell ::
  ( Has (Throw CheckErr) sig m
  , Has (Reader TerrainEntityMaps) sig m
  ) =>
  RawCellVal ->
  m CellVal
resolveCell :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Throw CheckErr) sig m,
 Has (Reader TerrainEntityMaps) sig m) =>
RawCellVal -> m CellVal
resolveCell RawCellVal
items = do
  [CellVal]
cellVals <- ((Maybe CellTag, Text) -> m CellVal) -> RawCellVal -> m [CellVal]
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 (Maybe CellTag, Text) -> m CellVal
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Throw CheckErr) sig m,
 Has (Reader TerrainEntityMaps) sig m) =>
(Maybe CellTag, Text) -> m CellVal
resolveCellItem RawCellVal
items
  CellVal -> m CellVal
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CellVal -> m CellVal) -> CellVal -> m CellVal
forall a b. (a -> b) -> a -> b
$ (CellVal -> CellVal -> CellVal) -> CellVal -> [CellVal] -> CellVal
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' CellVal -> CellVal -> CellVal
forall m. Over m => m -> m -> m
(<!>) CellVal
forall e. Empty e => e
empty [CellVal]
cellVals

-- | Try to resolve one cell item name into an actual item (terrain,
-- entity, robot, etc.).
resolveCellItem ::
  forall sig m.
  ( Has (Throw CheckErr) sig m
  , Has (Reader TerrainEntityMaps) sig m
  ) =>
  (Maybe CellTag, Text) ->
  m CellVal
resolveCellItem :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Throw CheckErr) sig m,
 Has (Reader TerrainEntityMaps) sig m) =>
(Maybe CellTag, Text) -> m CellVal
resolveCellItem (Maybe CellTag
mCellTag, Text
item) = case Maybe CellTag
mCellTag of
  Just CellTag
cellTag -> do
    -- The item was tagged specifically, like {terrain: dirt} or {entity: water}
    Maybe CellVal
mCell <- CellTag -> Text -> m (Maybe CellVal)
resolverByTag CellTag
cellTag Text
item
    m CellVal -> (CellVal -> m CellVal) -> Maybe CellVal -> m CellVal
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (CheckErr -> m CellVal
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m CellVal) -> CheckErr -> m CellVal
forall a b. (a -> b) -> a -> b
$ Text -> CellTag -> CheckErr
NotAThing Text
item CellTag
cellTag) CellVal -> m CellVal
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe CellVal
mCell
  Maybe CellTag
Nothing -> do
    -- The item was not tagged; try resolving in all possible ways and choose
    -- the first that works
    [Maybe CellVal]
maybeCells <- (CellTag -> m (Maybe CellVal)) -> [CellTag] -> m [Maybe CellVal]
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 (CellTag -> Text -> m (Maybe CellVal)
`resolverByTag` Text
item) (forall a. (Enum a, Bounded a) => [a]
enumerate @CellTag)
    case [Maybe CellVal] -> Maybe CellVal
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
F.asum [Maybe CellVal]
maybeCells of
      Maybe CellVal
Nothing -> CheckErr -> m CellVal
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (CheckErr -> m CellVal) -> CheckErr -> m CellVal
forall a b. (a -> b) -> a -> b
$ Text -> CheckErr
NotAnything Text
item
      Just CellVal
cell -> CellVal -> m CellVal
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return CellVal
cell
 where
  mkTerrain :: TerrainType -> CellVal
mkTerrain TerrainType
t = TerrainType -> Erasable (Last Entity) -> [TRobot] -> CellVal
CellVal TerrainType
t Erasable (Last Entity)
forall a. Monoid a => a
mempty [TRobot]
forall a. Monoid a => a
mempty
  mkEntity :: Entity -> CellVal
mkEntity Entity
e = TerrainType -> Erasable (Last Entity) -> [TRobot] -> CellVal
CellVal TerrainType
forall a. Monoid a => a
mempty (Last Entity -> Erasable (Last Entity)
forall e. e -> Erasable e
EJust (Entity -> Last Entity
forall a. a -> Last a
Last Entity
e)) [TRobot]
forall a. Monoid a => a
mempty

  resolverByTag :: CellTag -> Text -> m (Maybe CellVal)
  resolverByTag :: CellTag -> Text -> m (Maybe CellVal)
resolverByTag = \case
    CellTag
CellTerrain -> \Text
tName -> do
      TerrainEntityMaps TerrainMap
tm EntityMap
_em <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @TerrainEntityMaps
      Maybe CellVal -> m (Maybe CellVal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CellVal -> m (Maybe CellVal))
-> (TerrainType -> Maybe CellVal)
-> TerrainType
-> m (Maybe CellVal)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TerrainObj -> CellVal) -> Maybe TerrainObj -> Maybe CellVal
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TerrainType -> CellVal
mkTerrain (TerrainType -> CellVal)
-> (TerrainObj -> TerrainType) -> TerrainObj -> CellVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TerrainObj -> TerrainType
terrainName) (Maybe TerrainObj -> Maybe CellVal)
-> (TerrainType -> Maybe TerrainObj)
-> TerrainType
-> Maybe CellVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TerrainType -> Map TerrainType TerrainObj -> Maybe TerrainObj
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` TerrainMap -> Map TerrainType TerrainObj
terrainByName TerrainMap
tm) (TerrainType -> m (Maybe CellVal))
-> TerrainType -> m (Maybe CellVal)
forall a b. (a -> b) -> a -> b
$ Text -> TerrainType
terrainFromText Text
tName
    CellTag
CellEntity -> \Text
eName ->
      case Text
eName of
        Text
"erase" -> Maybe CellVal -> m (Maybe CellVal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CellVal -> m (Maybe CellVal))
-> Maybe CellVal -> m (Maybe CellVal)
forall a b. (a -> b) -> a -> b
$ CellVal -> Maybe CellVal
forall a. a -> Maybe a
Just (TerrainType -> Erasable (Last Entity) -> [TRobot] -> CellVal
CellVal TerrainType
forall a. Monoid a => a
mempty Erasable (Last Entity)
forall e. Erasable e
EErase [TRobot]
forall a. Monoid a => a
mempty)
        Text
_ -> do
          TerrainEntityMaps TerrainMap
_tm EntityMap
em <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @TerrainEntityMaps
          Maybe CellVal -> m (Maybe CellVal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CellVal -> m (Maybe CellVal))
-> (Maybe Entity -> Maybe CellVal)
-> Maybe Entity
-> m (Maybe CellVal)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Entity -> CellVal) -> Maybe Entity -> Maybe CellVal
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Entity -> CellVal
mkEntity (Maybe Entity -> m (Maybe CellVal))
-> Maybe Entity -> m (Maybe CellVal)
forall a b. (a -> b) -> a -> b
$ Text -> EntityMap -> Maybe Entity
lookupEntityName Text
eName EntityMap
em
    CellTag
CellRobot -> \Text
_ -> Maybe CellVal -> m (Maybe CellVal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe CellVal
forall a. Maybe a
Nothing -- TODO (#1396): support robots

-- | Infer the type of a let expression, and elaborate into a series
--   of lambda applications.
inferLet ::
  ( Has (Throw CheckErr) sig m
  , Has (Reader TerrainEntityMaps) sig m
  , Has (Reader WorldMap) sig m
  ) =>
  Ctx g ->
  [(Var, WExp)] ->
  WExp ->
  m (Some (TTerm g))
inferLet :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> [(Text, WExp)] -> WExp -> m (Some (TTerm g))
inferLet Ctx g
ctx [] WExp
body = Ctx g -> WExp -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> WExp -> m (Some (TTerm g))
infer Ctx g
ctx WExp
body
inferLet Ctx g
ctx ((Text
x, WExp
e) : [(Text, WExp)]
xs) WExp
body = do
  e' :: Some (TTerm g)
e'@(Some TTy α
ty1 TTerm g α
_) <- Ctx g -> WExp -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> WExp -> m (Some (TTerm g))
infer Ctx g
ctx WExp
e
  Some TTy α
ty2 TTerm (α : g) α
let' <- Ctx (α : g) -> [(Text, WExp)] -> WExp -> m (Some (TTerm (α : g)))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> [(Text, WExp)] -> WExp -> m (Some (TTerm g))
inferLet (Text -> TTy α -> Ctx g -> Ctx (α : g)
forall a (b :: [*]). Text -> TTy a -> Ctx b -> Ctx (a : b)
CCons Text
x TTy α
ty1 Ctx g
ctx) [(Text, WExp)]
xs WExp
body
  Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
apply (TTy (α -> α) -> TTerm g (α -> α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
ty1 TTy α -> TTy α -> TTy (α -> α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
ty2) (TTerm (α : g) α -> TTerm g (α -> α)
forall a (g :: [*]) b. TTerm (a : g) b -> TTerm g (a -> b)
TLam TTerm (α : g) α
let')) Some (TTerm g)
e'

-- | Infer the type of an @overlay@ expression, and elaborate into a
--   chain of @<>@ (over) operations.
inferOverlay ::
  ( Has (Throw CheckErr) sig m
  , Has (Reader TerrainEntityMaps) sig m
  , Has (Reader WorldMap) sig m
  ) =>
  Ctx g ->
  NE.NonEmpty WExp ->
  m (Some (TTerm g))
inferOverlay :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> NonEmpty WExp -> m (Some (TTerm g))
inferOverlay Ctx g
ctx NonEmpty WExp
es = case NonEmpty WExp -> (WExp, Maybe (NonEmpty WExp))
forall a. NonEmpty a -> (a, Maybe (NonEmpty a))
NE.uncons NonEmpty WExp
es of
  -- @overlay [e] = e@
  (WExp
e, Maybe (NonEmpty WExp)
Nothing) -> Ctx g -> WExp -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> WExp -> m (Some (TTerm g))
infer Ctx g
ctx WExp
e
  -- @overlay (e : es') = e <> overlay es'@
  (WExp
e, Just NonEmpty WExp
es') -> do
    Some (TTerm g)
e' <- Ctx g -> WExp -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> WExp -> m (Some (TTerm g))
infer Ctx g
ctx WExp
e
    Some (TTerm g)
o' <- Ctx g -> NonEmpty WExp -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader TerrainEntityMaps) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> NonEmpty WExp -> m (Some (TTerm g))
inferOverlay Ctx g
ctx NonEmpty WExp
es'
    case Some (TTerm g) -> SomeTy
forall (g :: [*]). Some (TTerm g) -> SomeTy
getBaseType Some (TTerm g)
e' of
      SomeTy TTy α
ty -> do
        let wty :: TTy (World α)
wty = TTy α -> TTy (World α)
forall a. TTy a -> TTy (World a)
TTyWorld TTy α
ty
        TTerm g (α -> α -> α)
c <- TTy α
-> ((Over α, NotFun α) => m (TTerm g (α -> α -> α)))
-> m (TTerm g (α -> α -> α))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Over ty, NotFun ty) => m a) -> m a
checkOver TTy α
ty (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α)))
-> TTerm g (α -> α -> α) -> m (TTerm g (α -> α -> α))
forall a b. (a -> b) -> a -> b
$ Const (α -> α -> α) -> TTerm g (α -> α -> α)
forall a. Const a -> TTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (α -> α -> α)
forall a. (Over a, NotFun a) => Const (a -> a -> a)
COver)
        Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
apply (TTy (World α -> World α -> World α)
-> TTerm g (World α -> World α -> World α) -> Some (TTerm g)
forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy (World α)
wty TTy (World α)
-> TTy (World α -> World α) -> TTy (World α -> World α -> World α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy (World α)
wty TTy (World α) -> TTy (World α) -> TTy (World α -> World α)
forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy (World α)
wty) (Const ((α -> α -> α) -> World α -> World α -> World α)
forall a b c d.
Const ((a -> b -> c) -> (d -> a) -> (d -> b) -> d -> c)
Φ Const ((α -> α -> α) -> World α -> World α -> World α)
-> TTerm g (α -> α -> α) -> TTerm g (World α -> World α -> World α)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ TTerm g (α -> α -> α)
c)) Some (TTerm g)
e' m (Some (TTerm g))
-> (Some (TTerm g) -> m (Some (TTerm g))) -> m (Some (TTerm g))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
applyTo Some (TTerm g)
o'