{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
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)
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)
infixl 1 $$
class Applicable t where
($$) :: t (a -> b) -> t a -> t b
type family IsFun a where
IsFun (_ -> _) = 'True
IsFun _ = 'False
type NotFun a = IsFun a ~ 'False
data Const :: Type -> Type where
CLit :: (Show a, NotFun a) => a -> Const a
CCell :: CellVal -> Const CellVal
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)
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)
Φ :: 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
"Φ"
type family Append (xs :: [k]) (ys :: [k]) :: [k] where
Append '[] ys = ys
Append (x ': xs) ys = x ': Append xs ys
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
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)
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
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
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)
data Base :: Type -> Type where
BInt :: Base Integer
BFloat :: Base Double
BBool :: Base Bool
BCell :: Base CellVal
deriving instance Show (Base ty)
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"
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)
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
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
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 WorldMap = Map Text (Some (TTerm '[]))
data Ctx :: [Type] -> Type where
CNil :: Ctx '[]
CCons :: Text -> TTy ty -> Ctx g -> Ctx (ty ': g)
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 ::
( 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'
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 :: (Has (Throw CheckErr) sig m) => Some (TTerm g) -> Some (TTerm g) -> m (Some (TTerm g))
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)
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))
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)
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))
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
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
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)]
_ = []
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 ::
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
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
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
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
[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
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'
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
(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
(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'