{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}

-- | Type checker for defined syntax constructors @define f xs = e@.

module BNFC.TypeChecker
  ( -- * Type checker entry point
    runTypeChecker
  , checkDefinitions
    -- * Backdoor for rechecking defined syntax constructors for list types
  , checkDefinition'
  , buildSignature, buildContext, ctxTokens, isToken
  , ListConstructors(..)
  ) where

import Control.Monad
import Control.Monad.Except (MonadError(..))
import Control.Monad.Reader

import Data.Bifunctor
import Data.Char
import Data.Either (partitionEithers)

import qualified Data.Map as Map
import qualified Data.Set as Set

import BNFC.CF
import BNFC.PrettyPrint

-- * Error monad

type TCError = WithPosition String

-- | Type checking monad, reports errors.
newtype Err a = Err { forall a. Err a -> ReaderT Position (Either TCError) a
unErr :: ReaderT Position (Either TCError) a }
  deriving (forall a b. a -> Err b -> Err a
forall a b. (a -> b) -> Err a -> Err b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Err b -> Err a
$c<$ :: forall a b. a -> Err b -> Err a
fmap :: forall a b. (a -> b) -> Err a -> Err b
$cfmap :: forall a b. (a -> b) -> Err a -> Err b
Functor, Functor Err
forall a. a -> Err a
forall a b. Err a -> Err b -> Err a
forall a b. Err a -> Err b -> Err b
forall a b. Err (a -> b) -> Err a -> Err b
forall a b c. (a -> b -> c) -> Err a -> Err b -> Err c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. Err a -> Err b -> Err a
$c<* :: forall a b. Err a -> Err b -> Err a
*> :: forall a b. Err a -> Err b -> Err b
$c*> :: forall a b. Err a -> Err b -> Err b
liftA2 :: forall a b c. (a -> b -> c) -> Err a -> Err b -> Err c
$cliftA2 :: forall a b c. (a -> b -> c) -> Err a -> Err b -> Err c
<*> :: forall a b. Err (a -> b) -> Err a -> Err b
$c<*> :: forall a b. Err (a -> b) -> Err a -> Err b
pure :: forall a. a -> Err a
$cpure :: forall a. a -> Err a
Applicative, Applicative Err
forall a. a -> Err a
forall a b. Err a -> Err b -> Err b
forall a b. Err a -> (a -> Err b) -> Err b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> Err a
$creturn :: forall a. a -> Err a
>> :: forall a b. Err a -> Err b -> Err b
$c>> :: forall a b. Err a -> Err b -> Err b
>>= :: forall a b. Err a -> (a -> Err b) -> Err b
$c>>= :: forall a b. Err a -> (a -> Err b) -> Err b
Monad, MonadReader Position)

instance MonadError String Err where
  throwError :: forall a. String -> Err a
throwError String
msg = forall a. ReaderT Position (Either TCError) a -> Err a
Err forall a b. (a -> b) -> a -> b
$ do
    Position
pos <- forall r (m :: * -> *). MonadReader r m => m r
ask
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Position -> a -> WithPosition a
WithPosition Position
pos String
msg
  catchError :: forall a. Err a -> (String -> Err a) -> Err a
catchError Err a
m String -> Err a
h = forall a. ReaderT Position (Either TCError) a -> Err a
Err forall a b. (a -> b) -> a -> b
$ do
    forall a. Err a -> ReaderT Position (Either TCError) a
unErr Err a
m forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ (WithPosition Position
_ String
msg) -> forall a. Err a -> ReaderT Position (Either TCError) a
unErr (String -> Err a
h String
msg)

withPosition :: Position -> Err a -> Err a
withPosition :: forall a. Position -> Err a -> Err a
withPosition Position
pos = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall a b. a -> b -> a
const Position
pos)

runTypeChecker :: Err a -> Either String a
runTypeChecker :: forall a. Err a -> Either String a
runTypeChecker Err a
m = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TCError -> String
blendInPosition forall a b. (a -> b) -> a -> b
$ forall a. Err a -> ReaderT Position (Either TCError) a
unErr Err a
m forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` Position
NoPosition

-- * Types and context

data Context = Ctx
  { Context -> Signature
ctxLabels :: Signature         -- ^ Types of labels, extracted from rules.
  , Context -> [String]
ctxTokens :: [String]          -- ^ User-defined token types.
  , Context -> Telescope
ctxLocals :: Telescope         -- ^ Types of local variables of a definition.
  }

data ListConstructors = LC
  { ListConstructors -> Base -> (String, Type)
nil   :: Base -> (String, Type)  -- ^ 'Base' is the element type. 'Type' the list type.
  , ListConstructors -> Base -> (String, Type)
cons  :: Base -> (String, Type)
  }

dummyConstructors :: ListConstructors
dummyConstructors :: ListConstructors
dummyConstructors = LC
  { nil :: Base -> (String, Type)
nil  = \ Base
b -> (String
"[]" , [Base] -> Base -> Type
FunT [] (forall a. Base' a -> Base' a
ListT Base
b))
  , cons :: Base -> (String, Type)
cons = \ Base
b -> (String
"(:)", [Base] -> Base -> Type
FunT [Base
b, forall a. Base' a -> Base' a
ListT Base
b] (forall a. Base' a -> Base' a
ListT Base
b))
  }

-- * Type checker for definitions and expressions

-- | Entry point.
checkDefinitions :: CF -> Err CF
checkDefinitions :: CF -> Err CF
checkDefinitions CF
cf = do
  let ctx :: Context
ctx = CF -> Context
buildContext CF
cf
  let ([Pragma]
pragmas, [Define]
defs0) = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Pragma -> Either Pragma Define
isFunDef forall a b. (a -> b) -> a -> b
$ forall function. CFG function -> [Pragma]
cfgPragmas CF
cf
  [Define]
defs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Context -> Define -> Err Define
checkDefinition Context
ctx) [Define]
defs0
  forall (m :: * -> *) a. Monad m => a -> m a
return CF
cf { cfgPragmas :: [Pragma]
cfgPragmas = [Pragma]
pragmas forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Define -> Pragma
FunDef [Define]
defs }

checkDefinition :: Context -> Define -> Err Define
checkDefinition :: Context -> Define -> Err Define
checkDefinition Context
ctx (Define TCError
f Telescope
args Exp
e0 Base
_) = do
  let xs :: [String]
xs = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst Telescope
args  -- Throw away dummy types.
  (Telescope
tel, (Exp
e, Base
b)) <- ListConstructors
-> Context
-> TCError
-> [String]
-> Exp
-> Err (Telescope, (Exp, Base))
checkDefinition' ListConstructors
dummyConstructors Context
ctx TCError
f [String]
xs Exp
e0
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ TCError -> Telescope -> Exp -> Base -> Define
Define TCError
f Telescope
tel Exp
e Base
b

checkDefinition'
  :: ListConstructors  -- ^ Translation of the list constructors.
  -> Context           -- ^ Signature (types of labels).
  -> RFun              -- ^ Function name.
  -> [String]          -- ^ Function arguments.
  -> Exp               -- ^ Function body.
  -> Err (Telescope, (Exp, Base))  -- ^ Typed arguments, translated body, type of body.
checkDefinition' :: ListConstructors
-> Context
-> TCError
-> [String]
-> Exp
-> Err (Telescope, (Exp, Base))
checkDefinition' ListConstructors
list Context
ctx TCError
ident [String]
xs Exp
e =
  forall a. Position -> Err a -> Err a
withPosition (forall a. WithPosition a -> Position
wpPosition TCError
ident) forall a b. (a -> b) -> a -> b
$
    do  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Char -> Bool
isLower forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head String
f) 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
$
          String
"Defined functions must start with a lowercase letter."
        t :: Type
t@(FunT [Base]
ts Base
t') <- String -> Context -> Err Type
lookupCtx String
f Context
ctx forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \String
_ ->
                                forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"'" forall a. [a] -> [a] -> [a]
++ String
f forall a. [a] -> [a] -> [a]
++ String
"' must be used in a rule."
        let expect :: Int
expect = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Base]
ts
            given :: Int
given  = forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
xs
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
expect forall a. Eq a => a -> a -> Bool
== Int
given) 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
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ String
"'", String
f, String
"' is used with type ", forall a. Show a => a -> String
show Type
t
          , String
" but defined with ", forall a. Show a => a -> String
show Int
given, String
" argument", forall {a} {a}. (Eq a, Num a, IsString a) => a -> a
plural Int
given forall a. [a] -> [a] -> [a]
++ String
"."
          ]
        Exp
e' <- ListConstructors -> Context -> Exp -> Base -> Err Exp
checkExp ListConstructors
list (Context -> Telescope -> Context
setLocals Context
ctx forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [String]
xs [Base]
ts) Exp
e Base
t'
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. [a] -> [b] -> [(a, b)]
zip [String]
xs [Base]
ts, (Exp
e', Base
t'))
    forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ String
err -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
      String
"In the definition " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (String
f forall a. a -> [a] -> [a]
: [String]
xs forall a. [a] -> [a] -> [a]
++ [String
"=", forall a. Pretty a => a -> String
prettyShow Exp
e, String
";"]) forall a. [a] -> [a] -> [a]
++ String
"\n  " forall a. [a] -> [a] -> [a]
++ String
err
    where
        f :: String
f = forall a. WithPosition a -> a
wpThing TCError
ident
        plural :: a -> a
plural a
1 = a
""
        plural a
_ = a
"s"

checkExp :: ListConstructors -> Context -> Exp -> Base -> Err Exp
checkExp :: ListConstructors -> Context -> Exp -> Base -> Err Exp
checkExp ListConstructors
list Context
ctx = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
  (App String
"[]" Type
_ []     , ListT Base
t      ) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall f. f -> Type -> [Exp' f] -> Exp' f
App (ListConstructors -> Base -> (String, Type)
nil ListConstructors
list Base
t) [])
  (App String
"[]" Type
_ [Exp]
_      , Base
_            ) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
    String
"[] is applied to too many arguments."

  (App String
"(:)" Type
_ [Exp
e,Exp
es], ListT Base
t      ) -> do
    Exp
e'  <- ListConstructors -> Context -> Exp -> Base -> Err Exp
checkExp ListConstructors
list Context
ctx Exp
e Base
t
    Exp
es' <- ListConstructors -> Context -> Exp -> Base -> Err Exp
checkExp ListConstructors
list Context
ctx Exp
es (forall a. Base' a -> Base' a
ListT Base
t)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall f. f -> Type -> [Exp' f] -> Exp' f
App (ListConstructors -> Base -> (String, Type)
cons ListConstructors
list Base
t) [Exp
e',Exp
es']

  (App String
"(:)" Type
_ [Exp]
es  , Base
_              ) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
    String
"(:) takes 2 arguments, but has been given " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp]
es) forall a. [a] -> [a] -> [a]
++ String
"."

  (e :: Exp
e@(App String
x Type
_ [Exp]
es)  , Base
t              ) -> forall {a}. Pretty a => a -> String -> [Exp] -> Base -> Err Exp
checkApp Exp
e String
x [Exp]
es Base
t
  (e :: Exp
e@(Var String
x)       , Base
t              ) -> Exp
e forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall {a}. Pretty a => a -> String -> [Exp] -> Base -> Err Exp
checkApp Exp
e String
x [] Base
t
  (e :: Exp
e@LitInt{}      , BaseT String
"Integer") -> forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e
  (e :: Exp
e@LitDouble{}   , BaseT String
"Double" ) -> forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e
  (e :: Exp
e@LitChar{}     , BaseT String
"Char"   ) -> forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e
  (e :: Exp
e@LitString{}   , BaseT String
"String" ) -> forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e
  (Exp
e               , Base
t              ) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
    forall a. Pretty a => a -> String
prettyShow Exp
e forall a. [a] -> [a] -> [a]
++ String
" does not have type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Base
t forall a. [a] -> [a] -> [a]
++ String
"."
  where
  checkApp :: a -> String -> [Exp] -> Base -> Err Exp
checkApp a
e String
x [Exp]
es Base
t = do
    ft :: Type
ft@(FunT [Base]
ts Base
t') <- String -> Context -> Err Type
lookupCtx String
x Context
ctx
    [Exp]
es' <- [Base] -> Err [Exp]
matchArgs [Base]
ts
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Base
t forall a. Eq a => a -> a -> Bool
== Base
t') 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
$ forall a. Pretty a => a -> String
prettyShow a
e forall a. [a] -> [a] -> [a]
++ String
" has type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Base
t' forall a. [a] -> [a] -> [a]
++ String
", but something of type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Base
t forall a. [a] -> [a] -> [a]
++ String
" was expected."
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall f. f -> Type -> [Exp' f] -> Exp' f
App String
x Type
ft [Exp]
es'
    where
    matchArgs :: [Base] -> Err [Exp]
matchArgs [Base]
ts
      | Int
expect forall a. Eq a => a -> a -> Bool
/= Int
given   = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"'" forall a. [a] -> [a] -> [a]
++ String
x forall a. [a] -> [a] -> [a]
++ String
"' takes " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
expect forall a. [a] -> [a] -> [a]
++ String
" arguments, but has been given " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
given forall a. [a] -> [a] -> [a]
++ String
"."
      | Bool
otherwise         = forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (ListConstructors -> Context -> Exp -> Base -> Err Exp
checkExp ListConstructors
list Context
ctx) [Exp]
es [Base]
ts
      where
        expect :: Int
expect = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Base]
ts
        given :: Int
given  = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp]
es

-- * Context handling

-- | Create context containing the types of all labels,
--   computed from the rules.
--
--   Fail if a label is used at different types.
--
buildSignature :: [Rule] -> Err Signature
buildSignature :: [Rule] -> Err Signature
buildSignature [Rule]
rules = do
  -- Build label signature with duplicates
  let sig0 :: Map String (Set (WithPosition Type))
sig0 = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. Monoid a => a -> a -> a
mappend forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a. a -> Set a
Set.singleton) [(String, WithPosition Type)]
labels
  -- Check for duplicates; extract from singleton sets.
  [(String, WithPosition Type)]
sig <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
Map.toAscList Map String (Set (WithPosition Type))
sig0) forall a b. (a -> b) -> a -> b
$ \ (String
f,Set (WithPosition Type)
ts) ->
    case forall a. Set a -> [a]
Set.toList Set (WithPosition Type)
ts of
      []  -> forall a. HasCallStack => a
undefined  -- impossible
      [WithPosition Type
t] -> forall (m :: * -> *) a. Monad m => a -> m a
return (String
f,WithPosition Type
t)
      [WithPosition Type]
ts' -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [ String
"The label '" forall a. [a] -> [a] -> [a]
++ String
f forall a. [a] -> [a] -> [a]
++ String
"' is used at conflicting types:" ]
        , forall a b. (a -> b) -> [a] -> [b]
map ((String
"  " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCError -> String
blendInPosition forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Show a => a -> String
show) [WithPosition Type]
ts'
        ]
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList [(String, WithPosition Type)]
sig
  where
    mkType :: Cat -> [Either Cat b] -> Type
mkType Cat
cat [Either Cat b]
args = [Base] -> Base -> Type
FunT [ Cat -> Base
mkBase Cat
t | Left Cat
t <- [Either Cat b]
args ]
                           (Cat -> Base
mkBase Cat
cat)
    mkBase :: Cat -> Base
mkBase Cat
t
        | Cat -> Bool
isList Cat
t  = forall a. Base' a -> Base' a
ListT forall a b. (a -> b) -> a -> b
$ Cat -> Base
mkBase forall a b. (a -> b) -> a -> b
$ Cat -> Cat
normCatOfList Cat
t
        | Bool
otherwise = forall a. a -> Base' a
BaseT forall a b. (a -> b) -> a -> b
$ Cat -> String
catToStr forall a b. (a -> b) -> a -> b
$ Cat -> Cat
normCat Cat
t

    labels :: [(String, WithPosition Type)]
labels =
      [ (String
x, forall a. Position -> a -> WithPosition a
WithPosition Position
pos forall a b. (a -> b) -> a -> b
$ forall {b}. Cat -> [Either Cat b] -> Type
mkType (forall a. WithPosition a -> a
wpThing RCat
cat) SentForm
args)
        | Rule f :: TCError
f@(WithPosition Position
pos String
x) RCat
cat SentForm
args InternalRule
_ <- [Rule]
rules
        , Bool -> Bool
not (forall a. IsFun a => a -> Bool
isCoercion TCError
f)
        , Bool -> Bool
not (forall a. IsFun a => a -> Bool
isNilCons TCError
f)
      ]

buildContext :: CF -> Context
buildContext :: CF -> Context
buildContext CF
cf = Ctx
    { ctxLabels :: Signature
ctxLabels = forall function. CFG function -> Signature
cfgSignature CF
cf
    , ctxTokens :: [String]
ctxTokens = (String
"Ident" forall a. a -> [a] -> [a]
: forall f. CFG f -> [String]
tokenNames CF
cf)
    , ctxLocals :: Telescope
ctxLocals = []
    }

isToken :: String -> Context -> Bool
isToken :: String -> Context -> Bool
isToken String
x Context
ctx = forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
x forall a b. (a -> b) -> a -> b
$ Context -> [String]
ctxTokens Context
ctx

setLocals :: Context -> [(String,Base)] -> Context
setLocals :: Context -> Telescope -> Context
setLocals Context
ctx Telescope
xs = Context
ctx { ctxLocals :: Telescope
ctxLocals = Telescope
xs }

lookupCtx :: String -> Context -> Err Type
lookupCtx :: String -> Context -> Err Type
lookupCtx String
x Context
ctx
  | String -> Context -> Bool
isToken String
x Context
ctx = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Base] -> Base -> Type
FunT [forall a. a -> Base' a
BaseT String
"String"] (forall a. a -> Base' a
BaseT String
x)
  | Bool
otherwise     = do
    case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
x forall a b. (a -> b) -> a -> b
$ Context -> Telescope
ctxLocals Context
ctx of
      Just Base
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Base] -> Base -> Type
FunT [] Base
b
      Maybe Base
Nothing -> do
        case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
x forall a b. (a -> b) -> a -> b
$ Context -> Signature
ctxLabels Context
ctx of
          Maybe (WithPosition Type)
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"Undefined symbol '" forall a. [a] -> [a] -> [a]
++ String
x forall a. [a] -> [a] -> [a]
++ String
"'."
          Just WithPosition Type
t  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. WithPosition a -> a
wpThing WithPosition Type
t