{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Swarm.Language.Typecheck (
TypeErr (..),
InvalidAtomicReason (..),
getTypeErrSrcLoc,
Infer,
runInfer,
lookup,
fresh,
substU,
(=:=),
HasBindings (..),
instantiate,
skolemize,
generalize,
inferTop,
inferModule,
infer,
inferConst,
check,
decomposeCmdTy,
decomposeFunTy,
isSimpleUType,
) where
import Control.Category ((>>>))
import Control.Lens ((^.))
import Control.Monad.Except
import Control.Monad.Reader
import Control.Unification hiding (applyBindings, (=:=))
import Control.Unification qualified as U
import Control.Unification.IntVar
import Data.Data (Data, gmapM)
import Data.Foldable (fold)
import Data.Functor.Identity
import Data.Generics (mkM)
import Data.Map (Map)
import Data.Map qualified as M
import Data.Maybe
import Data.Set (Set, (\\))
import Data.Set qualified as S
import Swarm.Language.Context hiding (lookup)
import Swarm.Language.Context qualified as Ctx
import Swarm.Language.Module
import Swarm.Language.Parse.QQ (tyQ)
import Swarm.Language.Syntax
import Swarm.Language.Types
import Prelude hiding (lookup)
type Infer = ReaderT UCtx (ExceptT TypeErr (IntBindingT TypeF Identity))
runInfer :: TCtx -> Infer UModule -> Either TypeErr TModule
runInfer :: Ctx Polytype -> Infer UModule -> Either TypeErr TModule
runInfer Ctx Polytype
ctx =
(forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall u. HasBindings u => u -> Infer u
applyBindings)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ( forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\(Module Syntax' UType
u UCtx
uctx) ->
forall s t. Syntax' s -> Ctx t -> Module s t
Module
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. WithU t => U t -> t
fromU forall b c a. (b -> c) -> (a -> b) -> a -> c
. UType -> Infer UPolytype
generalize) Syntax' UType
u
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t. WithU t => U t -> t
fromU UCtx
uctx)
)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall t. WithU t => t -> U t
toU Ctx Polytype
ctx)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (m :: * -> *) (t :: * -> *) a.
Monad m =>
IntBindingT t m a -> m a
evalIntBindingT
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall a. Identity a -> a
runIdentity
lookup :: SrcLoc -> Var -> Infer UType
lookup :: SrcLoc -> Var -> Infer UType
lookup SrcLoc
loc Var
x = do
UCtx
ctx <- forall r (m :: * -> *). MonadReader r m => m r
ask
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SrcLoc -> Var -> TypeErr
UnboundVar SrcLoc
loc Var
x) UPolytype -> Infer UType
instantiate (forall t. Var -> Ctx t -> Maybe t
Ctx.lookup Var
x UCtx
ctx)
deriving instance Ord IntVar
class FreeVars a where
freeVars :: a -> Infer (Set IntVar)
instance FreeVars UType where
freeVars :: UType -> Infer (Set IntVar)
freeVars UType
ut = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m [v]
getFreeVars UType
ut
instance FreeVars t => FreeVars (Poly t) where
freeVars :: Poly t -> Infer (Set IntVar)
freeVars (Forall [Var]
_ t
t) = forall a. FreeVars a => a -> Infer (Set IntVar)
freeVars t
t
instance FreeVars UCtx where
freeVars :: UCtx -> Infer (Set IntVar)
freeVars = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. FreeVars a => a -> Infer (Set IntVar)
freeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Ctx t -> Map Var t
unCtx
fresh :: Infer UType
fresh :: Infer UType
fresh = forall (t :: * -> *) v. v -> UTerm t v
UVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar)
substU :: Map (Either Var IntVar) UType -> UType -> UType
substU :: Map (Either Var IntVar) UType -> UType -> UType
substU Map (Either Var IntVar) UType
m =
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> UTerm t v -> a
ucata
(\IntVar
v -> forall a. a -> Maybe a -> a
fromMaybe (forall (t :: * -> *) v. v -> UTerm t v
UVar IntVar
v) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall a b. b -> Either a b
Right IntVar
v) Map (Either Var IntVar) UType
m))
( \case
TyVarF Var
v -> forall a. a -> Maybe a -> a
fromMaybe (Var -> UType
UTyVar Var
v) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall a b. a -> Either a b
Left Var
v) Map (Either Var IntVar) UType
m)
TypeF UType
f -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeF UType
f
)
infix 4 =:=
(=:=) :: UType -> UType -> Infer UType
UType
s =:= :: UType -> UType -> Infer UType
=:= UType
t = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ UType
s forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m (UTerm t v)
U.=:= UType
t
class HasBindings u where
applyBindings :: u -> Infer u
instance HasBindings UType where
applyBindings :: UType -> Infer UType
applyBindings = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> em m (UTerm t v)
U.applyBindings
instance HasBindings UPolytype where
applyBindings :: UPolytype -> Infer UPolytype
applyBindings (Forall [Var]
xs UType
u) = forall t. [Var] -> t -> Poly t
Forall [Var]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u. HasBindings u => u -> Infer u
applyBindings UType
u
instance HasBindings UCtx where
applyBindings :: UCtx -> Infer UCtx
applyBindings = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall u. HasBindings u => u -> Infer u
applyBindings
instance (HasBindings u, Data u) => HasBindings (Term' u) where
applyBindings :: Term' u -> Infer (Term' u)
applyBindings = forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> a -> m a
gmapM (forall (m :: * -> *) a b.
(Monad m, Typeable a, Typeable b) =>
(b -> m b) -> a -> m a
mkM (forall u. HasBindings u => u -> Infer u
applyBindings @(Syntax' u)))
instance (HasBindings u, Data u) => HasBindings (Syntax' u) where
applyBindings :: Syntax' u -> Infer (Syntax' u)
applyBindings (Syntax' SrcLoc
l Term' u
t u
u) = forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u. HasBindings u => u -> Infer u
applyBindings Term' u
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall u. HasBindings u => u -> Infer u
applyBindings u
u
instance HasBindings UModule where
applyBindings :: UModule -> Infer UModule
applyBindings (Module Syntax' UType
u UCtx
uctx) = forall s t. Syntax' s -> Ctx t -> Module s t
Module forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u. HasBindings u => u -> Infer u
applyBindings Syntax' UType
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall u. HasBindings u => u -> Infer u
applyBindings UCtx
uctx
instantiate :: UPolytype -> Infer UType
instantiate :: UPolytype -> Infer UType
instantiate (Forall [Var]
xs UType
uty) = do
[UType]
xs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const Infer UType
fresh) [Var]
xs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Map (Either Var IntVar) UType -> UType -> UType
substU (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. a -> Either a b
Left [Var]
xs) [UType]
xs')) UType
uty
skolemize :: UPolytype -> Infer UType
skolemize :: UPolytype -> Infer UType
skolemize (Forall [Var]
xs UType
uty) = do
[UType]
xs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const Infer UType
fresh) [Var]
xs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Map (Either Var IntVar) UType -> UType -> UType
substU (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. a -> Either a b
Left [Var]
xs) (forall a b. (a -> b) -> [a] -> [b]
map forall {t :: * -> *}.
Show (t (UTerm t IntVar)) =>
UTerm t IntVar -> UType
toSkolem [UType]
xs'))) UType
uty
where
toSkolem :: UTerm t IntVar -> UType
toSkolem (UVar IntVar
v) = Var -> UType
UTyVar (Var -> IntVar -> Var
mkVarName Var
"s" IntVar
v)
toSkolem UTerm t IntVar
x = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! Non-UVar in skolemize.toSkolem: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show UTerm t IntVar
x
generalize :: UType -> Infer UPolytype
generalize :: UType -> Infer UPolytype
generalize UType
uty = do
UType
uty' <- forall u. HasBindings u => u -> Infer u
applyBindings UType
uty
UCtx
ctx <- forall r (m :: * -> *). MonadReader r m => m r
ask
Set IntVar
tmfvs <- forall a. FreeVars a => a -> Infer (Set IntVar)
freeVars UType
uty'
Set IntVar
ctxfvs <- forall a. FreeVars a => a -> Infer (Set IntVar)
freeVars UCtx
ctx
let fvs :: [IntVar]
fvs = forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ Set IntVar
tmfvs forall a. Ord a => Set a -> Set a -> Set a
\\ Set IntVar
ctxfvs
xs :: [Var]
xs = forall a b. (a -> b) -> [a] -> [b]
map (Var -> IntVar -> Var
mkVarName Var
"a") [IntVar]
fvs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [Var] -> t -> Poly t
Forall [Var]
xs (Map (Either Var IntVar) UType -> UType -> UType
substU (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. b -> Either a b
Right [IntVar]
fvs) (forall a b. (a -> b) -> [a] -> [b]
map Var -> UType
UTyVar [Var]
xs))) UType
uty')
data TypeErr
=
UnboundVar SrcLoc Var
|
EscapedSkolem SrcLoc Var
| Infinite IntVar UType
|
Mismatch SrcLoc (TypeF UType) (TypeF UType)
|
DefNotTopLevel SrcLoc Term
|
CantInfer SrcLoc Term
|
InvalidAtomic SrcLoc InvalidAtomicReason Term
deriving (Int -> TypeErr -> ShowS
[TypeErr] -> ShowS
TypeErr -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TypeErr] -> ShowS
$cshowList :: [TypeErr] -> ShowS
show :: TypeErr -> [Char]
$cshow :: TypeErr -> [Char]
showsPrec :: Int -> TypeErr -> ShowS
$cshowsPrec :: Int -> TypeErr -> ShowS
Show)
data InvalidAtomicReason
=
TooManyTicks Int
|
AtomicDupingThing
|
NonSimpleVarType Var UPolytype
|
NestedAtomic
|
LongConst
deriving (Int -> InvalidAtomicReason -> ShowS
[InvalidAtomicReason] -> ShowS
InvalidAtomicReason -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [InvalidAtomicReason] -> ShowS
$cshowList :: [InvalidAtomicReason] -> ShowS
show :: InvalidAtomicReason -> [Char]
$cshow :: InvalidAtomicReason -> [Char]
showsPrec :: Int -> InvalidAtomicReason -> ShowS
$cshowsPrec :: Int -> InvalidAtomicReason -> ShowS
Show)
instance Fallible TypeF IntVar TypeErr where
occursFailure :: IntVar -> UType -> TypeErr
occursFailure = IntVar -> UType -> TypeErr
Infinite
mismatchFailure :: TypeF UType -> TypeF UType -> TypeErr
mismatchFailure = SrcLoc -> TypeF UType -> TypeF UType -> TypeErr
Mismatch SrcLoc
NoLoc
getTypeErrSrcLoc :: TypeErr -> Maybe SrcLoc
getTypeErrSrcLoc :: TypeErr -> Maybe SrcLoc
getTypeErrSrcLoc TypeErr
te = case TypeErr
te of
UnboundVar SrcLoc
l Var
_ -> forall a. a -> Maybe a
Just SrcLoc
l
EscapedSkolem SrcLoc
l Var
_ -> forall a. a -> Maybe a
Just SrcLoc
l
Infinite IntVar
_ UType
_ -> forall a. Maybe a
Nothing
Mismatch SrcLoc
l TypeF UType
_ TypeF UType
_ -> forall a. a -> Maybe a
Just SrcLoc
l
DefNotTopLevel SrcLoc
l Term
_ -> forall a. a -> Maybe a
Just SrcLoc
l
CantInfer SrcLoc
l Term
_ -> forall a. a -> Maybe a
Just SrcLoc
l
InvalidAtomic SrcLoc
l InvalidAtomicReason
_ Term
_ -> forall a. a -> Maybe a
Just SrcLoc
l
inferTop :: TCtx -> Syntax -> Either TypeErr TModule
inferTop :: Ctx Polytype -> Syntax -> Either TypeErr TModule
inferTop Ctx Polytype
ctx = Ctx Polytype -> Infer UModule -> Either TypeErr TModule
runInfer Ctx Polytype
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. Syntax -> Infer UModule
inferModule
inferModule :: Syntax -> Infer UModule
inferModule :: Syntax -> Infer UModule
inferModule s :: Syntax
s@(Syntax SrcLoc
l Term
t) = (forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall ty a. Syntax' ty -> TypeErr -> Infer a
addLocToTypeErr Syntax
s) forall a b. (a -> b) -> a -> b
$ case Term
t of
SDef Bool
r LocVar
x Maybe Polytype
Nothing Syntax
t1 -> do
UType
xTy <- Infer UType
fresh
Syntax' UType
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UType
xTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
t1
UType
_ <- UType
xTy UType -> UType -> Infer UType
=:= Syntax' UType
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType
UPolytype
pty <- UType -> Infer UPolytype
generalize (Syntax' UType
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s t. Syntax' s -> Ctx t -> Module s t
Module (forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty.
Bool -> LocVar -> Maybe Polytype -> Syntax' ty -> Term' ty
SDef Bool
r LocVar
x forall a. Maybe a
Nothing Syntax' UType
t1') (UType -> UType
UTyCmd UType
UTyUnit)) (forall t. Var -> t -> Ctx t
singleton (LocVar -> Var
lvVar LocVar
x) UPolytype
pty)
SDef Bool
r LocVar
x (Just Polytype
pty) Syntax
t1 -> do
let upty :: U Polytype
upty = forall t. WithU t => t -> U t
toU Polytype
pty
UType
uty <- UPolytype -> Infer UType
skolemize UPolytype
upty
Syntax' UType
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty forall a b. (a -> b) -> a -> b
$ Syntax
-> UType
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
check Syntax
t1 UType
uty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s t. Syntax' s -> Ctx t -> Module s t
Module (forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty.
Bool -> LocVar -> Maybe Polytype -> Syntax' ty -> Term' ty
SDef Bool
r LocVar
x (forall a. a -> Maybe a
Just Polytype
pty) Syntax' UType
t1') (UType -> UType
UTyCmd UType
UTyUnit)) (forall t. Var -> t -> Ctx t
singleton (LocVar -> Var
lvVar LocVar
x) UPolytype
upty)
SBind Maybe LocVar
mx Syntax
c1 Syntax
c2 -> do
Module Syntax' UType
c1' UCtx
ctx1 <- Syntax -> Infer UModule
inferModule Syntax
c1
UType
a <- UType -> Infer UType
decomposeCmdTy (Syntax' UType
c1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Ctx t -> m a -> m a
withBindings UCtx
ctx1 forall a b. (a -> b) -> a -> b
$
forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id ((forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
`withBinding` forall t. [Var] -> t -> Poly t
Forall [] UType
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx forall a b. (a -> b) -> a -> b
$ do
Module Syntax' UType
c2' UCtx
ctx2 <- Syntax -> Infer UModule
inferModule Syntax
c2
UType
_ <- UType -> Infer UType
decomposeCmdTy (Syntax' UType
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
let ctxX :: UCtx
ctxX = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall t. Ctx t
Ctx.empty ((forall t. Var -> t -> Ctx t
`Ctx.singleton` forall t. [Var] -> t -> Poly t
Forall [] UType
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
forall s t. Syntax' s -> Ctx t -> Module s t
Module
(forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Maybe LocVar -> Syntax' ty -> Syntax' ty -> Term' ty
SBind Maybe LocVar
mx Syntax' UType
c1' Syntax' UType
c2') (Syntax' UType
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))
(UCtx
ctx1 forall t. Ctx t -> Ctx t -> Ctx t
`Ctx.union` UCtx
ctxX forall t. Ctx t -> Ctx t -> Ctx t
`Ctx.union` UCtx
ctx2)
Term
_anyOtherTerm -> forall s t. Syntax' s -> Module s t
trivMod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
s
infer :: Syntax -> Infer (Syntax' UType)
infer :: Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer s :: Syntax
s@(Syntax SrcLoc
l Term
t) = (forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall ty a. Syntax' ty -> TypeErr -> Infer a
addLocToTypeErr Syntax
s) forall a b. (a -> b) -> a -> b
$ case Term
t of
Term
TUnit -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l forall ty. Term' ty
TUnit UType
UTyUnit
TConst Const
c -> forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Const -> Term' ty
TConst Const
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UPolytype -> Infer UType
instantiate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. WithU t => t -> U t
toU forall a b. (a -> b) -> a -> b
$ Const -> Polytype
inferConst Const
c)
TDir Direction
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Direction -> Term' ty
TDir Direction
d) UType
UTyDir
TInt Integer
n -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Integer -> Term' ty
TInt Integer
n) UType
UTyInt
TAntiInt Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TAntiInt Var
x) UType
UTyInt
TText Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TText Var
x) UType
UTyText
TAntiText Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TAntiText Var
x) UType
UTyText
TBool Bool
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Bool -> Term' ty
TBool Bool
b) UType
UTyBool
TRobot Int
r -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Int -> Term' ty
TRobot Int
r) UType
UTyActor
TRef Int
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term -> TypeErr
CantInfer SrcLoc
l Term
t
TRequireDevice Var
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TRequireDevice Var
d) (UType -> UType
UTyCmd UType
UTyUnit)
TRequire Int
n Var
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Int -> Var -> Term' ty
TRequire Int
n Var
d) (UType -> UType
UTyCmd UType
UTyUnit)
SPair Syntax
t1 Syntax
t2 -> do
Syntax' UType
t1' <- Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
t1
Syntax' UType
t2' <- Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
t2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SPair Syntax' UType
t1' Syntax' UType
t2') (UType -> UType -> UType
UTyProd (Syntax' UType
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType) (Syntax' UType
t2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))
SDelay DelayType
d Syntax
t1 -> do
Syntax' UType
t1' <- Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
t1
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. DelayType -> Syntax' ty -> Term' ty
SDelay DelayType
d Syntax' UType
t1') (UType -> UType
UTyDelay (Syntax' UType
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))
TConst Const
Atomic :$: Syntax
at -> do
UType
argTy <- Infer UType
fresh
Syntax' UType
at' <- Syntax
-> UType
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
check Syntax
at (UType -> UType
UTyCmd UType
argTy)
Syntax' UType
atomic' <- Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer (SrcLoc -> Term -> Syntax
Syntax SrcLoc
l (forall ty. Const -> Term' ty
TConst Const
Atomic))
Syntax -> Infer ()
validAtomic Syntax
at
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SApp Syntax' UType
atomic' Syntax' UType
at') (Syntax' UType
at' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
TVar Var
x -> forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TVar Var
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcLoc -> Var -> Infer UType
lookup SrcLoc
l Var
x
SLam LocVar
x (Just Fix TypeF
argTy) Syntax
lt -> do
let uargTy :: U (Fix TypeF)
uargTy = forall t. WithU t => t -> U t
toU Fix TypeF
argTy
Syntax' UType
lt' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UType
uargTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
lt
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. LocVar -> Maybe (Fix TypeF) -> Syntax' ty -> Term' ty
SLam LocVar
x (forall a. a -> Maybe a
Just Fix TypeF
argTy) Syntax' UType
lt') (UType -> UType -> UType
UTyFun UType
uargTy (Syntax' UType
lt' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))
SLam LocVar
x Maybe (Fix TypeF)
Nothing Syntax
lt -> do
UType
argTy <- Infer UType
fresh
Syntax' UType
lt' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UType
argTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
lt
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. LocVar -> Maybe (Fix TypeF) -> Syntax' ty -> Term' ty
SLam LocVar
x forall a. Maybe a
Nothing Syntax' UType
lt') (UType -> UType -> UType
UTyFun UType
argTy (Syntax' UType
lt' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))
SApp Syntax
f Syntax
x -> do
Syntax' UType
f' <- Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
f
(UType
ty1, UType
ty2) <- UType -> Infer (UType, UType)
decomposeFunTy (Syntax' UType
f' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
Syntax' UType
x' <- Syntax
-> UType
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
check Syntax
x UType
ty1 forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall ty a. Syntax' ty -> TypeErr -> Infer a
addLocToTypeErr Syntax
x
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SApp Syntax' UType
f' Syntax' UType
x') UType
ty2
SLet Bool
r LocVar
x Maybe Polytype
Nothing Syntax
t1 Syntax
t2 -> do
UType
xTy <- Infer UType
fresh
Syntax' UType
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UType
xTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
t1
let uty :: UType
uty = Syntax' UType
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType
UType
_ <- UType
xTy UType -> UType -> Infer UType
=:= UType
uty
UPolytype
upty <- UType -> Infer UPolytype
generalize UType
uty
Syntax' UType
t2' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
t2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty.
Bool
-> LocVar -> Maybe Polytype -> Syntax' ty -> Syntax' ty -> Term' ty
SLet Bool
r LocVar
x forall a. Maybe a
Nothing Syntax' UType
t1' Syntax' UType
t2') (Syntax' UType
t2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
SLet Bool
r LocVar
x (Just Polytype
pty) Syntax
t1 Syntax
t2 -> do
let upty :: U Polytype
upty = forall t. WithU t => t -> U t
toU Polytype
pty
UType
uty <- UPolytype -> Infer UType
skolemize UPolytype
upty
(Syntax' UType
t1', Syntax' UType
t2') <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty forall a b. (a -> b) -> a -> b
$ do
(,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Syntax
-> UType
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
check Syntax
t1 UType
uty
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall ty a. Syntax' ty -> TypeErr -> Infer a
addLocToTypeErr Syntax
t1
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
t2
forall r (m :: * -> *). MonadReader r m => m r
ask forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ UPolytype -> Infer ()
noSkolems
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty.
Bool
-> LocVar -> Maybe Polytype -> Syntax' ty -> Syntax' ty -> Term' ty
SLet Bool
r LocVar
x (forall a. a -> Maybe a
Just Polytype
pty) Syntax' UType
t1' Syntax' UType
t2') (Syntax' UType
t2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
SDef {} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term -> TypeErr
DefNotTopLevel SrcLoc
l Term
t
SBind Maybe LocVar
mx Syntax
c1 Syntax
c2 -> do
Syntax' UType
c1' <- Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
c1
UType
a <- UType -> Infer UType
decomposeCmdTy (Syntax' UType
c1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
Syntax' UType
c2' <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id ((forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
`withBinding` forall t. [Var] -> t -> Poly t
Forall [] UType
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
c2
UType
_ <- UType -> Infer UType
decomposeCmdTy (Syntax' UType
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Maybe LocVar -> Syntax' ty -> Syntax' ty -> Term' ty
SBind Maybe LocVar
mx Syntax' UType
c1' Syntax' UType
c2') (Syntax' UType
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
where
noSkolems :: UPolytype -> Infer ()
noSkolems :: UPolytype -> Infer ()
noSkolems (Forall [Var]
xs UType
upty) = do
UType
upty' <- forall u. HasBindings u => u -> Infer u
applyBindings UType
upty
let tyvs :: Set Var
tyvs =
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> UTerm t v -> a
ucata
(forall a b. a -> b -> a
const forall a. Set a
S.empty)
(\case TyVarF Var
v -> forall a. a -> Set a
S.singleton Var
v; TypeF (Set Var)
f -> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold TypeF (Set Var)
f)
UType
upty'
ftyvs :: Set Var
ftyvs = Set Var
tyvs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Set a -> Bool
S.null Set Var
ftyvs) forall a b. (a -> b) -> a -> b
$
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
SrcLoc -> Var -> TypeErr
EscapedSkolem SrcLoc
l (forall a. [a] -> a
head (forall a. Set a -> [a]
S.toList Set Var
ftyvs))
addLocToTypeErr :: Syntax' ty -> TypeErr -> Infer a
addLocToTypeErr :: forall ty a. Syntax' ty -> TypeErr -> Infer a
addLocToTypeErr Syntax' ty
s TypeErr
te = case TypeErr
te of
Mismatch SrcLoc
NoLoc TypeF UType
a TypeF UType
b -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SrcLoc -> TypeF UType -> TypeF UType -> TypeErr
Mismatch (Syntax' ty
s forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) SrcLoc
sLoc) TypeF UType
a TypeF UType
b
TypeErr
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TypeErr
te
decomposeCmdTy :: UType -> Infer UType
decomposeCmdTy :: UType -> Infer UType
decomposeCmdTy (UTyCmd UType
a) = forall (m :: * -> *) a. Monad m => a -> m a
return UType
a
decomposeCmdTy UType
ty = do
UType
a <- Infer UType
fresh
UType
_ <- UType
ty UType -> UType -> Infer UType
=:= UType -> UType
UTyCmd UType
a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
a
decomposeFunTy :: UType -> Infer (UType, UType)
decomposeFunTy :: UType -> Infer (UType, UType)
decomposeFunTy (UTyFun UType
ty1 UType
ty2) = forall (m :: * -> *) a. Monad m => a -> m a
return (UType
ty1, UType
ty2)
decomposeFunTy UType
ty = do
UType
ty1 <- Infer UType
fresh
UType
ty2 <- Infer UType
fresh
UType
_ <- UType
ty UType -> UType -> Infer UType
=:= UType -> UType -> UType
UTyFun UType
ty1 UType
ty2
forall (m :: * -> *) a. Monad m => a -> m a
return (UType
ty1, UType
ty2)
inferConst :: Const -> Polytype
inferConst :: Const -> Polytype
inferConst Const
c = case Const
c of
Const
Wait -> [tyQ| int -> cmd unit |]
Const
Noop -> [tyQ| cmd unit |]
Const
Selfdestruct -> [tyQ| cmd unit |]
Const
Move -> [tyQ| cmd unit |]
Const
Turn -> [tyQ| dir -> cmd unit |]
Const
Grab -> [tyQ| cmd text |]
Const
Harvest -> [tyQ| cmd text |]
Const
Place -> [tyQ| text -> cmd unit |]
Const
Give -> [tyQ| actor -> text -> cmd unit |]
Const
Equip -> [tyQ| text -> cmd unit |]
Const
Unequip -> [tyQ| text -> cmd unit |]
Const
Make -> [tyQ| text -> cmd unit |]
Const
Has -> [tyQ| text -> cmd bool |]
Const
Equipped -> [tyQ| text -> cmd bool |]
Const
Count -> [tyQ| text -> cmd int |]
Const
Reprogram -> [tyQ| actor -> {cmd a} -> cmd unit |]
Const
Build -> [tyQ| {cmd a} -> cmd actor |]
Const
Drill -> [tyQ| dir -> cmd unit |]
Const
Salvage -> [tyQ| cmd unit |]
Const
Say -> [tyQ| text -> cmd unit |]
Const
Listen -> [tyQ| cmd text |]
Const
Log -> [tyQ| text -> cmd unit |]
Const
View -> [tyQ| actor -> cmd unit |]
Const
Appear -> [tyQ| text -> cmd unit |]
Const
Create -> [tyQ| text -> cmd unit |]
Const
Time -> [tyQ| cmd int |]
Const
Whereami -> [tyQ| cmd (int * int) |]
Const
Heading -> [tyQ| cmd dir |]
Const
Blocked -> [tyQ| cmd bool |]
Const
Scan -> [tyQ| dir -> cmd (unit + text) |]
Const
Upload -> [tyQ| actor -> cmd unit |]
Const
Ishere -> [tyQ| text -> cmd bool |]
Const
Isempty -> [tyQ| cmd bool |]
Const
Self -> [tyQ| actor |]
Const
Parent -> [tyQ| actor |]
Const
Base -> [tyQ| actor |]
Const
Meet -> [tyQ| cmd (unit + actor) |]
Const
MeetAll -> [tyQ| (b -> actor -> cmd b) -> b -> cmd b |]
Const
Whoami -> [tyQ| cmd text |]
Const
Setname -> [tyQ| text -> cmd unit |]
Const
Random -> [tyQ| int -> cmd int |]
Const
Run -> [tyQ| text -> cmd unit |]
Const
If -> [tyQ| bool -> {a} -> {a} -> a |]
Const
Inl -> [tyQ| a -> a + b |]
Const
Inr -> [tyQ| b -> a + b |]
Const
Case -> [tyQ|a + b -> (a -> c) -> (b -> c) -> c |]
Const
Fst -> [tyQ| a * b -> a |]
Const
Snd -> [tyQ| a * b -> b |]
Const
Force -> [tyQ| {a} -> a |]
Const
Return -> [tyQ| a -> cmd a |]
Const
Try -> [tyQ| {cmd a} -> {cmd a} -> cmd a |]
Const
Undefined -> [tyQ| a |]
Const
Fail -> [tyQ| text -> a |]
Const
Not -> [tyQ| bool -> bool |]
Const
Neg -> [tyQ| int -> int |]
Const
Eq -> Polytype
cmpBinT
Const
Neq -> Polytype
cmpBinT
Const
Lt -> Polytype
cmpBinT
Const
Gt -> Polytype
cmpBinT
Const
Leq -> Polytype
cmpBinT
Const
Geq -> Polytype
cmpBinT
Const
And -> [tyQ| bool -> bool -> bool|]
Const
Or -> [tyQ| bool -> bool -> bool|]
Const
Add -> Polytype
arithBinT
Const
Sub -> Polytype
arithBinT
Const
Mul -> Polytype
arithBinT
Const
Div -> Polytype
arithBinT
Const
Exp -> Polytype
arithBinT
Const
Format -> [tyQ| a -> text |]
Const
Concat -> [tyQ| text -> text -> text |]
Const
Chars -> [tyQ| text -> int |]
Const
Split -> [tyQ| int -> text -> (text * text) |]
Const
CharAt -> [tyQ| int -> text -> int |]
Const
ToChar -> [tyQ| int -> text |]
Const
AppF -> [tyQ| (a -> b) -> a -> b |]
Const
Swap -> [tyQ| text -> cmd text |]
Const
Atomic -> [tyQ| cmd a -> cmd a |]
Const
Teleport -> [tyQ| actor -> (int * int) -> cmd unit |]
Const
As -> [tyQ| actor -> {cmd a} -> cmd a |]
Const
RobotNamed -> [tyQ| text -> cmd actor |]
Const
RobotNumbered -> [tyQ| int -> cmd actor |]
Const
Knows -> [tyQ| text -> cmd bool |]
where
cmpBinT :: Polytype
cmpBinT = [tyQ| a -> a -> bool |]
arithBinT :: Polytype
arithBinT = [tyQ| int -> int -> int |]
check :: Syntax -> UType -> Infer (Syntax' UType)
check :: Syntax
-> UType
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
check Syntax
t UType
ty = do
Syntax' SrcLoc
l Term' UType
t' UType
ty' <- Syntax
-> ReaderT
UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) (Syntax' UType)
infer Syntax
t
UType
theTy <- UType
ty UType -> UType -> Infer UType
=:= UType
ty'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l Term' UType
t' UType
theTy
validAtomic :: Syntax -> Infer ()
validAtomic :: Syntax -> Infer ()
validAtomic s :: Syntax
s@(Syntax SrcLoc
l Term
t) = do
Int
n <- Set Var -> Syntax -> Infer Int
analyzeAtomic forall a. Set a
S.empty Syntax
s
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Ord a => a -> a -> Bool
> Int
1) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SrcLoc -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic SrcLoc
l (Int -> InvalidAtomicReason
TooManyTicks Int
n) Term
t)
analyzeAtomic :: Set Var -> Syntax -> Infer Int
analyzeAtomic :: Set Var -> Syntax -> Infer Int
analyzeAtomic Set Var
locals (Syntax SrcLoc
l Term
t) = case Term
t of
TUnit {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TDir {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TInt {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TAntiInt {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TText {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TAntiText {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TBool {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TRobot {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TRequireDevice {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TRequire {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TConst Const
c
| Const
c forall a. Eq a => a -> a -> Bool
== Const
Atomic -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SrcLoc -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic SrcLoc
l InvalidAtomicReason
NestedAtomic Term
t
| Const -> Bool
isLong Const
c -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SrcLoc -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic SrcLoc
l InvalidAtomicReason
LongConst Term
t
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Const -> Bool
isTangible Const
c then Int
1 else Int
0
TConst Const
If :$: Syntax
tst :$: Syntax
thn :$: Syntax
els ->
forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> Infer Int
analyzeAtomic Set Var
locals Syntax
tst forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. Ord a => a -> a -> a
max forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> Infer Int
analyzeAtomic Set Var
locals Syntax
thn forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> Infer Int
analyzeAtomic Set Var
locals Syntax
els)
SPair Syntax
s1 Syntax
s2 -> forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> Infer Int
analyzeAtomic Set Var
locals Syntax
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> Infer Int
analyzeAtomic Set Var
locals Syntax
s2
SApp Syntax
s1 Syntax
s2 -> forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> Infer Int
analyzeAtomic Set Var
locals Syntax
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> Infer Int
analyzeAtomic Set Var
locals Syntax
s2
SDelay DelayType
_ Syntax
s1 -> Set Var -> Syntax -> Infer Int
analyzeAtomic Set Var
locals Syntax
s1
SBind Maybe LocVar
mx Syntax
s1 Syntax
s2 -> forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> Infer Int
analyzeAtomic Set Var
locals Syntax
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> Infer Int
analyzeAtomic (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id (forall a. Ord a => a -> Set a -> Set a
S.insert forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx Set Var
locals) Syntax
s2
TVar Var
x
| Var
x forall a. Ord a => a -> Set a -> Bool
`S.member` Set Var
locals -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
| Bool
otherwise -> do
Maybe UPolytype
mxTy <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall t. Var -> Ctx t -> Maybe t
Ctx.lookup Var
x
case Maybe UPolytype
mxTy of
Maybe UPolytype
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
Just UPolytype
xTy -> do
UPolytype
xTy' <- forall u. HasBindings u => u -> Infer u
applyBindings UPolytype
xTy
if UPolytype -> Bool
isSimpleUPolytype UPolytype
xTy'
then forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
else forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SrcLoc -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic SrcLoc
l (Var -> UPolytype -> InvalidAtomicReason
NonSimpleVarType Var
x UPolytype
xTy') Term
t)
SLam {} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SrcLoc -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic SrcLoc
l InvalidAtomicReason
AtomicDupingThing Term
t)
SLet {} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SrcLoc -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic SrcLoc
l InvalidAtomicReason
AtomicDupingThing Term
t)
SDef {} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SrcLoc -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic SrcLoc
l InvalidAtomicReason
AtomicDupingThing Term
t)
TRef {} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SrcLoc -> Term -> TypeErr
CantInfer SrcLoc
l Term
t)
isSimpleUPolytype :: UPolytype -> Bool
isSimpleUPolytype :: UPolytype -> Bool
isSimpleUPolytype (Forall [] UType
ty) = UType -> Bool
isSimpleUType UType
ty
isSimpleUPolytype UPolytype
_ = Bool
False
isSimpleUType :: UType -> Bool
isSimpleUType :: UType -> Bool
isSimpleUType = \case
UTyBase {} -> Bool
True
UTyVar {} -> Bool
False
UTySum UType
ty1 UType
ty2 -> UType -> Bool
isSimpleUType UType
ty1 Bool -> Bool -> Bool
&& UType -> Bool
isSimpleUType UType
ty2
UTyProd UType
ty1 UType
ty2 -> UType -> Bool
isSimpleUType UType
ty1 Bool -> Bool -> Bool
&& UType -> Bool
isSimpleUType UType
ty2
UTyFun {} -> Bool
False
UTyCmd {} -> Bool
False
UTyDelay {} -> Bool
False
UVar {} -> Bool
False
UTerm {} -> Bool
False