{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Swarm.Language.Typecheck (
TypeErr (..),
InvalidAtomicReason (..),
getTypeErrLocation,
Infer,
runInfer,
lookup,
fresh,
substU,
(=:=),
HasBindings (..),
instantiate,
skolemize,
generalize,
inferTop,
inferModule,
infer,
inferConst,
check,
decomposeCmdTy,
decomposeFunTy,
) where
import Control.Category ((>>>))
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.Foldable (fold)
import Data.Functor.Identity
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.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 UType
uty UCtx
uctx) -> forall s t. s -> Ctx t -> Module s t
Module forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall t. WithU t => U t -> t
fromU forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UType -> Infer UPolytype
generalize UType
uty) 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 :: Location -> Var -> Infer UType
lookup :: Location -> Var -> Infer UType
lookup Location
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
$ Location -> Var -> TypeErr
UnboundVar Location
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
s =:= :: UType -> UType -> Infer ()
=:= UType
t = forall (f :: * -> *) a. Functor f => f a -> f ()
void (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 UModule where
applyBindings :: UModule -> Infer UModule
applyBindings (Module UType
uty UCtx
uctx) = forall s t. 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 UType
uty 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 Location Var
|
EscapedSkolem Location Var
| Infinite IntVar UType
|
Mismatch Location (TypeF UType) (TypeF UType)
|
DefNotTopLevel Location Term
|
CantInfer Location Term
|
InvalidAtomic Location 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 = Location -> TypeF UType -> TypeF UType -> TypeErr
Mismatch Location
NoLoc
getTypeErrLocation :: TypeErr -> Maybe Location
getTypeErrLocation :: TypeErr -> Maybe Location
getTypeErrLocation TypeErr
te = case TypeErr
te of
UnboundVar Location
l Var
_ -> forall a. a -> Maybe a
Just Location
l
EscapedSkolem Location
l Var
_ -> forall a. a -> Maybe a
Just Location
l
Infinite IntVar
_ UType
_ -> forall a. Maybe a
Nothing
Mismatch Location
l TypeF UType
_ TypeF UType
_ -> forall a. a -> Maybe a
Just Location
l
DefNotTopLevel Location
l Term
_ -> forall a. a -> Maybe a
Just Location
l
CantInfer Location
l Term
_ -> forall a. a -> Maybe a
Just Location
l
InvalidAtomic Location
l InvalidAtomicReason
_ Term
_ -> forall a. a -> Maybe a
Just Location
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 Location
_ Term
t) = (forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall a. Syntax -> TypeErr -> Infer a
addLocToTypeErr Syntax
s) forall a b. (a -> b) -> a -> b
$ case Term
t of
SDef Bool
_ Var
x Maybe Polytype
Nothing Syntax
t1 -> do
UType
xTy <- Infer UType
fresh
UType
ty <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding Var
x (forall t. [Var] -> t -> Poly t
Forall [] UType
xTy) forall a b. (a -> b) -> a -> b
$ Syntax -> Infer UType
infer Syntax
t1
UType
xTy UType -> UType -> Infer ()
=:= UType
ty
UPolytype
pty <- UType -> Infer UPolytype
generalize UType
ty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s t. s -> Ctx t -> Module s t
Module (UType -> UType
UTyCmd UType
UTyUnit) (forall t. Var -> t -> Ctx t
singleton Var
x UPolytype
pty)
SDef Bool
_ Var
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
forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding Var
x UPolytype
upty forall a b. (a -> b) -> a -> b
$ Syntax -> UType -> Infer ()
check Syntax
t1 UType
uty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s t. s -> Ctx t -> Module s t
Module (UType -> UType
UTyCmd UType
UTyUnit) (forall t. Var -> t -> Ctx t
singleton Var
x UPolytype
upty)
SBind Maybe Var
mx Syntax
c1 Syntax
c2 -> do
Module UType
cmda UCtx
ctx1 <- Syntax -> Infer UModule
inferModule Syntax
c1
UType
a <- UType -> Infer UType
decomposeCmdTy UType
cmda
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) Maybe Var
mx forall a b. (a -> b) -> a -> b
$ do
Module UType
cmdb UCtx
ctx2 <- Syntax -> Infer UModule
inferModule Syntax
c2
UType
_ <- UType -> Infer UType
decomposeCmdTy UType
cmdb
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) Maybe Var
mx
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s t. s -> Ctx t -> Module s t
Module UType
cmdb (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. s -> Module s t
trivMod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Syntax -> Infer UType
infer Syntax
s
infer :: Syntax -> Infer UType
infer :: Syntax -> Infer UType
infer s :: Syntax
s@(Syntax Location
l Term
t) = (forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall a. Syntax -> 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 UType
UTyUnit
TConst Const
c -> 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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTyDir
TInt Integer
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTyInt
TAntiInt Var
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTyInt
TText Var
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTyText
TAntiText Var
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTyText
TBool Bool
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTyBool
TRobot Int
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return UType
UTyRobot
TRef Int
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Location -> Term -> TypeErr
CantInfer Location
l Term
t
TRequireDevice Var
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UType -> UType
UTyCmd UType
UTyUnit
TRequire Int
_ Var
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UType -> UType
UTyCmd UType
UTyUnit
SPair Syntax
t1 Syntax
t2 -> UType -> UType -> UType
UTyProd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Syntax -> Infer UType
infer Syntax
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Syntax -> Infer UType
infer Syntax
t2
SDelay DelayType
_ Syntax
dt -> UType -> UType
UTyDelay forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Syntax -> Infer UType
infer Syntax
dt
TConst Const
Atomic :$: Syntax
at -> do
UType
argTy <- Infer UType
fresh
Syntax -> UType -> Infer ()
check Syntax
at (UType -> UType
UTyCmd UType
argTy)
Syntax -> Infer ()
validAtomic Syntax
at
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UType -> UType
UTyCmd UType
argTy
TVar Var
x -> Location -> Var -> Infer UType
lookup Location
l Var
x
SLam Var
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
UType
resTy <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding Var
x (forall t. [Var] -> t -> Poly t
Forall [] UType
uargTy) forall a b. (a -> b) -> a -> b
$ Syntax -> Infer UType
infer Syntax
lt
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UType -> UType -> UType
UTyFun UType
uargTy UType
resTy
SLam Var
x Maybe (Fix TypeF)
Nothing Syntax
lt -> do
UType
argTy <- Infer UType
fresh
UType
resTy <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding Var
x (forall t. [Var] -> t -> Poly t
Forall [] UType
argTy) forall a b. (a -> b) -> a -> b
$ Syntax -> Infer UType
infer Syntax
lt
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UType -> UType -> UType
UTyFun UType
argTy UType
resTy
SApp Syntax
f Syntax
x -> do
UType
fTy <- Syntax -> Infer UType
infer Syntax
f
(UType
ty1, UType
ty2) <- UType -> Infer (UType, UType)
decomposeFunTy UType
fTy
Syntax -> UType -> Infer ()
check Syntax
x UType
ty1 forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall a. Syntax -> TypeErr -> Infer a
addLocToTypeErr Syntax
x
forall (m :: * -> *) a. Monad m => a -> m a
return UType
ty2
SLet Bool
_ Var
x Maybe Polytype
Nothing Syntax
t1 Syntax
t2 -> do
UType
xTy <- Infer UType
fresh
UType
uty <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding Var
x (forall t. [Var] -> t -> Poly t
Forall [] UType
xTy) forall a b. (a -> b) -> a -> b
$ Syntax -> Infer UType
infer Syntax
t1
UType
xTy UType -> UType -> Infer ()
=:= UType
uty
UPolytype
upty <- UType -> Infer UPolytype
generalize UType
uty
forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding Var
x UPolytype
upty forall a b. (a -> b) -> a -> b
$ Syntax -> Infer UType
infer Syntax
t2
SLet Bool
_ Var
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
UType
resTy <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding Var
x UPolytype
upty forall a b. (a -> b) -> a -> b
$ do
Syntax -> UType -> Infer ()
check Syntax
t1 UType
uty forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall a. Syntax -> TypeErr -> Infer a
addLocToTypeErr Syntax
t1
Syntax -> Infer 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 UType
resTy
SDef {} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Location -> Term -> TypeErr
DefNotTopLevel Location
l Term
t
SBind Maybe Var
mx Syntax
c1 Syntax
c2 -> do
UType
ty1 <- Syntax -> Infer UType
infer Syntax
c1
UType
a <- UType -> Infer UType
decomposeCmdTy UType
ty1
UType
ty2 <- 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) Maybe Var
mx forall a b. (a -> b) -> a -> b
$ Syntax -> Infer UType
infer Syntax
c2
UType
_ <- UType -> Infer UType
decomposeCmdTy UType
ty2
forall (m :: * -> *) a. Monad m => a -> m a
return UType
ty2
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
$ Location -> Var -> TypeErr
EscapedSkolem Location
l (forall a. [a] -> a
head (forall a. Set a -> [a]
S.toList Set Var
ftyvs))
addLocToTypeErr :: Syntax -> TypeErr -> Infer a
addLocToTypeErr :: forall a. Syntax -> TypeErr -> Infer a
addLocToTypeErr Syntax
s TypeErr
te = case TypeErr
te of
Mismatch Location
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
$ Location -> TypeF UType -> TypeF UType -> TypeErr
Mismatch (Syntax -> Location
sLoc Syntax
s) 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
ty UType -> UType -> Infer ()
=:= 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
ty UType -> UType -> Infer ()
=:= 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| robot -> text -> cmd unit |]
Const
Install -> [tyQ| robot -> text -> cmd unit |]
Const
Make -> [tyQ| text -> cmd unit |]
Const
Has -> [tyQ| text -> cmd bool |]
Const
Installed -> [tyQ| text -> cmd bool |]
Const
Count -> [tyQ| text -> cmd int |]
Const
Reprogram -> [tyQ| robot -> {cmd a} -> cmd unit |]
Const
Build -> [tyQ| {cmd a} -> cmd robot |]
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| robot -> 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
Blocked -> [tyQ| cmd bool |]
Const
Scan -> [tyQ| dir -> cmd (unit + text) |]
Const
Upload -> [tyQ| robot -> cmd unit |]
Const
Ishere -> [tyQ| text -> cmd bool |]
Const
Self -> [tyQ| robot |]
Const
Parent -> [tyQ| robot |]
Const
Base -> [tyQ| robot |]
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
AppF -> [tyQ| (a -> b) -> a -> b |]
Const
Swap -> [tyQ| text -> cmd text |]
Const
Atomic -> [tyQ| cmd a -> cmd a |]
Const
Teleport -> [tyQ| robot -> (int * int) -> cmd unit |]
Const
As -> [tyQ| robot -> {cmd a} -> cmd a |]
Const
RobotNamed -> [tyQ| text -> cmd robot |]
Const
RobotNumbered -> [tyQ| int -> cmd robot |]
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 ()
check :: Syntax -> UType -> Infer ()
check Syntax
t UType
ty = do
UType
ty' <- Syntax -> Infer UType
infer Syntax
t
()
_ <- UType
ty UType -> UType -> Infer ()
=:= UType
ty'
forall (m :: * -> *) a. Monad m => a -> m a
return ()
validAtomic :: Syntax -> Infer ()
validAtomic :: Syntax -> Infer ()
validAtomic s :: Syntax
s@(Syntax Location
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 (Location -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic Location
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 Location
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
$ Location -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic Location
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
$ Location -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic Location
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 Var
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 Maybe Var
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 (Location -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic Location
l (Var -> UPolytype -> InvalidAtomicReason
NonSimpleVarType Var
x UPolytype
xTy') Term
t)
SLam {} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Location -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic Location
l InvalidAtomicReason
AtomicDupingThing Term
t)
SLet {} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Location -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic Location
l InvalidAtomicReason
AtomicDupingThing Term
t)
SDef {} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Location -> InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic Location
l InvalidAtomicReason
AtomicDupingThing Term
t)
TRef {} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Location -> Term -> TypeErr
CantInfer Location
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