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

-- | 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(LC)
  ) where

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

import Data.Bifunctor
import Data.Char

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

import BNFC.CF

-- * Error monad

type TCError = WithPosition String

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

instance MonadError String Err where
  throwError :: 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 :: 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 :: 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 :: 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

-- | Function arguments with type.
type Telescope = [(String, Base)]

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
nil   :: Base -> String
        , ListConstructors -> Base -> String
cons  :: Base -> String
        }

dummyConstructors :: ListConstructors
dummyConstructors :: ListConstructors
dummyConstructors = (Base -> String) -> (Base -> String) -> ListConstructors
LC (String -> Base -> String
forall a b. a -> b -> a
const String
"[]") (String -> Base -> String
forall a b. a -> b -> a
const String
"(:)")


-- * Type checker for definitions and expressions

-- | Entry point.
checkDefinitions :: CF -> Err ()
checkDefinitions :: CF -> Err ()
checkDefinitions CF
cf = do
  let ctx :: Context
ctx = CF -> Context
buildContext CF
cf
  [Err ()] -> Err ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ Context -> TCError -> [String] -> Exp -> Err ()
checkDefinition Context
ctx TCError
f [String]
xs Exp
e | FunDef TCError
f [String]
xs Exp
e <- CF -> [Pragma]
forall function. CFG function -> [Pragma]
cfgPragmas CF
cf ]

checkDefinition :: Context -> RFun -> [String] -> Exp -> Err ()
checkDefinition :: Context -> TCError -> [String] -> Exp -> Err ()
checkDefinition Context
ctx TCError
f [String]
xs Exp
e =
    Err (Telescope, (Exp, Base)) -> Err ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Err (Telescope, (Exp, Base)) -> Err ())
-> Err (Telescope, (Exp, Base)) -> Err ()
forall a b. (a -> b) -> a -> b
$ ListConstructors
-> Context
-> TCError
-> [String]
-> Exp
-> Err (Telescope, (Exp, Base))
checkDefinition' ListConstructors
dummyConstructors Context
ctx TCError
f [String]
xs Exp
e

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 =
  Position
-> Err (Telescope, (Exp, Base)) -> Err (Telescope, (Exp, Base))
forall a. Position -> Err a -> Err a
withPosition (TCError -> Position
forall a. WithPosition a -> Position
wpPosition TCError
ident) (Err (Telescope, (Exp, Base)) -> Err (Telescope, (Exp, Base)))
-> Err (Telescope, (Exp, Base)) -> Err (Telescope, (Exp, 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
e' <- ListConstructors -> Context -> Exp -> Base -> Err Exp
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
e Base
t'
        (Telescope, (Exp, Base)) -> Err (Telescope, (Exp, 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
e', Base
t'))
    Err (Telescope, (Exp, Base))
-> (String -> Err (Telescope, (Exp, Base)))
-> Err (Telescope, (Exp, Base))
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ String
err -> String -> Err (Telescope, (Exp, Base))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err (Telescope, (Exp, Base)))
-> String -> Err (Telescope, (Exp, 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
forall a. Show a => a -> String
show Exp
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 -> Base -> Err Exp
checkExp ListConstructors
list Context
ctx = ((Exp, Base) -> Err Exp) -> Exp -> Base -> Err Exp
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Exp, Base) -> Err Exp) -> Exp -> Base -> Err Exp)
-> ((Exp, Base) -> Err Exp) -> Exp -> Base -> Err Exp
forall a b. (a -> b) -> a -> b
$ \case
  (App String
"[]" []     , ListT Base
t        ) -> Exp -> Err Exp
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> [Exp] -> Exp
App (ListConstructors -> Base -> String
nil ListConstructors
list Base
t) [])
  (App String
"[]" [Exp]
_      , Base
_              ) -> String -> Err Exp
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err Exp) -> String -> Err Exp
forall a b. (a -> b) -> a -> b
$
    String
"[] is applied to too many arguments."

  (App String
"(:)" [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 (Base -> Base
ListT Base
t)
    Exp -> Err Exp
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> Err Exp) -> Exp -> Err Exp
forall a b. (a -> b) -> a -> b
$ String -> [Exp] -> Exp
App (ListConstructors -> Base -> String
cons ListConstructors
list Base
t) [Exp
e',Exp
es']

  (App String
"(:)" [Exp]
es    , Base
_              ) -> String -> Err Exp
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err Exp) -> String -> Err Exp
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] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp]
es) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."

  (e :: Exp
e@(App String
x [Exp]
es)    , Base
t              ) -> Exp -> String -> [Exp] -> Base -> Err Exp
forall a. Show 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 Exp -> Err Exp -> Err Exp
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Exp -> String -> [Exp] -> Base -> Err Exp
forall a. Show a => a -> String -> [Exp] -> Base -> Err Exp
checkApp Exp
e String
x [] Base
t
  (e :: Exp
e@LitInt{}      , BaseT String
"Integer") -> Exp -> Err Exp
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e
  (e :: Exp
e@LitDouble{}   , BaseT String
"Double" ) -> Exp -> Err Exp
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e
  (e :: Exp
e@LitChar{}     , BaseT String
"Char"   ) -> Exp -> Err Exp
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e
  (e :: Exp
e@LitString{}   , BaseT String
"String" ) -> Exp -> Err Exp
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
e
  (Exp
e               , Base
t              ) -> String -> Err Exp
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err Exp) -> String -> Err Exp
forall a b. (a -> b) -> a -> b
$
    Exp -> String
forall a. Show a => a -> String
show Exp
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] -> Base -> Err Exp
checkApp a
e String
x [Exp]
es Base
t = do
    FunT [Base]
ts Base
t' <- String -> Context -> Err Type
lookupCtx String
x Context
ctx
    [Exp]
es' <- [Base] -> Err [Exp]
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. Show a => a -> String
show 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 -> Err Exp
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> Err Exp) -> Exp -> Err Exp
forall a b. (a -> b) -> a -> b
$ String -> [Exp] -> Exp
App String
x [Exp]
es'
    where
    matchArgs :: [Base] -> Err [Exp]
matchArgs [Base]
ts
      | Int
expect Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
given   = String -> Err [Exp]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Err [Exp]) -> String -> Err [Exp]
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 -> Base -> Err Exp) -> [Exp] -> [Base] -> Err [Exp]
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 = [Base] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Base]
ts
        given :: Int
given  = [Exp] -> Int
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 = (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