{-# 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
  , Base(..)
    -- * 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 -> b) -> Err a -> Err b)
-> (forall a b. a -> Err b -> Err a) -> Functor Err
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
Functor Err
-> (forall a. a -> Err a)
-> (forall a b. Err (a -> b) -> Err a -> Err b)
-> (forall a b c. (a -> b -> c) -> Err a -> Err b -> Err c)
-> (forall a b. Err a -> Err b -> Err b)
-> (forall a b. Err a -> Err b -> Err a)
-> Applicative 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
Applicative Err
-> (forall a b. Err a -> (a -> Err b) -> Err b)
-> (forall a b. Err a -> Err b -> Err b)
-> (forall a. a -> Err a)
-> Monad 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 = ReaderT Position (Either TCError) a -> Err a
forall a. ReaderT Position (Either TCError) a -> Err a
Err (ReaderT Position (Either TCError) a -> Err a)
-> ReaderT Position (Either TCError) a -> Err a
forall a b. (a -> b) -> a -> b
$ do
    Position
pos <- ReaderT Position (Either TCError) Position
forall r (m :: * -> *). MonadReader r m => m r
ask
    TCError -> ReaderT Position (Either TCError) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> ReaderT Position (Either TCError) a)
-> TCError -> ReaderT Position (Either TCError) a
forall a b. (a -> b) -> a -> b
$ Position -> String -> TCError
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 = ReaderT Position (Either TCError) a -> Err a
forall a. ReaderT Position (Either TCError) a -> Err a
Err (ReaderT Position (Either TCError) a -> Err a)
-> ReaderT Position (Either TCError) a -> Err a
forall a b. (a -> b) -> a -> b
$ do
    Err a -> ReaderT Position (Either TCError) a
forall a. Err a -> ReaderT Position (Either TCError) a
unErr Err a
m ReaderT Position (Either TCError) a
-> (TCError -> ReaderT Position (Either TCError) a)
-> ReaderT Position (Either TCError) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ (WithPosition Position
_ String
msg) -> Err a -> ReaderT Position (Either TCError) a
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 = (Position -> Position) -> Err a -> Err a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Position -> Position -> Position
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 = (TCError -> String) -> Either TCError a -> Either String a
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TCError -> String
blendInPosition (Either TCError a -> Either String a)
-> Either TCError a -> Either String a
forall a b. (a -> b) -> a -> b
$ Err a -> ReaderT Position (Either TCError) a
forall a. Err a -> ReaderT Position (Either TCError) a
unErr Err a
m ReaderT Position (Either TCError) a -> Position -> Either TCError a
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 :: (Base -> (String, Type))
-> (Base -> (String, Type)) -> ListConstructors
LC
  { nil :: Base -> (String, Type)
nil  = \ Base
b -> (String
"[]" , [Base] -> Base -> Type
FunT [] (Base -> Base
ListT Base
b))
  , cons :: Base -> (String, Type)
cons = \ Base
b -> (String
"(:)", [Base] -> Base -> Type
FunT [Base
b, Base -> Base
ListT Base
b] (Base -> Base
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) = [Either Pragma Define] -> ([Pragma], [Define])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either Pragma Define] -> ([Pragma], [Define]))
-> [Either Pragma Define] -> ([Pragma], [Define])
forall a b. (a -> b) -> a -> b
$ (Pragma -> Either Pragma Define)
-> [Pragma] -> [Either Pragma Define]
forall a b. (a -> b) -> [a] -> [b]
map Pragma -> Either Pragma Define
isFunDef ([Pragma] -> [Either Pragma Define])
-> [Pragma] -> [Either Pragma Define]
forall a b. (a -> b) -> a -> b
$ CF -> [Pragma]
forall function. CFG function -> [Pragma]
cfgPragmas CF
cf
  [Define]
defs <- (Define -> Err Define) -> [Define] -> Err [Define]
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
  CF -> Err CF
forall (m :: * -> *) a. Monad m => a -> m a
return CF
cf { cfgPragmas :: [Pragma]
cfgPragmas = [Pragma]
pragmas [Pragma] -> [Pragma] -> [Pragma]
forall a. [a] -> [a] -> [a]
++ (Define -> Pragma) -> [Define] -> [Pragma]
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' String
e0 Base
_) = do
  let xs :: [String]
xs = ((String, Base) -> String) -> Telescope -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Base) -> String
forall a b. (a, b) -> a
fst Telescope
args  -- Throw away dummy types.
  (Telescope
tel, (Exp' String
e, Base
b)) <- ListConstructors
-> Context
-> TCError
-> [String]
-> Exp' String
-> Err (Telescope, (Exp' String, Base))
checkDefinition' ListConstructors
dummyConstructors Context
ctx TCError
f [String]
xs Exp' String
e0
  Define -> Err Define
forall (m :: * -> *) a. Monad m => a -> m a
return (Define -> Err Define) -> Define -> Err Define
forall a b. (a -> b) -> a -> b
$ TCError -> Telescope -> Exp' String -> Base -> Define
Define TCError
f Telescope
tel Exp' String
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' String
-> Err (Telescope, (Exp' String, Base))
checkDefinition' ListConstructors
list Context
ctx TCError
ident [String]
xs Exp' String
e =
  Position
-> Err (Telescope, (Exp' String, Base))
-> Err (Telescope, (Exp' String, Base))
forall a. Position -> Err a -> Err a
withPosition (TCError -> Position
forall a. WithPosition a -> Position
wpPosition TCError
ident) (Err (Telescope, (Exp' String, Base))
 -> Err (Telescope, (Exp' String, Base)))
-> Err (Telescope, (Exp' String, Base))
-> Err (Telescope, (Exp' String, Base))
forall a b. (a -> b) -> a -> b
$
    do  Bool -> Err () -> Err ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Char -> Bool
isLower (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
forall a. [a] -> a
head String
f) (Err () -> Err ()) -> Err () -> Err ()
forall a b. (a -> b) -> a -> b
$ String -> Err ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err ()) -> String -> Err ()
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 Err Type -> (String -> Err Type) -> Err Type
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \String
_ ->
                                String -> Err Type
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err Type) -> String -> Err Type
forall a b. (a -> b) -> a -> b
$ String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' must be used in a rule."
        let expect :: Int
expect = [Base] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Base]
ts
            given :: Int
given  = [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
xs
        Bool -> Err () -> Err ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
expect Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
given) (Err () -> Err ()) -> Err () -> Err ()
forall a b. (a -> b) -> a -> b
$ String -> Err ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err ()) -> String -> Err ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ String
"'", String
f, String
"' is used with type ", Type -> String
forall a. Show a => a -> String
show Type
t
          , String
" but defined with ", Int -> String
forall a. Show a => a -> String
show Int
given, String
" argument", Int -> String
forall {a} {p}. (Eq a, Num a, IsString p) => a -> p
plural Int
given String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
          ]
        Exp' String
e' <- ListConstructors
-> Context -> Exp' String -> Base -> Err (Exp' String)
checkExp ListConstructors
list (Context -> Telescope -> Context
setLocals Context
ctx (Telescope -> Context) -> Telescope -> Context
forall a b. (a -> b) -> a -> b
$ [String] -> [Base] -> Telescope
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
xs [Base]
ts) Exp' String
e Base
t'
        (Telescope, (Exp' String, Base))
-> Err (Telescope, (Exp' String, Base))
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> [Base] -> Telescope
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
xs [Base]
ts, (Exp' String
e', Base
t'))
    Err (Telescope, (Exp' String, Base))
-> (String -> Err (Telescope, (Exp' String, Base)))
-> Err (Telescope, (Exp' String, Base))
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ String
err -> String -> Err (Telescope, (Exp' String, Base))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err (Telescope, (Exp' String, Base)))
-> String -> Err (Telescope, (Exp' String, Base))
forall a b. (a -> b) -> a -> b
$
      String
"In the definition " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (String
f String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
xs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"=", Exp' String -> String
forall a. Pretty a => a -> String
prettyShow Exp' String
e, String
";"]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err
    where
        f :: String
f = TCError -> String
forall a. WithPosition a -> a
wpThing TCError
ident
        plural :: a -> p
plural a
1 = p
""
        plural a
_ = p
"s"

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

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

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

  (e :: Exp' String
e@(App String
x Type
_ [Exp' String]
es)  , Base
t              ) -> Exp' String -> String -> [Exp' String] -> Base -> Err (Exp' String)
forall {a}.
Pretty a =>
a -> String -> [Exp' String] -> Base -> Err (Exp' String)
checkApp Exp' String
e String
x [Exp' String]
es Base
t
  (e :: Exp' String
e@(Var String
x)       , Base
t              ) -> Exp' String
e Exp' String -> Err (Exp' String) -> Err (Exp' String)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Exp' String -> String -> [Exp' String] -> Base -> Err (Exp' String)
forall {a}.
Pretty a =>
a -> String -> [Exp' String] -> Base -> Err (Exp' String)
checkApp Exp' String
e String
x [] Base
t
  (e :: Exp' String
e@LitInt{}      , BaseT String
"Integer") -> Exp' String -> Err (Exp' String)
forall (m :: * -> *) a. Monad m => a -> m a
return Exp' String
e
  (e :: Exp' String
e@LitDouble{}   , BaseT String
"Double" ) -> Exp' String -> Err (Exp' String)
forall (m :: * -> *) a. Monad m => a -> m a
return Exp' String
e
  (e :: Exp' String
e@LitChar{}     , BaseT String
"Char"   ) -> Exp' String -> Err (Exp' String)
forall (m :: * -> *) a. Monad m => a -> m a
return Exp' String
e
  (e :: Exp' String
e@LitString{}   , BaseT String
"String" ) -> Exp' String -> Err (Exp' String)
forall (m :: * -> *) a. Monad m => a -> m a
return Exp' String
e
  (Exp' String
e               , Base
t              ) -> String -> Err (Exp' String)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err (Exp' String)) -> String -> Err (Exp' String)
forall a b. (a -> b) -> a -> b
$
    Exp' String -> String
forall a. Pretty a => a -> String
prettyShow Exp' String
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does not have type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Base -> String
forall a. Show a => a -> String
show Base
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
  where
  checkApp :: a -> String -> [Exp' String] -> Base -> Err (Exp' String)
checkApp a
e String
x [Exp' String]
es Base
t = do
    ft :: Type
ft@(FunT [Base]
ts Base
t') <- String -> Context -> Err Type
lookupCtx String
x Context
ctx
    [Exp' String]
es' <- [Base] -> Err [Exp' String]
matchArgs [Base]
ts
    Bool -> Err () -> Err ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Base
t Base -> Base -> Bool
forall a. Eq a => a -> a -> Bool
== Base
t') (Err () -> Err ()) -> Err () -> Err ()
forall a b. (a -> b) -> a -> b
$ String -> Err ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err ()) -> String -> Err ()
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Pretty a => a -> String
prettyShow a
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Base -> String
forall a. Show a => a -> String
show Base
t' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", but something of type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Base -> String
forall a. Show a => a -> String
show Base
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" was expected."
    Exp' String -> Err (Exp' String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp' String -> Err (Exp' String))
-> Exp' String -> Err (Exp' String)
forall a b. (a -> b) -> a -> b
$ String -> Type -> [Exp' String] -> Exp' String
forall f. f -> Type -> [Exp' f] -> Exp' f
App String
x Type
ft [Exp' String]
es'
    where
    matchArgs :: [Base] -> Err [Exp' String]
matchArgs [Base]
ts
      | Int
expect Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
given   = String -> Err [Exp' String]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err [Exp' String]) -> String -> Err [Exp' String]
forall a b. (a -> b) -> a -> b
$ String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' takes " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
expect String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" arguments, but has been given " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
given String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
      | Bool
otherwise         = (Exp' String -> Base -> Err (Exp' String))
-> [Exp' String] -> [Base] -> Err [Exp' String]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (ListConstructors
-> Context -> Exp' String -> Base -> Err (Exp' String)
checkExp ListConstructors
list Context
ctx) [Exp' String]
es [Base]
ts
      where
        expect :: Int
expect = [Base] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Base]
ts
        given :: Int
given  = [Exp' String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp' String]
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 = (Set (WithPosition Type)
 -> Set (WithPosition Type) -> Set (WithPosition Type))
-> [(String, Set (WithPosition Type))]
-> Map String (Set (WithPosition Type))
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Set (WithPosition Type)
-> Set (WithPosition Type) -> Set (WithPosition Type)
forall a. Monoid a => a -> a -> a
mappend ([(String, Set (WithPosition Type))]
 -> Map String (Set (WithPosition Type)))
-> [(String, Set (WithPosition Type))]
-> Map String (Set (WithPosition Type))
forall a b. (a -> b) -> a -> b
$ ((String, WithPosition Type) -> (String, Set (WithPosition Type)))
-> [(String, WithPosition Type)]
-> [(String, Set (WithPosition Type))]
forall a b. (a -> b) -> [a] -> [b]
map ((WithPosition Type -> Set (WithPosition Type))
-> (String, WithPosition Type) -> (String, Set (WithPosition Type))
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second WithPosition Type -> Set (WithPosition Type)
forall a. a -> Set a
Set.singleton) [(String, WithPosition Type)]
labels
  -- Check for duplicates; extract from singleton sets.
  [(String, WithPosition Type)]
sig <- [(String, Set (WithPosition Type))]
-> ((String, Set (WithPosition Type))
    -> Err (String, WithPosition Type))
-> Err [(String, WithPosition Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map String (Set (WithPosition Type))
-> [(String, Set (WithPosition Type))]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map String (Set (WithPosition Type))
sig0) (((String, Set (WithPosition Type))
  -> Err (String, WithPosition Type))
 -> Err [(String, WithPosition Type)])
-> ((String, Set (WithPosition Type))
    -> Err (String, WithPosition Type))
-> Err [(String, WithPosition Type)]
forall a b. (a -> b) -> a -> b
$ \ (String
f,Set (WithPosition Type)
ts) ->
    case Set (WithPosition Type) -> [WithPosition Type]
forall a. Set a -> [a]
Set.toList Set (WithPosition Type)
ts of
      []  -> Err (String, WithPosition Type)
forall a. HasCallStack => a
undefined  -- impossible
      [WithPosition Type
t] -> (String, WithPosition Type) -> Err (String, WithPosition Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
f,WithPosition Type
t)
      [WithPosition Type]
ts' -> String -> Err (String, WithPosition Type)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err (String, WithPosition Type))
-> String -> Err (String, WithPosition Type)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [ String
"The label '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' is used at conflicting types:" ]
        , (WithPosition Type -> String) -> [WithPosition Type] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String)
-> (WithPosition Type -> String) -> WithPosition Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCError -> String
blendInPosition (TCError -> String)
-> (WithPosition Type -> TCError) -> WithPosition Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> String) -> WithPosition Type -> TCError
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> String
forall a. Show a => a -> String
show) [WithPosition Type]
ts'
        ]
  Signature -> Err Signature
forall (m :: * -> *) a. Monad m => a -> m a
return (Signature -> Err Signature) -> Signature -> Err Signature
forall a b. (a -> b) -> a -> b
$ [(String, WithPosition Type)] -> Signature
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  = Base -> Base
ListT (Base -> Base) -> Base -> Base
forall a b. (a -> b) -> a -> b
$ Cat -> Base
mkBase (Cat -> Base) -> Cat -> Base
forall a b. (a -> b) -> a -> b
$ Cat -> Cat
normCatOfList Cat
t
        | Bool
otherwise = String -> Base
BaseT (String -> Base) -> String -> Base
forall a b. (a -> b) -> a -> b
$ Cat -> String
catToStr (Cat -> String) -> Cat -> String
forall a b. (a -> b) -> a -> b
$ Cat -> Cat
normCat Cat
t

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

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

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