{-# 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 qualified as F
import Data.Functor.Const qualified as F
import Data.Kind (Type)
import Data.List (foldl')
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 (EntityMap, lookupEntityName)
import Swarm.Game.Terrain (readTerrain)
import Swarm.Game.World.Syntax
import Swarm.Language.Pretty
import Swarm.Util (showT)
import Swarm.Util.Erasable
import Prelude hiding (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) -> [Robot] -> CellVal
CellVal forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty 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 [Robot]
r1 <!> :: CellVal -> CellVal -> CellVal
<!> CellVal TerrainType
t2 Erasable (Last Entity)
e2 [Robot]
r2 = TerrainType -> Erasable (Last Entity) -> [Robot] -> CellVal
CellVal (TerrainType
t1 forall a. Semigroup a => a -> a -> a
<> TerrainType
t2) (Erasable (Last Entity)
e1 forall a. Semigroup a => a -> a -> a
<> Erasable (Last Entity)
e2) ([Robot]
r1 forall a. Semigroup a => a -> a -> a
<> [Robot]
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)
  CReflect :: Axis -> Const (World a -> World a)
  CRot :: Rot -> Const (World a -> World a)
  COver :: (Over a, NotFun a) => Const (a -> a -> 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 = forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (a -> b)
c 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 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ 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 = forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (a -> b)
c1 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ 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 -> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Show a => a -> Text
showT α
a)
    CCell CellVal
c -> 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 -> forall a ann. PrettyPrec a => a -> Doc ann
ppr Axis
ax
    Const α
CHash -> Doc ann
"hash"
    Const α
CPerlin -> Doc ann
"perlin"
    CReflect Axis
ax -> case Axis
ax of Axis
X -> Doc ann
"vreflect"; Axis
Y -> Doc ann
"hreflect"
    CRot Rot
rot -> forall a ann. PrettyPrec a => a -> Doc ann
ppr Rot
rot
    Const α
COver -> Doc ann
"over"
    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 forall a. Num a => a -> a -> a
+ 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 = forall ty (a :: [*]). Idx (ty : a) ty
VZ
weakenVar (VS Idx g a
x) = 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
x
  TTerm g (a -> b)
f $$ TTerm g a
x = 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 = 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 -> forall a ann. Pretty a => a -> Doc ann
pretty (forall (g :: [*]) a. Idx g a -> Int
idxToNat Idx g α
ix)
    TLam TTerm (ty1 : g) ty2
t ->
      forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
        Doc ann
"λ." forall ann. Doc ann -> Doc ann -> 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 ->
      forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
1) forall a b. (a -> b) -> a -> b
$
        forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
1 TTerm g (a -> α)
t1 forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
2 TTerm g a
t2
    TConst Const α
c -> 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) = 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) = 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) = 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) = 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
  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) ->
      forall ann. Int -> Doc ann -> Doc ann
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. [Doc ann] -> Doc ann
vsep forall a b. (a -> b) -> a -> b
$
        [ Doc ann
"Error in application:"
        , forall ann. Doc ann -> Doc ann
squotes (forall a ann. PrettyPrec a => a -> Doc ann
ppr TTerm g α
t1) forall a. Semigroup a => a -> a -> a
<> Doc ann
" has type " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
squotes (forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy α
ty1)
        , Doc ann
"and cannot be applied to"
        , forall ann. Doc ann -> Doc ann
squotes (forall a ann. PrettyPrec a => a -> Doc ann
ppr TTerm g α
t2) forall a. Semigroup a => a -> a -> a
<> Doc ann
" which has type " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
squotes (forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy α
ty2)
        ]
    NoInstance Text
cls TTy a
ty -> forall ann. Doc ann -> Doc ann
squotes (forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy a
ty) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not an instance of" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Text
cls
    Unbound Text
x -> Doc ann
"Undefined variable" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Text
x
    BadType (Some TTy α
tty TTerm g α
t) TTy b
ty ->
      forall ann. [Doc ann] -> Doc ann
hsep
        [forall ann. Doc ann -> Doc ann
squotes (forall a ann. PrettyPrec a => a -> Doc ann
ppr TTerm g α
t), Doc ann
"has type", forall ann. Doc ann -> Doc ann
squotes (forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy α
tty), Doc ann
"and cannot be given type", forall ann. Doc ann -> Doc ann
squotes (forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy b
ty)]
    BadDivType TTy a
ty -> Doc ann
"Division operator used at type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
squotes (forall a ann. PrettyPrec a => a -> Doc ann
ppr TTy a
ty)
    UnknownImport Text
key -> Doc ann
"Import" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
squotes (forall a ann. Pretty a => a -> Doc ann
pretty Text
key) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"not found"
    NotAThing Text
item CellTag
tag -> forall ann. Doc ann -> Doc ann
squotes (forall a ann. Pretty a => a -> Doc ann
pretty Text
item) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. PrettyPrec a => a -> Doc ann
ppr CellTag
tag
    NotAnything Text
item -> Doc ann
"Cannot resolve cell item" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
squotes (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 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality Base a
BFloat Base b
BFloat = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality Base a
BBool Base b
BBool = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality Base a
BCell Base b
BCell = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality Base a
_ Base 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 $bTTyBool :: TTy Bool
$mTTyBool :: forall {r}. TTy Bool -> ((# #) -> r) -> ((# #) -> r) -> r
TTyBool = TTyBase BBool

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

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

pattern TTyCell :: TTy CellVal
pattern $bTTyCell :: TTy CellVal
$mTTyCell :: forall {r}. TTy CellVal -> ((# #) -> r) -> ((# #) -> r) -> r
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) = 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 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 -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
      Maybe (t :~: t)
Nothing -> forall a. Maybe a
Nothing
  testEquality TTy a
_ TTy 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) = forall a ann. PrettyPrec a => a -> Doc ann
ppr Base ty
b
  prettyPrec Int
p (TTy a
α :->: TTy b
β) =
    forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
      forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
1 TTy a
α forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"->" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
0 TTy b
β
  prettyPrec Int
p (TTyWorld TTy t
t) =
    forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
1) forall a b. (a -> b) -> a -> b
$
      Doc ann
"World" forall ann. Doc ann -> Doc ann -> 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 = (Eq ty, NotFun ty) => m a
a
checkEq (TTyBase Base ty
BInt) (Eq ty, NotFun ty) => m a
a = (Eq ty, NotFun ty) => m a
a
checkEq (TTyBase Base ty
BFloat) (Eq ty, NotFun ty) => m a
a = (Eq ty, NotFun ty) => m a
a
checkEq TTy ty
ty (Eq ty, NotFun ty) => m a
_ = forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ 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 = (Ord ty, NotFun ty) => m a
a
checkOrd (TTyBase Base ty
BInt) (Ord ty, NotFun ty) => m a
a = (Ord ty, NotFun ty) => m a
a
checkOrd (TTyBase Base ty
BFloat) (Ord ty, NotFun ty) => m a
a = (Ord ty, NotFun ty) => m a
a
checkOrd TTy ty
ty (Ord ty, NotFun ty) => m a
_ = forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ 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 = (Num ty, NotFun ty) => m a
a
checkNum (TTyBase Base ty
BFloat) (Num ty, NotFun ty) => m a
a = (Num ty, NotFun ty) => m a
a
checkNum TTy ty
ty (Num ty, NotFun ty) => m a
_ = forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ 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 = (Integral ty, NotFun ty) => m a
a
checkIntegral TTy ty
ty (Integral ty, NotFun ty) => m a
_ = forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ 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 = (Empty ty, NotFun ty) => m a
a
checkEmpty TTy ty
ty (Empty ty, NotFun ty) => m a
_ = forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ 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 = (Over ty, NotFun ty) => m a
a
checkOver (TTyBase Base ty
BInt) (Over ty, NotFun ty) => m a
a = (Over ty, NotFun ty) => m a
a
checkOver (TTyBase Base ty
BFloat) (Over ty, NotFun ty) => m a
a = (Over ty, NotFun ty) => m a
a
checkOver (TTyBase Base ty
BCell) (Over ty, NotFun ty) => m a
a = (Over ty, NotFun ty) => m a
a
checkOver TTy ty
ty (Over ty, NotFun ty) => m a
_ = forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Text -> TTy a -> CheckErr
NoInstance Text
"Over" 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) = forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy α
ty (forall α. s α -> t α
f s α
t)

type SomeTy = Some (F.Const ())

pattern SomeTy :: TTy α -> SomeTy
pattern $bSomeTy :: forall α. TTy α -> SomeTy
$mSomeTy :: forall {r}. SomeTy -> (forall {α}. TTy α -> r) -> ((# #) -> r) -> r
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 = forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError 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 forall a. Eq a => a -> a -> Bool
== Text
y = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy ty
ty forall ty (a :: [*]). Idx (ty : a) ty
VZ
  | Bool
otherwise = forall (s :: * -> *) (t :: * -> *).
(forall α. s α -> t α) -> Some s -> Some t
mapSome forall (a :: [*]) ty b. Idx a ty -> Idx (b : a) ty
VS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 EntityMap) 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 EntityMap) 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 <- forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) 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' <- forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
apply (forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy t
ty forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy t
ty) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. Const (a -> a)
I)) Some (TTerm g)
t1
  case 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 -> forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall (a :: [*]) b. Some (TTerm a) -> TTy b -> CheckErr
BadType Some (TTerm g)
t1 TTy t
ty
    Just t :~: α
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 α
_) = forall α. TTy α -> SomeTy
SomeTy TTy t
ty
getBaseType (Some TTy α
ty TTerm g α
_) = 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 <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy a
ty11 TTy α
ty2 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy b
ty12 (TTerm g α
t1 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 <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy t
ty11 TTy α
ty2 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy b
ty12 (TTerm g α
t1 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ (forall a b. Const (a -> b -> a)
K 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 <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy a
ty11 TTy t
ty2 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall a. TTy a -> TTy (World a)
TTyWorld TTy b
ty12) (forall a b c. Const ((a -> b) -> (c -> a) -> c -> b)
B forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ TTerm g α
t1 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ TTerm g α
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 <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy a
ty11 TTy α
ty2 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall a. TTy a -> TTy (World a)
TTyWorld TTy b
ty12) (forall a b c. Const ((a -> b -> c) -> (a -> b) -> a -> c)
S forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ TTerm g α
t1 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ (forall a b. Const (a -> b -> a)
K 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 <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TTy a
ty11 TTy t
ty2 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall a. TTy a -> TTy (World a)
TTyWorld TTy b
ty12) (forall a b c. Const ((a -> b -> c) -> (a -> b) -> a -> c)
S forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ TTerm g α
t1 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ TTerm g α
t2)
apply Some (TTerm g)
t1 Some (TTerm g)
t2 = forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Bool
TTyBool forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Bool -> Bool)
CNot)
inferOp [SomeTy TTy α
tyA] Op
Neg = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Num a, NotFun a) => Const (a -> a)
CNeg)
inferOp [SomeTy]
_ Op
And = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Bool
TTyBool forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Bool -> Bool -> Bool)
CAnd)
inferOp [SomeTy]
_ Op
Or = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Bool
TTyBool forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Bool -> Bool -> Bool)
COr)
inferOp [SomeTy TTy α
tyA] Op
Abs = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Num a, NotFun a) => Const (a -> a)
CAbs)
inferOp [SomeTy TTy α
tyA] Op
Add = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Num a, NotFun a) => Const (a -> a -> a)
CAdd)
inferOp [SomeTy TTy α
tyA] Op
Sub = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Num a, NotFun a) => Const (a -> a -> a)
CSub)
inferOp [SomeTy TTy α
tyA] Op
Mul = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Num ty, NotFun ty) => m a) -> m a
checkNum TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Num a, NotFun a) => Const (a -> a -> a)
CMul)
inferOp [SomeTy TTy α
tyA] Op
Div = case TTy α
tyA of
  TTyBase Base α
BInt -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Integral a, NotFun a) => Const (a -> a -> a)
CIDiv)
  TTyBase Base α
BFloat -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Fractional a, NotFun a) => Const (a -> a -> a)
CDiv)
  TTy α
_ -> forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. TTy a -> CheckErr
BadDivType TTy α
tyA
inferOp [SomeTy TTy α
tyA] Op
Mod = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Integral ty, NotFun ty) => m a) -> m a
checkIntegral TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Integral a, NotFun a) => Const (a -> a -> a)
CMod)
inferOp [SomeTy TTy α
tyA] Op
Eq = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Eq ty, NotFun ty) => m a) -> m a
checkEq TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Eq a, NotFun a) => Const (a -> a -> Bool)
CEq)
inferOp [SomeTy TTy α
tyA] Op
Neq = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Eq ty, NotFun ty) => m a) -> m a
checkEq TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Eq a, NotFun a) => Const (a -> a -> Bool)
CNeq)
inferOp [SomeTy TTy α
tyA] Op
Lt = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Ord ty, NotFun ty) => m a) -> m a
checkOrd TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Ord a, NotFun a) => Const (a -> a -> Bool)
CLt)
inferOp [SomeTy TTy α
tyA] Op
Leq = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Ord ty, NotFun ty) => m a) -> m a
checkOrd TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Ord a, NotFun a) => Const (a -> a -> Bool)
CLeq)
inferOp [SomeTy TTy α
tyA] Op
Gt = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Ord ty, NotFun ty) => m a) -> m a
checkOrd TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Ord a, NotFun a) => Const (a -> a -> Bool)
CGt)
inferOp [SomeTy TTy α
tyA] Op
Geq = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Bool
TTyBool) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Ord ty, NotFun ty) => m a) -> m a
checkOrd TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Ord a, NotFun a) => Const (a -> a -> Bool)
CGeq)
inferOp [SomeTy TTy α
tyA] Op
If = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Bool
TTyBool forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. Const (Bool -> a -> a -> a)
CIf)
inferOp [SomeTy]
_ Op
Perlin = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy Integer
TTyInt forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Integer
TTyInt forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Double
TTyFloat forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy Double
TTyFloat forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: forall a. TTy a -> TTy (World a)
TTyWorld TTy Double
TTyFloat) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Integer -> Integer -> Double -> Double -> World Double)
CPerlin)
inferOp [SomeTy TTy α
tyA] (Reflect Axis
r) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall a. TTy a -> TTy (World a)
TTyWorld TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: forall a. TTy a -> TTy (World a)
TTyWorld TTy α
tyA) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (forall a. Axis -> Const (World a -> World a)
CReflect Axis
r))
inferOp [SomeTy TTy α
tyA] (Rot Rot
r) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall a. TTy a -> TTy (World a)
TTyWorld TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: forall a. TTy a -> TTy (World a)
TTyWorld TTy α
tyA) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (forall a. Rot -> Const (World a -> World a)
CRot Rot
r))
inferOp [SomeTy TTy α
tyA] Op
Mask = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall a. TTy a -> TTy (World a)
TTyWorld TTy Bool
TTyBool forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: forall a. TTy a -> TTy (World a)
TTyWorld TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: forall a. TTy a -> TTy (World a)
TTyWorld TTy α
tyA) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Empty ty, NotFun ty) => m a) -> m a
checkEmpty TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a.
(Empty a, NotFun a) =>
Const (World Bool -> World a -> World a)
CMask)
inferOp [SomeTy TTy α
tyA] Op
Overlay = forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
tyA) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Over ty, NotFun ty) => m a) -> m a
checkOver TTy α
tyA (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Over a, NotFun a) => Const (a -> a -> a)
COver)
inferOp [SomeTy]
tys Op
op = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"bad call to inferOp: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [SomeTy]
tys forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show 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 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] = [forall (g :: [*]). Some (TTerm g) -> SomeTy
getBaseType Some (TTerm g)
t]
typeArgsFor (Reflect Axis
_) (Some (TTerm g)
t : [Some (TTerm g)]
_) = [forall (g :: [*]). Some (TTerm g) -> SomeTy
getBaseType Some (TTerm g)
t]
typeArgsFor (Rot Rot
_) (Some (TTerm g)
t : [Some (TTerm g)]
_) = [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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Op
If, Op
Mask, Op
Overlay] = [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 EntityMap) 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 EntityMap) 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> WExp -> m (Some (TTerm g))
infer Ctx g
ctx) [WExp]
ts
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\m (Some (TTerm g))
r -> (m (Some (TTerm g))
r forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
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 =>
[SomeTy] -> Op -> m (Some (TTerm g))
inferOp (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 EntityMap) 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 EntityMap) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> WExp -> m (Some (TTerm g))
infer Ctx g
_ (WInt Integer
i) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall t. Base t -> TTy t
TTyBase Base Integer
BInt) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (forall a. (Show a, NotFun a) => a -> Const a
CLit Integer
i))
infer Ctx g
_ (WFloat Double
f) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall t. Base t -> TTy t
TTyBase Base Double
BFloat) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (forall a. (Show a, NotFun a) => a -> Const a
CLit Double
f))
infer Ctx g
_ (WBool Bool
b) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall t. Base t -> TTy t
TTyBase Base Bool
BBool) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (forall a. (Show a, NotFun a) => a -> Const a
CLit Bool
b))
infer Ctx g
_ (WCell RawCellVal
c) = do
  CellVal
c' <- forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) sig m) =>
RawCellVal -> m CellVal
resolveCell RawCellVal
c
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy CellVal
TTyCell (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (CellVal -> Const CellVal
CCell CellVal
c'))
infer Ctx g
ctx (WVar Text
x) = forall (s :: * -> *) (t :: * -> *).
(forall α. s α -> t α) -> Some s -> Some t
mapSome forall (g :: [*]) a. Idx g a -> TTerm g a
TVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) = forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some TTy Integer
TTyInt (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const Integer
CSeed)
infer Ctx g
_ (WCoord Axis
ax) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall a. TTy a -> TTy (World a)
TTyWorld TTy Integer
TTyInt) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed (Axis -> Const (Coords -> Integer)
CCoord Axis
ax))
infer Ctx g
_ WExp
WHash = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a (t :: * -> *). TTy a -> t a -> Some t
Some (forall a. TTy a -> TTy (World a)
TTyWorld TTy Integer
TTyInt) (forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const (Coords -> Integer)
CHash)
infer Ctx g
ctx (WLet [(Text, WExp)]
defs WExp
body) = forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) 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) = forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) 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 forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
key WorldMap
worldMap of
    Just (Some TTy α
ty TTerm '[] α
t) -> forall (m :: * -> *) a. Monad m => a -> m a
return (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 -> forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError 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 EntityMap) sig m) =>
  RawCellVal ->
  m CellVal
resolveCell :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) sig m) =>
RawCellVal -> m CellVal
resolveCell RawCellVal
items = do
  [CellVal]
cellVals <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) sig m) =>
(Maybe CellTag, Text) -> m CellVal
resolveCellItem RawCellVal
items
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall m. Over m => m -> m -> m
(<!>) 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 EntityMap) sig m) =>
  (Maybe CellTag, Text) ->
  m CellVal
resolveCellItem :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) 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
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Text -> CellTag -> CheckErr
NotAThing Text
item CellTag
cellTag) 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CellTag -> Text -> m (Maybe CellVal)
`resolverByTag` Text
item) [forall a. Bounded a => a
minBound .. forall a. Bounded a => a
maxBound :: CellTag]
    case forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
F.asum [Maybe CellVal]
maybeCells of
      Maybe CellVal
Nothing -> forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Text -> CheckErr
NotAnything Text
item
      Just CellVal
cell -> forall (m :: * -> *) a. Monad m => a -> m a
return CellVal
cell
 where
  mkTerrain :: TerrainType -> CellVal
mkTerrain TerrainType
t = TerrainType -> Erasable (Last Entity) -> [Robot] -> CellVal
CellVal TerrainType
t forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
  mkEntity :: Entity -> CellVal
mkEntity Entity
e = TerrainType -> Erasable (Last Entity) -> [Robot] -> CellVal
CellVal forall a. Monoid a => a
mempty (forall e. e -> Erasable e
EJust (forall a. a -> Last a
Last Entity
e)) forall a. Monoid a => a
mempty
  resolverByTag :: CellTag -> Text -> m (Maybe CellVal)
  resolverByTag :: CellTag -> Text -> m (Maybe CellVal)
resolverByTag = \case
    CellTag
CellTerrain -> forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TerrainType -> CellVal
mkTerrain forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Maybe TerrainType
readTerrain
    CellTag
CellEntity -> \Text
eName ->
      case Text
eName of
        Text
"erase" -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (TerrainType -> Erasable (Last Entity) -> [Robot] -> CellVal
CellVal forall a. Monoid a => a
mempty forall e. Erasable e
EErase forall a. Monoid a => a
mempty)
        Text
_ -> do
          EntityMap
em <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @EntityMap
          forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Entity -> CellVal
mkEntity forall a b. (a -> b) -> a -> b
$ Text -> EntityMap -> Maybe Entity
lookupEntityName Text
eName EntityMap
em
    CellTag
CellRobot -> \Text
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 EntityMap) 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 EntityMap) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> [(Text, WExp)] -> WExp -> m (Some (TTerm g))
inferLet Ctx g
ctx [] WExp
body = forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) 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 α
_) <- forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) 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' <- forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> [(Text, WExp)] -> WExp -> m (Some (TTerm g))
inferLet (forall a (b :: [*]). Text -> TTy a -> Ctx b -> Ctx (a : b)
CCons Text
x TTy α
ty1 Ctx g
ctx) [(Text, WExp)]
xs WExp
body
  forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
apply (forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy α
ty1 forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy α
ty2) (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 EntityMap) 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 EntityMap) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> NonEmpty WExp -> m (Some (TTerm g))
inferOverlay Ctx g
ctx NonEmpty WExp
es = case forall a. NonEmpty a -> (a, Maybe (NonEmpty a))
NE.uncons NonEmpty WExp
es of
  -- @overlay [e] = e@
  (WExp
e, Maybe (NonEmpty WExp)
Nothing) -> forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) 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' <- forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> WExp -> m (Some (TTerm g))
infer Ctx g
ctx WExp
e
    Some (TTerm g)
o' <- forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
(Has (Throw CheckErr) sig m, Has (Reader EntityMap) sig m,
 Has (Reader WorldMap) sig m) =>
Ctx g -> NonEmpty WExp -> m (Some (TTerm g))
inferOverlay Ctx g
ctx NonEmpty WExp
es'
    case forall (g :: [*]). Some (TTerm g) -> SomeTy
getBaseType Some (TTerm g)
e' of
      SomeTy TTy α
ty -> do
        let wty :: TTy (World α)
wty = forall a. TTy a -> TTy (World a)
TTyWorld TTy α
ty
        TTerm g (α -> α -> α)
c <- forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty a.
Has (Throw CheckErr) sig m =>
TTy ty -> ((Over ty, NotFun ty) => m a) -> m a
checkOver TTy α
ty (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. HasConst t => Const a -> t a
embed forall a. (Over a, NotFun a) => Const (a -> a -> a)
COver)
        forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
apply (forall a (t :: * -> *). TTy a -> t a -> Some t
Some (TTy (World α)
wty forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy (World α)
wty forall a b. TTy a -> TTy b -> TTy (a -> b)
:->: TTy (World α)
wty) (forall a b c d.
Const ((a -> b -> c) -> (d -> a) -> (d -> b) -> d -> c)
Φ forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ TTerm g (α -> α -> α)
c)) Some (TTerm g)
e' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (sig :: (* -> *) -> * -> *) (m :: * -> *) (g :: [*]).
Has (Throw CheckErr) sig m =>
Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
applyTo Some (TTerm g)
o'