{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}

-- | Check definition bodies.
--
-- Simple first-order type-checking for the bodies of @define@d constructors.

module BNFC.Check.Expressions ( checkFunction ) where

import BNFC.Prelude
import Lens.Micro.TH (makeLensesFor)

import qualified Data.Map         as Map
import qualified BNFC.Utils.List1 as List1

import qualified BNFC.Abs as A
import BNFC.Abs (HasPosition(..))
import BNFC.CF
import BNFC.Types.Position

import BNFC.Check.Monad


-- | State of the type checker.

data Env = Env
  { Env -> Signature
_envSignature :: Signature
      -- ^ The function types of labels and definitions.

  , Env -> Context
_envContext   :: Context
      -- ^ The base types of definition parameters.

  , Env -> Position
_envPosition  :: Position
      -- ^ The current position.
  }
  deriving (Int -> Env -> ShowS
[Env] -> ShowS
Env -> String
(Int -> Env -> ShowS)
-> (Env -> String) -> ([Env] -> ShowS) -> Show Env
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Env] -> ShowS
$cshowList :: [Env] -> ShowS
show :: Env -> String
$cshow :: Env -> String
showsPrec :: Int -> Env -> ShowS
$cshowsPrec :: Int -> Env -> ShowS
Show)

-- | Typing context, mapping parameters to their type.

type Context = Map VarName Type

-- @makeLenses ''Env@ will generate unused definitions if not all lenses are used
makeLensesFor (map (\ s -> ('_':s, s)) ["envSignature", "envContext"]) ''Env

-- | Entry point to check contents of a 'A.Function'.

checkFunction :: Position -> Signature -> LabelName -> [A.Arg] -> A.Exp -> FunType -> Check Function
checkFunction :: Position
-> Signature
-> LabelName
-> [Arg]
-> Exp
-> FunType
-> Check Function
checkFunction Position
p Signature
sig LabelName
_f [Arg]
params0 Exp
exp0 (FunType Type
t [Type]
ts) = Position -> Check Function -> Check Function
forall (m :: * -> *) p a.
(MonadCheck m, ToPosition' p) =>
p -> m a -> m a
atPosition Position
p (Check Function -> Check Function)
-> Check Function -> Check Function
forall a b. (a -> b) -> a -> b
$ do
  ([Parameter]
params, Context
cxt) <- [Arg] -> [Type] -> StateT Context Check [Parameter]
checkParameters [Arg]
params0 [Type]
ts StateT Context Check [Parameter]
-> Context -> Check ([Parameter], Context)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` Context
forall a. Monoid a => a
mempty
  -- let cxt = Map.fromList $ params <&> \ (Parameter x t) -> (x,t)
  Exp
exp    <- Type -> Exp -> ReaderT Env Check Exp
checkExp Type
t Exp
exp0 ReaderT Env Check Exp -> Env -> Check Exp
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` Signature -> Context -> Position -> Env
Env Signature
sig Context
cxt Position
p
  Function -> Check Function
forall (m :: * -> *) a. Monad m => a -> m a
return (Function -> Check Function) -> Function -> Check Function
forall a b. (a -> b) -> a -> b
$ [Parameter] -> Exp -> Type -> Function
Function [Parameter]
params Exp
exp Type
t

-- | Build a typing context from a list of parameters and their types.
--   If the list do not have equal length, report an error and try to
--   patch the situation.

checkParameters :: [A.Arg] -> [Type] -> StateT Context Check [Parameter]
checkParameters :: [Arg] -> [Type] -> StateT Context Check [Parameter]
checkParameters = (([Arg], [Type]) -> StateT Context Check [Parameter])
-> [Arg] -> [Type] -> StateT Context Check [Parameter]
forall a b c. ((a, b) -> c) -> a -> b -> c
curry ((([Arg], [Type]) -> StateT Context Check [Parameter])
 -> [Arg] -> [Type] -> StateT Context Check [Parameter])
-> (([Arg], [Type]) -> StateT Context Check [Parameter])
-> [Arg]
-> [Type]
-> StateT Context Check [Parameter]
forall a b. (a -> b) -> a -> b
$ \case
  ([]  , []) -> [Parameter] -> StateT Context Check [Parameter]
forall (m :: * -> *) a. Monad m => a -> m a
return []

  -- More parameters than types: drop the parameters.
  (Arg
a:[Arg]
as, []) -> [] [Parameter]
-> StateT Context Check () -> StateT Context Check [Parameter]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
    BNFC'Position -> StateT Context Check () -> StateT Context Check ()
forall (m :: * -> *) p a.
(MonadCheck m, ToPosition' p) =>
p -> m a -> m a
atPosition (Arg -> BNFC'Position
forall a. HasPosition a => a -> BNFC'Position
hasPosition Arg
a) (StateT Context Check () -> StateT Context Check ())
-> StateT Context Check () -> StateT Context Check ()
forall a b. (a -> b) -> a -> b
$
      RecoverableError -> StateT Context Check ()
forall (m :: * -> *). MonadCheck m => RecoverableError -> m ()
recoverableError (RecoverableError -> StateT Context Check ())
-> RecoverableError -> StateT Context Check ()
forall a b. (a -> b) -> a -> b
$ List1 Arg -> RecoverableError
DroppingSpuriousParameters (List1 Arg -> RecoverableError) -> List1 Arg -> RecoverableError
forall a b. (a -> b) -> a -> b
$ Arg
a Arg -> [Arg] -> List1 Arg
forall a. a -> [a] -> NonEmpty a
:| [Arg]
as

  -- More types than parameters: make up some dummy parameters.
  ([]  , ts :: [Type]
ts@(Type
_:[Type]
_)) -> do
    -- If there are not enough parameters given, we can make some up.
    BNFC'Position
p <- (Position -> (Int, Int)) -> Maybe Position -> BNFC'Position
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Position Int
l Int
c) -> (Int
l, Int
c)) (Maybe Position -> BNFC'Position)
-> StateT Context Check (Maybe Position)
-> StateT Context Check BNFC'Position
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT Context Check (Maybe Position)
forall (m :: * -> *). MonadCheck m => m (Maybe Position)
askPosition
    let
      xs :: [LabelName]
xs = [Int
1 .. [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts] [Int] -> (Int -> LabelName) -> [LabelName]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Int
n -> Char
'_' Char -> String -> LabelName
forall a. a -> [a] -> NonEmpty a
:| Int -> String
forall a. Show a => a -> String
show Int
n
      dummies :: [Arg]
dummies = (LabelName -> Arg) -> [LabelName] -> [Arg]
forall a b. (a -> b) -> [a] -> [b]
map (BNFC'Position -> Identifier -> Arg
forall a. a -> Identifier -> Arg' a
A.Arg BNFC'Position
p (Identifier -> Arg)
-> (LabelName -> Identifier) -> LabelName -> Arg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Int), String) -> Identifier
A.Identifier (((Int, Int), String) -> Identifier)
-> (LabelName -> ((Int, Int), String)) -> LabelName -> Identifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Int) -> BNFC'Position -> (Int, Int)
forall a. a -> Maybe a -> a
fromMaybe (Int, Int)
forall a. HasCallStack => a
panicPositionNothing BNFC'Position
p,) (String -> ((Int, Int), String))
-> (LabelName -> String) -> LabelName -> ((Int, Int), String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList) [LabelName]
xs
    RecoverableError -> StateT Context Check ()
forall (m :: * -> *). MonadCheck m => RecoverableError -> m ()
recoverableError (RecoverableError -> StateT Context Check ())
-> RecoverableError -> StateT Context Check ()
forall a b. (a -> b) -> a -> b
$ List1 LabelName -> RecoverableError
NotEnoughParameters (List1 LabelName -> RecoverableError)
-> List1 LabelName -> RecoverableError
forall a b. (a -> b) -> a -> b
$ [LabelName] -> List1 LabelName
forall a. [a] -> NonEmpty a
List1.fromList [LabelName]
xs
    [Arg] -> [Type] -> StateT Context Check [Parameter]
checkParameters [Arg]
dummies [Type]
ts

  -- Check the first parameter against the first type.
  -- If the parameter is already in the typing context, warn about shadowing.
  -- Add the parameter to the context and continue.

  (A.Arg BNFC'Position
p (A.Identifier ((Int, Int)
_, String
x0)) : [Arg]
as, Type
t:[Type]
ts) -> BNFC'Position
-> StateT Context Check [Parameter]
-> StateT Context Check [Parameter]
forall (m :: * -> *) p a.
(MonadCheck m, ToPosition' p) =>
p -> m a -> m a
atPosition BNFC'Position
p (StateT Context Check [Parameter]
 -> StateT Context Check [Parameter])
-> StateT Context Check [Parameter]
-> StateT Context Check [Parameter]
forall a b. (a -> b) -> a -> b
$ do
    let x :: LabelName
x = LabelName -> Maybe LabelName -> LabelName
forall a. a -> Maybe a -> a
fromMaybe LabelName
forall a. HasCallStack => a
panicEmptyIdentifier (Maybe LabelName -> LabelName) -> Maybe LabelName -> LabelName
forall a b. (a -> b) -> a -> b
$ String -> Maybe LabelName
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty String
x0
    -- If x is not lowercase, warn.
    Bool -> StateT Context Check () -> StateT Context Check ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Char -> Bool
isLower (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ LabelName -> Char
forall a. NonEmpty a -> a
List1.head LabelName
x) (StateT Context Check () -> StateT Context Check ())
-> StateT Context Check () -> StateT Context Check ()
forall a b. (a -> b) -> a -> b
$ Warning -> StateT Context Check ()
forall (m :: * -> *). MonadCheck m => Warning -> m ()
warn (Warning -> StateT Context Check ())
-> Warning -> StateT Context Check ()
forall a b. (a -> b) -> a -> b
$ LabelName -> Warning
ParameterShouldBeLowerCase LabelName
x
    -- If x is already in the context, warn about shadowing.
    (Type -> StateT Context Check ())
-> Maybe Type -> StateT Context Check ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (StateT Context Check () -> Type -> StateT Context Check ()
forall a b. a -> b -> a
const (StateT Context Check () -> Type -> StateT Context Check ())
-> StateT Context Check () -> Type -> StateT Context Check ()
forall a b. (a -> b) -> a -> b
$ Warning -> StateT Context Check ()
forall (m :: * -> *). MonadCheck m => Warning -> m ()
warn (Warning -> StateT Context Check ())
-> Warning -> StateT Context Check ()
forall a b. (a -> b) -> a -> b
$ LabelName -> Warning
ShadowingParameter LabelName
x) (Maybe Type -> StateT Context Check ())
-> StateT Context Check (Maybe Type) -> StateT Context Check ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Context -> Maybe Type) -> StateT Context Check (Maybe Type)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (LabelName -> Context -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LabelName
x)
    (LabelName -> Type -> Parameter
Parameter LabelName
x Type
t Parameter -> [Parameter] -> [Parameter]
forall a. a -> [a] -> [a]
:) ([Parameter] -> [Parameter])
-> StateT Context Check [Parameter]
-> StateT Context Check [Parameter]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      -- Add parameter to context, possibly overwriting the shadowed alter ego.
      (Context -> Context) -> StateT Context Check ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> StateT Context Check ())
-> (Context -> Context) -> StateT Context Check ()
forall a b. (a -> b) -> a -> b
$ LabelName -> Type -> Context -> Context
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LabelName
x Type
t
      [Arg] -> [Type] -> StateT Context Check [Parameter]
checkParameters [Arg]
as [Type]
ts

-- | Check a list of expressions against a list of types.
--   The lists are checked for the same length.

checkExps :: LabelName -> [Type] -> [A.Exp] -> ReaderT Env Check [Exp]
checkExps :: LabelName -> [Type] -> [Exp] -> ReaderT Env Check [Exp]
checkExps LabelName
x = (([Type], [Exp]) -> ReaderT Env Check [Exp])
-> [Type] -> [Exp] -> ReaderT Env Check [Exp]
forall a b c. ((a, b) -> c) -> a -> b -> c
curry ((([Type], [Exp]) -> ReaderT Env Check [Exp])
 -> [Type] -> [Exp] -> ReaderT Env Check [Exp])
-> (([Type], [Exp]) -> ReaderT Env Check [Exp])
-> [Type]
-> [Exp]
-> ReaderT Env Check [Exp]
forall a b. (a -> b) -> a -> b
$ \case
  ([]  , []  ) -> [Exp] -> ReaderT Env Check [Exp]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  ([]  , Exp
e:[Exp]
es) -> [] [Exp] -> ReaderT Env Check () -> ReaderT Env Check [Exp]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do RecoverableError -> ReaderT Env Check ()
forall (m :: * -> *). MonadCheck m => RecoverableError -> m ()
recoverableError (RecoverableError -> ReaderT Env Check ())
-> RecoverableError -> ReaderT Env Check ()
forall a b. (a -> b) -> a -> b
$ LabelName -> List1 Exp -> RecoverableError
DroppingSpuriousArguments LabelName
x (List1 Exp -> RecoverableError) -> List1 Exp -> RecoverableError
forall a b. (a -> b) -> a -> b
$ Exp
e Exp -> [Exp] -> List1 Exp
forall a. a -> [a] -> NonEmpty a
:| [Exp]
es
  (Type
t:[Type]
ts, []  ) -> [] [Exp] -> ReaderT Env Check () -> ReaderT Env Check [Exp]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do RecoverableError -> ReaderT Env Check ()
forall (m :: * -> *). MonadCheck m => RecoverableError -> m ()
recoverableError (RecoverableError -> ReaderT Env Check ())
-> RecoverableError -> ReaderT Env Check ()
forall a b. (a -> b) -> a -> b
$ LabelName -> List1 Type -> RecoverableError
MissingArguments LabelName
x (List1 Type -> RecoverableError) -> List1 Type -> RecoverableError
forall a b. (a -> b) -> a -> b
$ Type
t Type -> [Type] -> List1 Type
forall a. a -> [a] -> NonEmpty a
:| [Type]
ts
  (Type
t:[Type]
ts, Exp
e:[Exp]
es) -> (:) (Exp -> [Exp] -> [Exp])
-> ReaderT Env Check Exp -> ReaderT Env Check ([Exp] -> [Exp])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Exp -> ReaderT Env Check Exp
checkExp Type
t Exp
e ReaderT Env Check ([Exp] -> [Exp])
-> ReaderT Env Check [Exp] -> ReaderT Env Check [Exp]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> LabelName -> [Type] -> [Exp] -> ReaderT Env Check [Exp]
checkExps LabelName
x [Type]
ts [Exp]
es

-- | Check an LBNF expression against the given type and return the
--   expression in internal representation.

checkExp :: Type -> A.Exp -> ReaderT Env Check Exp
checkExp :: Type -> Exp -> ReaderT Env Check Exp
checkExp Type
t = \case
    A.App BNFC'Position
p0 (A.Identifier ((Int, Int)
_, String
x0)) [Exp]
es0 -> BNFC'Position -> ReaderT Env Check Exp -> ReaderT Env Check Exp
forall (m :: * -> *) p a.
(MonadCheck m, ToPosition' p) =>
p -> m a -> m a
atPosition BNFC'Position
p0 (ReaderT Env Check Exp -> ReaderT Env Check Exp)
-> ReaderT Env Check Exp -> ReaderT Env Check Exp
forall a b. (a -> b) -> a -> b
$ do
      let x :: LabelName
x = LabelName -> Maybe LabelName -> LabelName
forall a. a -> Maybe a -> a
fromMaybe LabelName
forall a. HasCallStack => a
panicEmptyIdentifier (Maybe LabelName -> LabelName) -> Maybe LabelName -> LabelName
forall a b. (a -> b) -> a -> b
$ String -> Maybe LabelName
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty String
x0
      LabelName -> ReaderT Env Check ()
forall (m :: * -> *).
(MonadCheck m, MonadReader Env m) =>
LabelName -> m ()
warnIfShadowed LabelName
x
      ft :: FunType
ft@(FunType Type
t' [Type]
ts) <- LabelName -> ReaderT Env Check FunType
forall (m :: * -> *).
(MonadReader Env m, MonadCheck m) =>
LabelName -> m FunType
lookupSig LabelName
x
      Type -> ReaderT Env Check ()
forall (m :: * -> *). MonadCheck m => Type -> m ()
inferred Type
t'
      Label -> FunType -> [Exp] -> Exp
App (LabelName -> Label
labelFromIdentifier LabelName
x) FunType
ft ([Exp] -> Exp) -> ReaderT Env Check [Exp] -> ReaderT Env Check Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LabelName -> [Type] -> [Exp] -> ReaderT Env Check [Exp]
checkExps LabelName
x [Type]
ts [Exp]
es0

    A.Var BNFC'Position
p0 (A.Identifier ((Int, Int)
_, String
x0)) -> BNFC'Position -> ReaderT Env Check Exp -> ReaderT Env Check Exp
forall (m :: * -> *) p a.
(MonadCheck m, ToPosition' p) =>
p -> m a -> m a
atPosition BNFC'Position
p0 (ReaderT Env Check Exp -> ReaderT Env Check Exp)
-> ReaderT Env Check Exp -> ReaderT Env Check Exp
forall a b. (a -> b) -> a -> b
$ do
      let x :: LabelName
x = LabelName -> Maybe LabelName -> LabelName
forall a. a -> Maybe a -> a
fromMaybe LabelName
forall a. HasCallStack => a
panicEmptyIdentifier (Maybe LabelName -> LabelName) -> Maybe LabelName -> LabelName
forall a b. (a -> b) -> a -> b
$ String -> Maybe LabelName
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty String
x0
      LabelName -> ReaderT Env Check (Maybe Type)
forall (f :: * -> *).
MonadReader Env f =>
LabelName -> f (Maybe Type)
lookupCxt LabelName
x ReaderT Env Check (Maybe Type)
-> (Maybe Type -> ReaderT Env Check Exp) -> ReaderT Env Check Exp
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just Type
t' -> Type -> ReaderT Env Check ()
forall (m :: * -> *). MonadCheck m => Type -> m ()
inferred Type
t' ReaderT Env Check () -> Exp -> ReaderT Env Check Exp
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Parameter -> Exp
Var (LabelName -> Type -> Parameter
Parameter LabelName
x Type
t)
        Maybe Type
Nothing -> do
          ft :: FunType
ft@(FunType Type
t' [Type]
ts) <- LabelName -> ReaderT Env Check FunType
forall (m :: * -> *).
(MonadReader Env m, MonadCheck m) =>
LabelName -> m FunType
lookupSig LabelName
x
          -- If this is a proper function type, then we are missing arguments
          (List1 Type -> ReaderT Env Check ())
-> Maybe (List1 Type) -> ReaderT Env Check ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (RecoverableError -> ReaderT Env Check ()
forall (m :: * -> *). MonadCheck m => RecoverableError -> m ()
recoverableError (RecoverableError -> ReaderT Env Check ())
-> (List1 Type -> RecoverableError)
-> List1 Type
-> ReaderT Env Check ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelName -> List1 Type -> RecoverableError
MissingArguments LabelName
x) (Maybe (List1 Type) -> ReaderT Env Check ())
-> Maybe (List1 Type) -> ReaderT Env Check ()
forall a b. (a -> b) -> a -> b
$ [Type] -> Maybe (List1 Type)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [Type]
ts
          Type -> ReaderT Env Check ()
forall (m :: * -> *). MonadCheck m => Type -> m ()
inferred Type
t' ReaderT Env Check () -> Exp -> ReaderT Env Check Exp
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Label -> FunType -> [Exp] -> Exp
App (LabelName -> Label
labelFromIdentifier LabelName
x) FunType
ft []

    A.Cons BNFC'Position
p0 Exp
e0 Exp
es0 -> BNFC'Position -> ReaderT Env Check Exp -> ReaderT Env Check Exp
forall (m :: * -> *) p a.
(MonadCheck m, ToPosition' p) =>
p -> m a -> m a
atPosition BNFC'Position
p0 (ReaderT Env Check Exp -> ReaderT Env Check Exp)
-> ReaderT Env Check Exp -> ReaderT Env Check Exp
forall a b. (a -> b) -> a -> b
$ do
      (Type -> ReaderT Env Check Exp) -> ReaderT Env Check Exp
forall (m :: * -> *) a. MonadCheck m => (Type -> m a) -> m a
elemType ((Type -> ReaderT Env Check Exp) -> ReaderT Env Check Exp)
-> (Type -> ReaderT Env Check Exp) -> ReaderT Env Check Exp
forall a b. (a -> b) -> a -> b
$ \ Type
s -> do
        Exp
e <- Type -> Exp -> ReaderT Env Check Exp
checkExp Type
s Exp
e0
        Type -> Exp -> Exp -> Exp
cons Type
s Exp
e (Exp -> Exp) -> ReaderT Env Check Exp -> ReaderT Env Check Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Exp -> ReaderT Env Check Exp
checkExp Type
t Exp
es0

    A.List BNFC'Position
p0 [Exp]
es0    -> BNFC'Position -> ReaderT Env Check Exp -> ReaderT Env Check Exp
forall (m :: * -> *) p a.
(MonadCheck m, ToPosition' p) =>
p -> m a -> m a
atPosition BNFC'Position
p0 (ReaderT Env Check Exp -> ReaderT Env Check Exp)
-> ReaderT Env Check Exp -> ReaderT Env Check Exp
forall a b. (a -> b) -> a -> b
$ do
      (Type -> ReaderT Env Check Exp) -> ReaderT Env Check Exp
forall (m :: * -> *) a. MonadCheck m => (Type -> m a) -> m a
elemType ((Type -> ReaderT Env Check Exp) -> ReaderT Env Check Exp)
-> (Type -> ReaderT Env Check Exp) -> ReaderT Env Check Exp
forall a b. (a -> b) -> a -> b
$ \ Type
s -> do
        (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Exp -> Exp -> Exp
cons Type
s) Exp
nil ([Exp] -> Exp) -> ReaderT Env Check [Exp] -> ReaderT Env Check Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> ReaderT Env Check Exp) -> [Exp] -> ReaderT Env Check [Exp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> Exp -> ReaderT Env Check Exp
checkExp Type
s) [Exp]
es0

    A.LitInteger BNFC'Position
_ Integer
l   -> Type -> ReaderT Env Check ()
forall (m :: * -> *). MonadCheck m => Type -> m ()
inferred Type
tInteger ReaderT Env Check () -> Exp -> ReaderT Env Check Exp
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Integer -> Exp
LitInteger Integer
l
    A.LitDouble  BNFC'Position
_ Double
l   -> Type -> ReaderT Env Check ()
forall (m :: * -> *). MonadCheck m => Type -> m ()
inferred Type
tDouble  ReaderT Env Check () -> Exp -> ReaderT Env Check Exp
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Double -> Exp
LitDouble Double
l
    A.LitChar    BNFC'Position
_ Char
l   -> Type -> ReaderT Env Check ()
forall (m :: * -> *). MonadCheck m => Type -> m ()
inferred Type
tChar    ReaderT Env Check () -> Exp -> ReaderT Env Check Exp
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Char -> Exp
LitChar Char
l
    A.LitString  BNFC'Position
_ String
l   -> Type -> ReaderT Env Check ()
forall (m :: * -> *). MonadCheck m => Type -> m ()
inferred Type
tString  ReaderT Env Check () -> Exp -> ReaderT Env Check Exp
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> String -> Exp
LitString String
l
  where
  -- Match inferred type against ascribed type.
  inferred :: Type -> m ()
inferred Type
t'
    | Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t'   = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
otherwise = RecoverableError -> m ()
forall (m :: * -> *). MonadCheck m => RecoverableError -> m ()
recoverableError (RecoverableError -> m ()) -> RecoverableError -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> RecoverableError
ExpectedVsInferredType Type
t Type
t'
  -- Check whether the ascribed type is a list type.
  elemType :: (Type -> m a) -> m a
elemType Type -> m a
k =
    case Type
t of
      ListType Type
s -> Type -> m a
k Type
s
      BaseType{} -> FatalError -> m a
forall (m :: * -> *) a. MonadCheck m => FatalError -> m a
fatalError (FatalError -> m a) -> FatalError -> m a
forall a b. (a -> b) -> a -> b
$ Type -> FatalError
ListsDontInhabitType Type
t
  -- List constructors
  nil :: Exp
nil = Label -> FunType -> [Exp] -> Exp
App Label
LNil (Type -> [Type] -> FunType
FunType Type
t []) []
  -- Precondition to cons: t == ListT s
  cons :: Type -> Exp -> Exp -> Exp
cons Type
s Exp
e Exp
es = Label -> FunType -> [Exp] -> Exp
App Label
LCons (Type -> [Type] -> FunType
FunType Type
t [Type
s,Type
t]) [Exp
e,Exp
es]

  lookupCxt :: LabelName -> f (Maybe Type)
lookupCxt LabelName
x = LabelName -> Context -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LabelName
x (Context -> Maybe Type) -> f Context -> f (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting Context Env Context -> f Context
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Context Env Context
Lens' Env Context
envContext
  lookupSig :: LabelName -> m FunType
lookupSig LabelName
x = do
    (LabelName -> Signature -> Maybe (WithPosition FunType)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LabelName
x (Signature -> Maybe (WithPosition FunType))
-> m Signature -> m (Maybe (WithPosition FunType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting Signature Env Signature -> m Signature
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Signature Env Signature
Lens' Env Signature
envSignature) m (Maybe (WithPosition FunType))
-> (Maybe (WithPosition FunType) -> m FunType) -> m FunType
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe (WithPosition FunType)
Nothing                  -> FatalError -> m FunType
forall (m :: * -> *) a. MonadCheck m => FatalError -> m a
fatalError (FatalError -> m FunType) -> FatalError -> m FunType
forall a b. (a -> b) -> a -> b
$ LabelName -> FatalError
UndefinedLabel LabelName
x
      Just (WithPosition Position
_ FunType
ft) -> FunType -> m FunType
forall (m :: * -> *) a. Monad m => a -> m a
return FunType
ft

  -- If a label applied to arguments is one of the parameters,
  -- we issue a warning because it looks confusing, even though
  -- it is not ambiguous, strictly speaking.  Example:
  --
  -- @
  --   define f x = EInt x;
  --   define g f = f f;  -- The first f is shadowed by the parameter f.
  -- @
  warnIfShadowed :: LabelName -> m ()
warnIfShadowed LabelName
x =
    (Type -> m ()) -> Maybe Type -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (m () -> Type -> m ()
forall a b. a -> b -> a
const (m () -> Type -> m ()) -> m () -> Type -> m ()
forall a b. (a -> b) -> a -> b
$ Warning -> m ()
forall (m :: * -> *). MonadCheck m => Warning -> m ()
warn (Warning -> m ()) -> Warning -> m ()
forall a b. (a -> b) -> a -> b
$ LabelName -> Warning
ShadowedByParameter LabelName
x) (Maybe Type -> m ()) -> m (Maybe Type) -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< LabelName -> m (Maybe Type)
forall (f :: * -> *).
MonadReader Env f =>
LabelName -> f (Maybe Type)
lookupCxt LabelName
x