-- NOTE: insertion of polarity variables disabled here, must be done
-- in TypeChecker

{-# LANGUAGE TupleSections, DeriveFunctor, GeneralizedNewtypeDeriving,
      FlexibleContexts, FlexibleInstances, UndecidableInstances,
      MultiParamTypeClasses #-}

{-# OPTIONS_GHC -fno-warn-missing-signatures #-}

module ScopeChecker (scopeCheck) where

import Prelude hiding (mapM, null)

#if !MIN_VERSION_base(4,8,0)
import Control.Applicative
#endif
import Control.Monad          hiding (mapM)
import Control.Monad.Identity (Identity, runIdentity)
import Control.Monad.Reader   (ReaderT, runReaderT, MonadReader, ask, asks, local)
import Control.Monad.State    (StateT, execStateT, runStateT, get, gets, modify, put)
import Control.Monad.Except   (ExceptT, runExceptT, MonadError, catchError)
import Control.Monad.Trans    (lift)

import Data.List (sort, (\\))
import qualified Data.List as List
import Data.Maybe
import Data.Traversable (mapM)

-- import Debug.Trace

import Polarity(Pol(..))
import qualified Polarity as A
import Abstract
  ( Sized, Co, ConK(..), PrePost(..), MVar, Override(..), Measure(..), adjustTopDecsM
  , Arity, polarity, LensPol(..)
  )
import qualified Abstract as A
import qualified Concrete as C

import TraceError

import Util

-- * Scope checker.
-- - check that all identifiers are in scope and global identifiers are only used once
-- - replaces Ident with Con, Def, Let or Var
-- - replaces IdentP with ConP or VarP in patterns
-- - replaces Unknown by a new Meta-Variable
-- - check pattern length is equal in each clause
-- - group mutual declarations

-- | Entry point for scope checker.
scopeCheck :: [C.Declaration] -> Either TraceError ([A.Declaration],SCState)
scopeCheck :: [Declaration] -> Either TraceError ([Declaration], SCState)
scopeCheck [Declaration]
dl = SCCxt
-> SCState
-> ScopeCheck [Declaration]
-> Either TraceError ([Declaration], SCState)
forall a.
SCCxt -> SCState -> ScopeCheck a -> Either TraceError (a, SCState)
runScopeCheck SCCxt
initCtx SCState
initSt ([Declaration] -> ScopeCheck [Declaration]
scopeCheckDecls [Declaration]
dl)

-- * Local identifiers.

-- ** local environment of scope checker

data SCCxt = SCCxt
  { SCCxt -> Stack
stack             :: Stack     -- ^ Local names in scope.
    -- We keep a stack of these to disallow shadowing on the same level.
  , SCCxt -> Pol
defaultPolarity   :: Pol       -- ^ Replacement for @Default@ polarity.
  , SCCxt -> Bool
constraintAllowed :: Bool      -- ^ Is a constraint @|m| < |m'|@ legal now, since we just parsed a quantifier?
  }

type Stack = [Context]

initCtx :: SCCxt
initCtx :: SCCxt
initCtx = SCCxt
  { stack :: Stack
stack             = [[]]  -- one empty context to begin with
  , defaultPolarity :: Pol
defaultPolarity   = Pol
A.Rec -- POL VARS DISABLED!!
  , constraintAllowed :: Bool
constraintAllowed = Bool
False
  }

-- ** A lens for @constraintAllowed@

class LensConstraintAllowed a where
  mapConstraintAllowed :: (Bool -> Bool) -> a -> a
  setConstraintAllowed :: Bool -> a -> a
  setConstraintAllowed Bool
b = (Bool -> Bool) -> a -> a
forall a. LensConstraintAllowed a => (Bool -> Bool) -> a -> a
mapConstraintAllowed (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
b)

instance LensConstraintAllowed SCCxt where
  mapConstraintAllowed :: (Bool -> Bool) -> SCCxt -> SCCxt
mapConstraintAllowed Bool -> Bool
f SCCxt
sc = SCCxt
sc { constraintAllowed = f (constraintAllowed sc) }

instance (LensConstraintAllowed r, MonadReader r m) => LensConstraintAllowed (m a) where
  mapConstraintAllowed :: (Bool -> Bool) -> m a -> m a
mapConstraintAllowed Bool -> Bool
f = (r -> r) -> m a -> m a
forall a. (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Bool -> Bool) -> r -> r
forall a. LensConstraintAllowed a => (Bool -> Bool) -> a -> a
mapConstraintAllowed Bool -> Bool
f)

-- ** Managing the stack of local contexts.

newLevel :: ScopeCheck a -> ScopeCheck a
newLevel :: forall a. ScopeCheck a -> ScopeCheck a
newLevel = (SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a
forall a. (SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a)
-> (SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a
forall a b. (a -> b) -> a -> b
$ \ SCCxt
cxt -> SCCxt
cxt { stack = [] : stack cxt }

thisLevel :: SCCxt -> Context
thisLevel :: SCCxt -> PatCtx
thisLevel SCCxt
cxt = Stack -> PatCtx
forall a. HasCallStack => [a] -> a
head (SCCxt -> Stack
stack SCCxt
cxt)

instance Push Local SCCxt where
  push :: Local -> SCCxt -> SCCxt
push Local
nx SCCxt
sc = SCCxt
sc { stack = push nx (stack sc) }

-- ** translating concrete names to abstract names

type Local   = (C.Name,A.Name)
type Context = [Local]

emptyCtx :: Context
emptyCtx :: PatCtx
emptyCtx = []

newLocal :: Push Local b => C.Name -> b -> (A.Name, b)
newLocal :: forall b. Push Local b => Name -> b -> (Name, b)
newLocal Name
n b
cxt = (Name
x, Local -> b -> b
forall a b. Push a b => a -> b -> b
push (Name
n, Name
x) b
cxt)
  where x :: Name
x = String -> Name
A.fresh (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ Name -> String
C.theName Name
n

lookupLocal :: C.Name -> ScopeCheck (Maybe A.Name)
lookupLocal :: Name -> ScopeCheck (Maybe Name)
lookupLocal Name
n = Name -> Stack -> Maybe Name
forall a b c. (Retrieve a b c, Eq a) => a -> b -> Maybe c
retrieve Name
n (Stack -> Maybe Name)
-> ScopeCheck Stack -> ScopeCheck (Maybe Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SCCxt -> Stack) -> ScopeCheck Stack
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SCCxt -> Stack
stack

lookupGlobal :: C.QName -> ScopeCheck (Maybe DefI)
lookupGlobal :: QName -> ScopeCheck (Maybe DefI)
lookupGlobal QName
n = QName -> Sig -> Maybe DefI
lookupSig QName
n (Sig -> Maybe DefI) -> ScopeCheck Sig -> ScopeCheck (Maybe DefI)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ScopeCheck Sig
getSig

addContext :: Context -> SCCxt -> SCCxt
addContext :: PatCtx -> SCCxt -> SCCxt
addContext PatCtx
delta SCCxt
sc = SCCxt
sc { stack = delta : stack sc }

-- * Global identifiers.

-- | Kind of identifier.
data IKind
  = DataK
  | ConK ConK
  | FunK Bool  -- ^ @False@ = inside body, @True@ = outside body
  | ProjK      -- ^ a record projection
  | LetK

-- | Global identifier.
data DefI = DefI { DefI -> IKind
ikind :: IKind, DefI -> QName
aname :: A.QName }

-- | Scope check signature.
type Sig = [(C.QName,DefI)]

emptySig :: Sig
emptySig :: Sig
emptySig = []

lookupSigU :: C.Name -> Sig -> Maybe DefI
lookupSigU :: Name -> Sig -> Maybe DefI
lookupSigU Name
n = QName -> Sig -> Maybe DefI
lookupSig (Name -> QName
C.QName Name
n)

lookupSig :: C.QName -> Sig -> Maybe DefI
lookupSig :: QName -> Sig -> Maybe DefI
lookupSig QName
n [] = Maybe DefI
forall a. Maybe a
Nothing
lookupSig QName
n ((QName
x,DefI
k):Sig
xs) = if (QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
n) then DefI -> Maybe DefI
forall a. a -> Maybe a
Just DefI
k else QName -> Sig -> Maybe DefI
lookupSig QName
n Sig
xs

-- ** State of scope checker.

data SCState = SCState
  { SCState -> Sig
signature  :: Sig
  , SCState -> Int
nextMeta   :: MVar
  , SCState -> Int
nextPolVar :: MVar
  }

initSt :: SCState
initSt :: SCState
initSt = Sig -> Int -> Int -> SCState
SCState Sig
emptySig Int
0 Int
0

-- * The scope checking monad.

-- | Scope checking monad.
--
-- Reader monad for local environment of variables (used in expresssions and patterns).
-- State monad (hidden) for global signature.
-- Error monad for reporting scope violations.
newtype ScopeCheck a = ScopeCheck { forall a.
ScopeCheck a
-> ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
unScopeCheck ::
  ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a }
  deriving ((forall a b. (a -> b) -> ScopeCheck a -> ScopeCheck b)
-> (forall a b. a -> ScopeCheck b -> ScopeCheck a)
-> Functor ScopeCheck
forall a b. a -> ScopeCheck b -> ScopeCheck a
forall a b. (a -> b) -> ScopeCheck a -> ScopeCheck b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> ScopeCheck a -> ScopeCheck b
fmap :: forall a b. (a -> b) -> ScopeCheck a -> ScopeCheck b
$c<$ :: forall a b. a -> ScopeCheck b -> ScopeCheck a
<$ :: forall a b. a -> ScopeCheck b -> ScopeCheck a
Functor, Functor ScopeCheck
Functor ScopeCheck =>
(forall a. a -> ScopeCheck a)
-> (forall a b.
    ScopeCheck (a -> b) -> ScopeCheck a -> ScopeCheck b)
-> (forall a b c.
    (a -> b -> c) -> ScopeCheck a -> ScopeCheck b -> ScopeCheck c)
-> (forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck b)
-> (forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck a)
-> Applicative ScopeCheck
forall a. a -> ScopeCheck a
forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck a
forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck b
forall a b. ScopeCheck (a -> b) -> ScopeCheck a -> ScopeCheck b
forall a b c.
(a -> b -> c) -> ScopeCheck a -> ScopeCheck b -> ScopeCheck 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
$cpure :: forall a. a -> ScopeCheck a
pure :: forall a. a -> ScopeCheck a
$c<*> :: forall a b. ScopeCheck (a -> b) -> ScopeCheck a -> ScopeCheck b
<*> :: forall a b. ScopeCheck (a -> b) -> ScopeCheck a -> ScopeCheck b
$cliftA2 :: forall a b c.
(a -> b -> c) -> ScopeCheck a -> ScopeCheck b -> ScopeCheck c
liftA2 :: forall a b c.
(a -> b -> c) -> ScopeCheck a -> ScopeCheck b -> ScopeCheck c
$c*> :: forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck b
*> :: forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck b
$c<* :: forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck a
<* :: forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck a
Applicative, Applicative ScopeCheck
Applicative ScopeCheck =>
(forall a b. ScopeCheck a -> (a -> ScopeCheck b) -> ScopeCheck b)
-> (forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck b)
-> (forall a. a -> ScopeCheck a)
-> Monad ScopeCheck
forall a. a -> ScopeCheck a
forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck b
forall a b. ScopeCheck a -> (a -> ScopeCheck b) -> ScopeCheck 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
$c>>= :: forall a b. ScopeCheck a -> (a -> ScopeCheck b) -> ScopeCheck b
>>= :: forall a b. ScopeCheck a -> (a -> ScopeCheck b) -> ScopeCheck b
$c>> :: forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck b
>> :: forall a b. ScopeCheck a -> ScopeCheck b -> ScopeCheck b
$creturn :: forall a. a -> ScopeCheck a
return :: forall a. a -> ScopeCheck a
Monad,
    MonadReader SCCxt, MonadError TraceError)

runScopeCheck
  :: SCCxt          -- ^ Local variable mapping.
  -> SCState        -- ^ Global identifier mapping.
  -> ScopeCheck a   -- ^ The computation.
  -> Either TraceError (a, SCState)
runScopeCheck :: forall a.
SCCxt -> SCState -> ScopeCheck a -> Either TraceError (a, SCState)
runScopeCheck SCCxt
ctx SCState
st (ScopeCheck ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
sc) = Identity (Either TraceError (a, SCState))
-> Either TraceError (a, SCState)
forall a. Identity a -> a
runIdentity (Identity (Either TraceError (a, SCState))
 -> Either TraceError (a, SCState))
-> Identity (Either TraceError (a, SCState))
-> Either TraceError (a, SCState)
forall a b. (a -> b) -> a -> b
$ ExceptT TraceError Identity (a, SCState)
-> Identity (Either TraceError (a, SCState))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT TraceError Identity (a, SCState)
 -> Identity (Either TraceError (a, SCState)))
-> ExceptT TraceError Identity (a, SCState)
-> Identity (Either TraceError (a, SCState))
forall a b. (a -> b) -> a -> b
$
  StateT SCState (ExceptT TraceError Identity) a
-> SCState -> ExceptT TraceError Identity (a, SCState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> SCCxt -> StateT SCState (ExceptT TraceError Identity) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
sc SCCxt
ctx) SCState
st

-- ** Local state.

-- | Add a local identifier.
--   (Not tail recursive, since it also returns the generate id.)
addBind' :: Show e => e -> C.Name -> (A.Name -> ScopeCheck a) -> ScopeCheck (A.Name, a)
addBind' :: forall e a.
Show e =>
e -> Name -> (Name -> ScopeCheck a) -> ScopeCheck (Name, a)
addBind' e
e Name
n Name -> ScopeCheck a
k = do
  ctx <- ScopeCheck SCCxt
forall r (m :: * -> *). MonadReader r m => m r
ask
  case retrieve n (thisLevel ctx) of
    Just Name
_  -> e -> Name -> ScopeCheck (Name, a)
forall {m :: * -> *} {a} {a} {a}.
(MonadError TraceError m, Show a, Show a) =>
a -> a -> m a
errorAlreadyInContext e
e Name
n
    Maybe Name
Nothing -> do
      let (Name
x, SCCxt
ctx') = Name -> SCCxt -> (Name, SCCxt)
forall b. Push Local b => Name -> b -> (Name, b)
newLocal Name
n SCCxt
ctx -- addCtx' n ctx
      a <- (SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a
forall a. (SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (SCCxt -> SCCxt -> SCCxt
forall a b. a -> b -> a
const SCCxt
ctx') (ScopeCheck a -> ScopeCheck a) -> ScopeCheck a -> ScopeCheck a
forall a b. (a -> b) -> a -> b
$ Name -> ScopeCheck a
k Name
x
      return (x, a)

addBind :: Show e => e -> C.Name -> ScopeCheck a -> ScopeCheck (A.Name, a)
addBind :: forall e a.
Show e =>
e -> Name -> ScopeCheck a -> ScopeCheck (Name, a)
addBind e
e Name
n ScopeCheck a
k = e -> Name -> (Name -> ScopeCheck a) -> ScopeCheck (Name, a)
forall e a.
Show e =>
e -> Name -> (Name -> ScopeCheck a) -> ScopeCheck (Name, a)
addBind' e
e Name
n ((Name -> ScopeCheck a) -> ScopeCheck (Name, a))
-> (Name -> ScopeCheck a) -> ScopeCheck (Name, a)
forall a b. (a -> b) -> a -> b
$ ScopeCheck a -> Name -> ScopeCheck a
forall a b. a -> b -> a
const ScopeCheck a
k

addBinds :: Show e => e -> [C.Name] -> ScopeCheck a -> ScopeCheck ([A.Name], a)
addBinds :: forall e a.
Show e =>
e -> [Name] -> ScopeCheck a -> ScopeCheck ([Name], a)
addBinds e
e [Name]
ns ScopeCheck a
k = (Name -> ScopeCheck ([Name], a) -> ScopeCheck ([Name], a))
-> ScopeCheck ([Name], a) -> [Name] -> ScopeCheck ([Name], a)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> ScopeCheck ([Name], a) -> ScopeCheck ([Name], a)
forall {b}.
Name -> ScopeCheck ([Name], b) -> ScopeCheck ([Name], b)
step ScopeCheck ([Name], a)
forall {a}. ScopeCheck ([a], a)
start [Name]
ns where
  start :: ScopeCheck ([a], a)
start    = do
    a <- ScopeCheck a
k
    return ([], a)
  step :: Name -> ScopeCheck ([Name], b) -> ScopeCheck ([Name], b)
step Name
n ScopeCheck ([Name], b)
k = do
    (x, (xs, a)) <- e
-> Name -> ScopeCheck ([Name], b) -> ScopeCheck (Name, ([Name], b))
forall e a.
Show e =>
e -> Name -> ScopeCheck a -> ScopeCheck (Name, a)
addBind e
e Name
n ScopeCheck ([Name], b)
k
    return (x:xs, a)

-- | Add local variable without checking shadowing.
addLocal :: C.Name -> (A.Name -> ScopeCheck a) -> ScopeCheck a
addLocal :: forall a. Name -> (Name -> ScopeCheck a) -> ScopeCheck a
addLocal Name
n Name -> ScopeCheck a
k = do
  ctx <- ScopeCheck SCCxt
forall r (m :: * -> *). MonadReader r m => m r
ask
  let (x, ctx') = newLocal n ctx
  local (const ctx') $ k x

addTel :: C.Telescope -> A.Telescope -> ScopeCheck a -> ScopeCheck a
addTel :: forall a. Telescope -> Telescope -> ScopeCheck a -> ScopeCheck a
addTel Telescope
ctel Telescope
atel = (SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a
forall a. (SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (PatCtx -> SCCxt -> SCCxt
addContext PatCtx
nxs)
  where nxs :: PatCtx
nxs = PatCtx -> PatCtx
forall a. [a] -> [a]
reverse (PatCtx -> PatCtx) -> PatCtx -> PatCtx
forall a b. (a -> b) -> a -> b
$ Telescope -> Telescope -> PatCtx
zipTels Telescope
ctel Telescope
atel

zipTels :: C.Telescope -> A.Telescope -> [(C.Name,A.Name)]
zipTels :: Telescope -> Telescope -> PatCtx
zipTels Telescope
ctel Telescope
atel = [Name] -> [Name] -> PatCtx
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Name]
xs
  where ns :: [Name]
ns = Telescope -> [Name]
collectTelescopeNames Telescope
ctel
        xs :: [Name]
xs = (TBind -> Name) -> [TBind] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TBind -> Name
forall a. TBinding a -> Name
A.boundName ([TBind] -> [Name]) -> [TBind] -> [Name]
forall a b. (a -> b) -> a -> b
$ Telescope -> [TBind]
A.telescope Telescope
atel

-- ** Global state.

getSig :: ScopeCheck Sig
getSig :: ScopeCheck Sig
getSig = ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) Sig
-> ScopeCheck Sig
forall a.
ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> ScopeCheck a
ScopeCheck (ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) Sig
 -> ScopeCheck Sig)
-> ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) Sig
-> ScopeCheck Sig
forall a b. (a -> b) -> a -> b
$ (SCState -> Sig)
-> ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) Sig
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SCState -> Sig
signature

-- | Add a global identifier.
addName :: IKind -> C.Name -> ScopeCheck A.Name
addName :: IKind -> Name -> ScopeCheck Name
addName IKind
k Name
n = do
  sig <- ScopeCheck Sig
getSig
  when (isJust (lookupSig (C.QName n) sig)) $
    errorAlreadyInSignature "shadowing of global definitions forbidden" n
  let x = String -> Name
A.fresh (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ Name -> String
C.theName Name
n
  addANameU k n x
  return x

-- addNameU :: IKind -> C.Name -> ScopeCheck A.Name
-- addNameU k n = A.unqual <$> addName k (C.QName n)

-- | Add an already translated global identifier.
addAName :: IKind -> C.QName -> A.QName -> ScopeCheck ()
addAName :: IKind -> QName -> QName -> ScopeCheck ()
addAName IKind
k QName
n QName
x = ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) ()
-> ScopeCheck ()
forall a.
ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> ScopeCheck a
ScopeCheck (ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) ()
 -> ScopeCheck ())
-> ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) ()
-> ScopeCheck ()
forall a b. (a -> b) -> a -> b
$ (SCState -> SCState)
-> ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SCState -> SCState)
 -> ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) ())
-> (SCState -> SCState)
-> ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) ()
forall a b. (a -> b) -> a -> b
$ \ SCState
st ->
  SCState
st { signature = (n, DefI k x) : signature st }

addANameU :: IKind -> C.Name -> A.Name -> ScopeCheck ()
addANameU :: IKind -> Name -> Name -> ScopeCheck ()
addANameU IKind
ki Name
n Name
x = IKind -> QName -> QName -> ScopeCheck ()
addAName IKind
ki (Name -> QName
C.QName Name
n) (Name -> QName
A.QName Name
x)

-- | Add or reuse an unqualified name.
overloadName :: IKind -> C.Name -> ScopeCheck A.Name
overloadName :: IKind -> Name -> ScopeCheck Name
overloadName IKind
k Name
n = do
  sig <- ScopeCheck Sig
getSig
  case lookupSigU n sig of
    Maybe DefI
Nothing -> do
      let x :: Name
x = String -> Name
A.fresh (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ Name -> String
C.theName Name
n
      IKind -> Name -> Name -> ScopeCheck ()
addANameU IKind
k Name
n Name
x
      Name -> ScopeCheck Name
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
    Just (DefI IKind
k' (A.QName Name
x)) -> Name -> ScopeCheck Name
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x

{- UNUSED
addDecl :: C.Declaration -> ScopeCheck A.Name
addDecl (C.DataDecl n _ _ _ _ _ _) = addName DataK n
addDecl (C.RecordDecl n _ _ _ _)   = addName DataK n
-}
{- UNUSED
addFunDecl :: Bool -> C.Declaration -> ScopeCheck A.Name
addFunDecl b (C.FunDecl _ ts _) = addTypeSig (FunK b) ts
-}

addTypeSig :: IKind -> C.TypeSig -> A.TypeSig -> ScopeCheck ()
addTypeSig :: IKind -> TypeSig -> TypeSig -> ScopeCheck ()
addTypeSig IKind
kind (C.TypeSig Name
n Expr
_) (A.TypeSig Name
x Expr
_) = IKind -> Name -> Name -> ScopeCheck ()
addANameU IKind
kind Name
n Name
x

{- UNUSED
-- | Add a global identifier.  Fail if already in signature.
addGlobal :: Show d => d -> IKind -> C.Name -> ScopeCheck A.Name
addGlobal d k n = enterShow n $ do
  sig <- getSig
  case lookupSig n sig of
    Just _  -> errorAlreadyInSignature d n
    Nothing -> addName k n
-}

-- | Create a meta variable.
nextMVar :: (MVar -> ScopeCheck a) -> ScopeCheck a
nextMVar :: forall a. (Int -> ScopeCheck a) -> ScopeCheck a
nextMVar Int -> ScopeCheck a
f = ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> ScopeCheck a
forall a.
ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> ScopeCheck a
ScopeCheck (ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
 -> ScopeCheck a)
-> ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> ScopeCheck a
forall a b. (a -> b) -> a -> b
$ do
  st <- ReaderT
  SCCxt (StateT SCState (ExceptT TraceError Identity)) SCState
forall s (m :: * -> *). MonadState s m => m s
get
  put $ st { nextMeta = nextMeta st + 1 }
  unScopeCheck $ f (nextMeta st)

-- | Create a polarity meta variable.
nextPVar :: (MVar -> ScopeCheck a) -> ScopeCheck a
nextPVar :: forall a. (Int -> ScopeCheck a) -> ScopeCheck a
nextPVar Int -> ScopeCheck a
f = ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> ScopeCheck a
forall a.
ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> ScopeCheck a
ScopeCheck (ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
 -> ScopeCheck a)
-> ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> ScopeCheck a
forall a b. (a -> b) -> a -> b
$ do
  st <- ReaderT
  SCCxt (StateT SCState (ExceptT TraceError Identity)) SCState
forall s (m :: * -> *). MonadState s m => m s
get
  put $ st { nextPolVar = nextPolVar st + 1 }
  unScopeCheck $ f (nextPolVar st)

-- ** Additional services of scope monad.

-- | Default polarity is context-sensitive.
setDefaultPolarity :: Pol -> ScopeCheck a -> ScopeCheck a
setDefaultPolarity :: forall a. Pol -> ScopeCheck a -> ScopeCheck a
setDefaultPolarity Pol
p = (SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a
forall a. (SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ SCCxt
sccxt -> SCCxt
sccxt { defaultPolarity = p })
{-
insertingPolVars :: Bool -> ScopeCheck a -> ScopeCheck a
insertingPolVars b = local (\ sccxt -> sccxt { insertPolVars = b })
-}

-- | Insert polarity variables for omitted polarities.
generalizeDec :: A.Dec -> ScopeCheck A.Dec
generalizeDec :: Dec -> ScopeCheck Dec
generalizeDec dec :: Dec
dec@Dec
A.Hidden = Dec -> ScopeCheck Dec
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Dec
dec
generalizeDec dec :: Dec
dec@A.Dec{}  =
  if (Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
polarity Dec
dec Pol -> Pol -> Bool
forall a. Eq a => a -> a -> Bool
== Pol
Default) then do
    p0 <- (SCCxt -> Pol) -> ScopeCheck Pol
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SCCxt -> Pol
defaultPolarity
    case p0 of
      PVar{} -> (Int -> ScopeCheck Dec) -> ScopeCheck Dec
forall a. (Int -> ScopeCheck a) -> ScopeCheck a
nextPVar ((Int -> ScopeCheck Dec) -> ScopeCheck Dec)
-> (Int -> ScopeCheck Dec) -> ScopeCheck Dec
forall a b. (a -> b) -> a -> b
$ \ Int
i ->
                  Dec -> ScopeCheck Dec
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dec -> ScopeCheck Dec) -> Dec -> ScopeCheck Dec
forall a b. (a -> b) -> a -> b
$ Pol -> Dec -> Dec
forall a. LensPol a => Pol -> a -> a
setPol (Int -> Pol
PVar Int
i) Dec
dec
      Pol
_      -> Dec -> ScopeCheck Dec
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dec -> ScopeCheck Dec) -> Dec -> ScopeCheck Dec
forall a b. (a -> b) -> a -> b
$ Pol -> Dec -> Dec
forall a. LensPol a => Pol -> a -> a
setPol Pol
p0 Dec
dec
   else Dec -> ScopeCheck Dec
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Dec
dec

generalizeTBind :: C.TBind -> ScopeCheck C.TBind
generalizeTBind :: TBind -> ScopeCheck TBind
generalizeTBind tb :: TBind
tb@C.TMeasure{} = TBind -> ScopeCheck TBind
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return TBind
tb
generalizeTBind TBind
tb = do
  dec' <- Dec -> ScopeCheck Dec
generalizeDec (TBind -> Dec
forall a. TBinding a -> Dec
C.boundDec TBind
tb)
  return $ tb { C.boundDec = dec' }

-- | Insert polarity variables in telescope.
generalizeTel :: C.Telescope -> ScopeCheck C.Telescope
generalizeTel :: Telescope -> ScopeCheck Telescope
generalizeTel = (TBind -> ScopeCheck TBind) -> Telescope -> ScopeCheck Telescope
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TBind -> ScopeCheck TBind
generalizeTBind

-- * Scope checking concrete syntax.
----------------------------------------------------------------------

scopeCheckDecls :: [C.Declaration] -> ScopeCheck [A.Declaration]
scopeCheckDecls :: [Declaration] -> ScopeCheck [Declaration]
scopeCheckDecls = (Declaration -> ScopeCheck Declaration)
-> [Declaration] -> ScopeCheck [Declaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Declaration -> ScopeCheck Declaration
scopeCheckDeclaration

scopeCheckDeclaration :: C.Declaration -> ScopeCheck A.Declaration

scopeCheckDeclaration :: Declaration -> ScopeCheck Declaration
scopeCheckDeclaration (C.OverrideDecl Override
Check [Declaration]
ds) = ReaderT
  SCCxt (StateT SCState (ExceptT TraceError Identity)) Declaration
-> ScopeCheck Declaration
forall a.
ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> ScopeCheck a
ScopeCheck (ReaderT
   SCCxt (StateT SCState (ExceptT TraceError Identity)) Declaration
 -> ScopeCheck Declaration)
-> ReaderT
     SCCxt (StateT SCState (ExceptT TraceError Identity)) Declaration
-> ScopeCheck Declaration
forall a b. (a -> b) -> a -> b
$ do
  st <- ReaderT
  SCCxt (StateT SCState (ExceptT TraceError Identity)) SCState
forall s (m :: * -> *). MonadState s m => m s
get
  as <- unScopeCheck $ scopeCheckDecls ds -- declarations need to scope check
  put st                   -- but then forget their effect: restore old state
  return $ A.OverrideDecl Check as

scopeCheckDeclaration (C.OverrideDecl Override
Fail [Declaration]
ds) = ReaderT
  SCCxt (StateT SCState (ExceptT TraceError Identity)) Declaration
-> ScopeCheck Declaration
forall a.
ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a
-> ScopeCheck a
ScopeCheck (ReaderT
   SCCxt (StateT SCState (ExceptT TraceError Identity)) Declaration
 -> ScopeCheck Declaration)
-> ReaderT
     SCCxt (StateT SCState (ExceptT TraceError Identity)) Declaration
-> ScopeCheck Declaration
forall a b. (a -> b) -> a -> b
$ do
  st <- ReaderT
  SCCxt (StateT SCState (ExceptT TraceError Identity)) SCState
forall s (m :: * -> *). MonadState s m => m s
get
  as <- unScopeCheck $ scopeCheckDecls ds
               `catchError` (const $ return [])  --on error discard block
  put st
  return $ A.OverrideDecl Fail as
{-
scopeCheckDeclaration (C.OverrideDecl Fail ds) = do
  st <- get
  (as,st') <- (do as  <- scopeCheckDecls ds
                  st' <- get
                  return (as,st'))
               `catchError` (const $ return ([],st))  --on error discard block
  put st'
  return $ A.OverrideDecl Fail as
-}
scopeCheckDeclaration (C.OverrideDecl Override
override [Declaration]
ds) = do -- TrustMe,Impredicative
  as <- [Declaration] -> ScopeCheck [Declaration]
scopeCheckDecls [Declaration]
ds
  return $ A.OverrideDecl override as

scopeCheckDeclaration (C.RecordDecl Name
n Telescope
tel Expr
t Constructor
c [Name]
fields) =
  Name
-> Telescope
-> Expr
-> Constructor
-> [Name]
-> ScopeCheck Declaration
scopeCheckRecordDecl Name
n Telescope
tel Expr
t Constructor
c [Name]
fields

scopeCheckDeclaration d :: Declaration
d@(C.DataDecl{}) =
  Declaration -> ScopeCheck Declaration
scopeCheckDataDecl Declaration
d -- >>= return . (:[])

scopeCheckDeclaration d :: Declaration
d@(C.FunDecl Co
co TypeSig
_ [Clause]
_) =
  Co -> [Declaration] -> ScopeCheck Declaration
scopeCheckFunDecls Co
co [Declaration
d] -- >>= return . (:[])

scopeCheckDeclaration (C.LetDecl Bool
eval letdef :: LetDef
letdef@C.LetDef{ letDefDec :: LetDef -> Dec
C.letDefDec = Dec
dec, letDefName :: LetDef -> Name
C.letDefName = Name
n }) = do
  Bool -> ScopeCheck () -> ScopeCheck ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Dec
dec Dec -> Dec -> Bool
forall a. Eq a => a -> a -> Bool
== Dec
A.defaultDec) (ScopeCheck () -> ScopeCheck ()) -> ScopeCheck () -> ScopeCheck ()
forall a b. (a -> b) -> a -> b
$
    String -> ScopeCheck ()
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> ScopeCheck ()) -> String -> ScopeCheck ()
forall a b. (a -> b) -> a -> b
$ String
"polarity annotation not supported in global let definition of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
  (tel, mt, e) <- LetDef -> ScopeCheck (Telescope, Maybe Expr, Expr)
scopeCheckLetDef LetDef
letdef
  x <- addName LetK n
  return $ A.LetDecl eval x tel mt e

scopeCheckDeclaration d :: Declaration
d@(C.PatternDecl Name
n [Name]
ns Pattern
p) = do
  let errorHead :: String
errorHead = String
"invalid pattern declaration\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Declaration -> String
C.prettyDecl Declaration
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
  -- check pattern
  (p, delta) <- StateT PatCtx ScopeCheck (Pat Expr)
-> PatCtx -> ScopeCheck (Pat Expr, PatCtx)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Pattern -> StateT PatCtx ScopeCheck (Pat Expr)
scopeCheckPattern Pattern
p) PatCtx
emptyCtx
  p <- local (addContext delta) $ scopeCheckDotPattern p
  -- ensure that pattern variables are the declared variables
  unless (sort ns == sort (map fst delta)) $ do
    let usedNames = (Local -> Name) -> PatCtx -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Local -> Name
forall a b. (a, b) -> a
fst PatCtx
delta
        unusedNames = [Name]
ns [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
usedNames
        undeclaredNames = [Name]
usedNames [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
ns
    when (not (null unusedNames)) $ throwErrorMsg $
      errorHead ++ "unsed variables in pattern: "
        ++ Util.showList " " show unusedNames
    when (not (null undeclaredNames)) $ throwErrorMsg $
      errorHead ++ "undeclared variables in pattern: "
        ++ Util.showList " " show undeclaredNames
  --  when (n `elem` ns) $ throwErrorMsg $ errorHead ++ "pattern"
  x <- addName (ConK DefPat) n
  let xs = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Name -> Name
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Name -> Name) -> (Name -> Maybe Name) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> PatCtx -> Maybe Name) -> PatCtx -> Name -> Maybe Name
forall a b c. (a -> b -> c) -> b -> a -> c
flip Name -> PatCtx -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup PatCtx
delta) [Name]
ns
  return (A.PatternDecl x xs p)

-- we support
-- - mutual (co)funs
-- - mutual (co)data

scopeCheckDeclaration (C.MutualDecl []) = String -> ScopeCheck Declaration
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg String
"empty mutual block"
scopeCheckDeclaration (C.MutualDecl l :: [Declaration]
l@(C.DataDecl{}:[Declaration]
xl)) =
  [Declaration] -> ScopeCheck Declaration
scopeCheckMutual [Declaration]
l
scopeCheckDeclaration (C.MutualDecl l :: [Declaration]
l@(C.FunDecl  Co
co TypeSig
_ [Clause]
_:[Declaration]
xl)) =
  Co -> [Declaration] -> ScopeCheck Declaration
scopeCheckFunDecls Co
co [Declaration]
l  -- >>= return . (:[])
scopeCheckDeclaration (C.MutualDecl [Declaration]
_) = String -> ScopeCheck Declaration
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg String
"mutual combination not supported"

scopeCheckLetDef :: C.LetDef -> ScopeCheck (A.Telescope, Maybe (A.Type), A.Expr)
scopeCheckLetDef :: LetDef -> ScopeCheck (Telescope, Maybe Expr, Expr)
scopeCheckLetDef (C.LetDef Dec
dec Name
n Telescope
tel Maybe Expr
mt Expr
e) =  Pol
-> ScopeCheck (Telescope, Maybe Expr, Expr)
-> ScopeCheck (Telescope, Maybe Expr, Expr)
forall a. Pol -> ScopeCheck a -> ScopeCheck a
setDefaultPolarity Pol
A.Rec (ScopeCheck (Telescope, Maybe Expr, Expr)
 -> ScopeCheck (Telescope, Maybe Expr, Expr))
-> ScopeCheck (Telescope, Maybe Expr, Expr)
-> ScopeCheck (Telescope, Maybe Expr, Expr)
forall a b. (a -> b) -> a -> b
$ do
  tel <- Telescope -> ScopeCheck Telescope
generalizeTel Telescope
tel
  (tel, (mt, e)) <- scopeCheckTele tel $ do
     (,) <$> mapM scopeCheckExprN mt  -- allow shadowing after : in type
         <*> scopeCheckExprN e        -- allow shadowing after =
  return (tel, mt, e)

{- scopeCheck Mutual block
first check signatures
then bodies
-}
scopeCheckMutual :: [C.Declaration] -> ScopeCheck A.Declaration
scopeCheckMutual :: [Declaration] -> ScopeCheck Declaration
scopeCheckMutual [Declaration]
ds0 = do
  -- flatten nested mutual blocks and override decls
  ds <- [Declaration] -> ScopeCheck [Declaration]
mutualFlattenDecls [Declaration]
ds0
  -- extract, check, and add type signatures
  let ktsigs = (Declaration -> (IKind, TypeSig))
-> [Declaration] -> [(IKind, TypeSig)]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> (IKind, TypeSig)
mutualGetTypeSig [Declaration]
ds
  (mmm, tsigs') <- unzip <$> mapM checkAndAddTypeSig ktsigs
  -- funs have been added with internal names
  -- check that all functions are unmeasured or have a same length measure
  let (ns, mll) = unzip $ compressMaybes mmm
  let measured = [Maybe Int] -> Bool
forall a. Null a => a -> Bool
null [Maybe Int]
mll Bool -> Bool -> Bool
|| Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust ([Maybe Int] -> Maybe Int
forall a. HasCallStack => [a] -> a
head [Maybe Int]
mll)
  let ok = [Maybe Int] -> Bool
forall a. Null a => a -> Bool
null [Maybe Int]
mll Bool -> Bool -> Bool
|| (Maybe Int -> Bool) -> [Maybe Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (([Maybe Int] -> Maybe Int
forall a. HasCallStack => [a] -> a
head [Maybe Int]
mll)Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
==) ([Maybe Int] -> [Maybe Int]
forall a. HasCallStack => [a] -> [a]
tail [Maybe Int]
mll)
  when (not ok) $ throwErrorMsg $ "in a mutual function block, either all functions must be without measure or have a measure of the same length"
{-
  -- switch to internal fun ids
  let funNames = [ n | (FunK _ , A.TypeSig n _) <- ktsigs ] -- internal fun names
{- SAME W/O COMPR
  let funNames = map (\ (_, C.TypeSig n _) -> n) $ filter aux ktsigs where
                   aux (FunK _, _) = True
                   aux _ = False
-}
  mapM_ (addName (FunK False)) funNames -- TODO
-}
  -- check bodies of declarations
  ds' <- mapM (setDefaultPolarity A.Rec . checkBody) (zip tsigs' ds)
  -- switch back to external fun ids
  let funNames = [ Name
x | A.FunDecl Co
_ (A.Fun TypeSig
_ Name
x Arity
_ [Clause]
_) <- [Declaration]
ds' ] -- external fun names
  zipWithM_ (addANameU (LetK)) ns funNames
--  zipWithM_ (addAName (FunK True)) ns funNames
  return $ A.MutualDecl measured ds'

scopeCheckTele :: C.Telescope -> ScopeCheck a -> ScopeCheck (A.Telescope, a)
scopeCheckTele :: forall a. Telescope -> ScopeCheck a -> ScopeCheck (Telescope, a)
scopeCheckTele []         ScopeCheck a
cont = (Telescope
A.emptyTel,) (a -> (Telescope, a)) -> ScopeCheck a -> ScopeCheck (Telescope, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ScopeCheck a
cont
scopeCheckTele (TBind
tb : Telescope
tel) ScopeCheck a
cont = do
  (tbs, (A.Telescope tel, a)) <- TBind
-> ScopeCheck (Telescope, a)
-> ScopeCheck ([TBind], (Telescope, a))
forall a. TBind -> ScopeCheck a -> ScopeCheck ([TBind], a)
scopeCheckTBind TBind
tb (ScopeCheck (Telescope, a) -> ScopeCheck ([TBind], (Telescope, a)))
-> ScopeCheck (Telescope, a)
-> ScopeCheck ([TBind], (Telescope, a))
forall a b. (a -> b) -> a -> b
$ Telescope -> ScopeCheck a -> ScopeCheck (Telescope, a)
forall a. Telescope -> ScopeCheck a -> ScopeCheck (Telescope, a)
scopeCheckTele Telescope
tel ScopeCheck a
cont
  return (A.Telescope $ tbs ++ tel, a)

scopeCheckTBind :: C.TBind -> ScopeCheck a -> ScopeCheck ([A.TBind], a)
scopeCheckTBind :: forall a. TBind -> ScopeCheck a -> ScopeCheck ([TBind], a)
scopeCheckTBind TBind
tb ScopeCheck a
cont = do
  let contYes :: ScopeCheck a
contYes = Bool -> ScopeCheck a -> ScopeCheck a
forall a. LensConstraintAllowed a => Bool -> a -> a
setConstraintAllowed Bool
True  ScopeCheck a
cont
      contNo :: ScopeCheck a
contNo  = Bool -> ScopeCheck a -> ScopeCheck a
forall a. LensConstraintAllowed a => Bool -> a -> a
setConstraintAllowed Bool
False ScopeCheck a
cont
  case TBind
tb of
    C.TBind Dec
dec [] Expr
t -> do -- non-dependent function type
      t       <- Expr -> ScopeCheck Expr
scopeCheckExprN Expr
t
      ([A.noBind $ A.Domain t A.defaultKind dec],) <$> contNo
    C.TBind Dec
dec [Name]
ns Expr
t -> do
      t       <- Expr -> ScopeCheck Expr
scopeCheckExprN Expr
t
      (xs, a) <- addBinds tb ns $ contYes
      return (map (\ Name
x -> Name -> Dom Expr -> TBind
forall a. Name -> Dom a -> TBinding a
A.TBind Name
x (Expr -> Kind -> Dec -> Dom Expr
forall a. a -> Kind -> Dec -> Dom a
A.Domain Expr
t Kind
A.defaultKind Dec
dec)) xs, a)
    C.TBounded Dec
dec Name
n LtLe
ltle Expr
e -> do
      e <- Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e
      (x, a) <- addBind tb n $ contYes
      return ([A.TBind x (A.Domain (A.Below ltle e) A.defaultKind dec)], a)
    C.TMeasure Measure Expr
mu -> do
      mu <- Measure Expr -> ScopeCheck (Measure Expr)
scopeCheckMeasure Measure Expr
mu
      ([A.TMeasure mu],) <$> cont
--    C.TMeasure mu -> throwErrorMsg $ "measure not allowed in telescope"
    C.TBound Bound Expr
beta -> do
      ScopeCheck Bool -> ScopeCheck () -> ScopeCheck ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((SCCxt -> Bool) -> ScopeCheck Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SCCxt -> Bool
constraintAllowed) (ScopeCheck () -> ScopeCheck ()) -> ScopeCheck () -> ScopeCheck ()
forall a b. (a -> b) -> a -> b
$
        Bound Expr -> ScopeCheck ()
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorConstraintNotAllowed Bound Expr
beta
      beta <- Bound Expr -> ScopeCheck (Bound Expr)
scopeCheckBound Bound Expr
beta
      ([A.TBound beta],) <$> cont

checkBody :: (A.TypeSig, C.Declaration) -> ScopeCheck A.Declaration
checkBody :: (TypeSig, Declaration) -> ScopeCheck Declaration
checkBody (A.TypeSig Name
x Expr
tt, C.DataDecl Name
n Sized
sz Co
co Telescope
tel Expr
_ [Constructor]
cs [Name]
fields) =
  Expr
-> Name
-> Name
-> Sized
-> Co
-> Telescope
-> [Constructor]
-> [Name]
-> ScopeCheck Declaration
checkDataBody Expr
tt Name
n Name
x Sized
sz Co
co Telescope
tel [Constructor]
cs [Name]
fields
checkBody (ts :: TypeSig
ts@(A.TypeSig Name
n Expr
t), d :: Declaration
d@(C.FunDecl Co
co TypeSig
tsig [Clause]
cls)) = do
  (ar,cls') <- Declaration -> ScopeCheck (Arity, [Clause])
scopeCheckFunClauses Declaration
d
  let n' = Name -> Name
A.mkExtName Name
n
  return $ A.FunDecl co $ A.Fun ts n' ar cls'

mutualFlattenDecls :: [C.Declaration] -> ScopeCheck [C.Declaration]
mutualFlattenDecls :: [Declaration] -> ScopeCheck [Declaration]
mutualFlattenDecls [Declaration]
ds = (Declaration -> ScopeCheck [Declaration])
-> [Declaration] -> ScopeCheck [[Declaration]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Declaration -> ScopeCheck [Declaration]
mutualFlattenDecl [Declaration]
ds ScopeCheck [[Declaration]]
-> ([[Declaration]] -> ScopeCheck [Declaration])
-> ScopeCheck [Declaration]
forall a b. ScopeCheck a -> (a -> ScopeCheck b) -> ScopeCheck b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Declaration] -> ScopeCheck [Declaration]
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Declaration] -> ScopeCheck [Declaration])
-> ([[Declaration]] -> [Declaration])
-> [[Declaration]]
-> ScopeCheck [Declaration]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Declaration]] -> [Declaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat

mutualFlattenDecl :: C.Declaration -> ScopeCheck [C.Declaration]
mutualFlattenDecl :: Declaration -> ScopeCheck [Declaration]
mutualFlattenDecl (C.MutualDecl [Declaration]
ds) = [Declaration] -> ScopeCheck [Declaration]
mutualFlattenDecls [Declaration]
ds
mutualFlattenDecl (C.OverrideDecl Override
Fail [Declaration]
_) = String -> ScopeCheck [Declaration]
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> ScopeCheck [Declaration])
-> String -> ScopeCheck [Declaration]
forall a b. (a -> b) -> a -> b
$ String
"fail declaration not supported in mutual block"
mutualFlattenDecl (C.OverrideDecl Override
o [Declaration]
ds) = do
  ds' <- [Declaration] -> ScopeCheck [Declaration]
mutualFlattenDecls [Declaration]
ds
  return $ map (\ Declaration
d -> Override -> [Declaration] -> Declaration
C.OverrideDecl Override
o [Declaration
d]) ds'
mutualFlattenDecl (C.LetDecl{}) = String -> ScopeCheck [Declaration]
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> ScopeCheck [Declaration])
-> String -> ScopeCheck [Declaration]
forall a b. (a -> b) -> a -> b
$ String
"let in mutual block not supported"
mutualFlattenDecl Declaration
d = [Declaration] -> ScopeCheck [Declaration]
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Declaration] -> ScopeCheck [Declaration])
-> [Declaration] -> ScopeCheck [Declaration]
forall a b. (a -> b) -> a -> b
$ [Declaration
d]

-- extract type sigs of a mutual block in order, error on nested mutual
mutualGetTypeSig :: C.Declaration -> (IKind, C.TypeSig)
mutualGetTypeSig :: Declaration -> (IKind, TypeSig)
mutualGetTypeSig (C.DataDecl Name
n Sized
sz Co
co Telescope
tel Expr
t [Constructor]
cs [Name]
fields) =
  (IKind
DataK, Name -> Expr -> TypeSig
C.TypeSig Name
n (Telescope -> Expr -> Expr
C.teleToType Telescope
tel Expr
t))
mutualGetTypeSig (C.FunDecl Co
co TypeSig
tsig [Clause]
cls) =
  (Bool -> IKind
FunK Bool
False, TypeSig
tsig) -- fun id for use inside defining body
mutualGetTypeSig (C.LetDecl Bool
ev (C.LetDef Dec
dec Name
n Telescope
tel Maybe Expr
Nothing Expr
e)) =
  String -> (IKind, TypeSig)
forall a. HasCallStack => String -> a
error (String -> (IKind, TypeSig)) -> String -> (IKind, TypeSig)
forall a b. (a -> b) -> a -> b
$ String
"let declaration of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": type required in mutual block"
mutualGetTypeSig (C.LetDecl Bool
ev (C.LetDef Dec
dec Name
n Telescope
tel (Just Expr
t) Expr
e)) =
  (IKind
LetK, Name -> Expr -> TypeSig
C.TypeSig Name
n (Telescope -> Expr -> Expr
C.teleToType Telescope
tel Expr
t))
{- mutualGetTypeSig (C.LetDecl ev tsig e) =
  (LetK, tsig) -}
mutualGetTypeSig (C.OverrideDecl Override
_ [Declaration
d]) =
  Declaration -> (IKind, TypeSig)
mutualGetTypeSig Declaration
d


scopeCheckRecordDecl :: C.Name -> C.Telescope -> C.Type -> C.Constructor -> [C.Name] ->
  ScopeCheck A.Declaration
scopeCheckRecordDecl :: Name
-> Telescope
-> Expr
-> Constructor
-> [Name]
-> ScopeCheck Declaration
scopeCheckRecordDecl Name
n Telescope
tel Expr
t Constructor
c [Name]
cfields = Name -> ScopeCheck Declaration -> ScopeCheck Declaration
forall (m :: * -> *) a b.
(MonadError TraceError m, Show a) =>
a -> m b -> m b
enterShow Name
n (ScopeCheck Declaration -> ScopeCheck Declaration)
-> ScopeCheck Declaration -> ScopeCheck Declaration
forall a b. (a -> b) -> a -> b
$ do
  Pol -> ScopeCheck Declaration -> ScopeCheck Declaration
forall a. Pol -> ScopeCheck a -> ScopeCheck a
setDefaultPolarity Pol
A.Param (ScopeCheck Declaration -> ScopeCheck Declaration)
-> ScopeCheck Declaration -> ScopeCheck Declaration
forall a b. (a -> b) -> a -> b
$ do
    tel <- Telescope -> ScopeCheck Telescope
generalizeTel Telescope
tel
    -- STALE COMMENT: we do not infer at all: -- do not infer polarities in index arguments
    (A.TypeSig x tt') <- scopeCheckTypeSig (C.TypeSig n $ C.teleToType tel t)
    addANameU DataK n x
    let names = Telescope -> [Name]
collectTelescopeNames Telescope
tel
        target = Expr -> [Expr] -> Expr
C.App (Name -> Expr
C.ident Name
n) ((Name -> Expr) -> [Name] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Expr
C.ident [Name]
names)  -- R pars
        (tel',t') = A.typeToTele' (length names) tt'
    c' <- scopeCheckConstructor n x (zipTels tel tel') A.CoInd target c
    let delta = Constructor -> Constructor -> PatCtx
contextFromConstructors Constructor
c Constructor
c'
    afields <- addFields ProjK delta cfields
    return $ A.RecordDecl x tel' t' c' afields

contextFromConstructors :: C.Constructor -> A.Constructor -> Context
contextFromConstructors :: Constructor -> Constructor -> PatCtx
contextFromConstructors (C.Constructor Name
_ Telescope
ctel0 Maybe Expr
mct) (A.Constructor QName
_ ParamPats
_ Expr
at) = PatCtx
delta
  where ctel :: Telescope
ctel = Telescope -> (Expr -> Telescope) -> Maybe Expr -> Telescope
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((Telescope, Expr) -> Telescope
forall a b. (a, b) -> a
fst ((Telescope, Expr) -> Telescope)
-> (Expr -> (Telescope, Expr)) -> Expr -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> (Telescope, Expr)
C.typeToTele) Maybe Expr
mct
        (Telescope
atel, Expr
_) = Expr -> (Telescope, Expr)
A.typeToTele Expr
at
        delta :: PatCtx
delta = Telescope -> Telescope -> PatCtx
zipTels (Telescope
ctel0 Telescope -> Telescope -> Telescope
forall a. [a] -> [a] -> [a]
++ Telescope
ctel) Telescope
atel

scopeCheckField :: Context -> C.Name -> ScopeCheck A.Name
scopeCheckField :: PatCtx -> Name -> ScopeCheck Name
scopeCheckField PatCtx
delta Name
n =
  case Name -> PatCtx -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n PatCtx
delta of
    Maybe Name
Nothing -> Name -> ScopeCheck Name
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorNotAField Name
n
    Just Name
x  -> Name -> ScopeCheck Name
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> ScopeCheck Name) -> Name -> ScopeCheck Name
forall a b. (a -> b) -> a -> b
$ Name
x

addFields :: IKind -> Context -> [C.Name] -> ScopeCheck [A.Name]
addFields :: IKind -> PatCtx -> [Name] -> ScopeCheck [Name]
addFields IKind
kind PatCtx
delta [Name]
cfields = do
    afields <- (Name -> ScopeCheck Name) -> [Name] -> ScopeCheck [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (PatCtx -> Name -> ScopeCheck Name
scopeCheckField PatCtx
delta) [Name]
cfields
    mapM_ (uncurry $ addANameU kind) $ zip cfields afields
    return afields

scopeCheckDataDecl :: C.Declaration -> ScopeCheck A.Declaration
scopeCheckDataDecl :: Declaration -> ScopeCheck Declaration
scopeCheckDataDecl decl :: Declaration
decl@(C.DataDecl Name
n Sized
sz Co
co Telescope
tel0 Expr
t [Constructor]
cs [Name]
fields) = Name -> ScopeCheck Declaration -> ScopeCheck Declaration
forall (m :: * -> *) a b.
(MonadError TraceError m, Show a) =>
a -> m b -> m b
enterShow Name
n (ScopeCheck Declaration -> ScopeCheck Declaration)
-> ScopeCheck Declaration -> ScopeCheck Declaration
forall a b. (a -> b) -> a -> b
$ do
  Pol -> ScopeCheck Declaration -> ScopeCheck Declaration
forall a. Pol -> ScopeCheck a -> ScopeCheck a
setDefaultPolarity Pol
A.Param (ScopeCheck Declaration -> ScopeCheck Declaration)
-> ScopeCheck Declaration -> ScopeCheck Declaration
forall a b. (a -> b) -> a -> b
$ do
    tel <- Telescope -> ScopeCheck Telescope
generalizeTel Telescope
tel0
    -- STALE: -- do not infer polarities in index arguments
    (A.TypeSig x tt') <- scopeCheckTypeSig (C.TypeSig n $ C.teleToType tel t)
    addANameU DataK n x
    checkDataBody tt' n x sz co tel cs fields

-- precondition: name already added to signature
checkDataBody :: A.Type -> C.Name -> A.Name -> Sized -> Co -> C.Telescope -> [C.Constructor] -> [C.Name] -> ScopeCheck A.Declaration
checkDataBody :: Expr
-> Name
-> Name
-> Sized
-> Co
-> Telescope
-> [Constructor]
-> [Name]
-> ScopeCheck Declaration
checkDataBody Expr
tt' Name
n Name
x Sized
sz Co
co Telescope
tel [Constructor]
cs [Name]
fields = do
      let cnames :: [Name]
cnames = Telescope -> [Name]
collectTelescopeNames Telescope
tel         -- parameters
          target :: Expr
target = Expr -> [Expr] -> Expr
C.App (Name -> Expr
C.ident Name
n) ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (Name -> Expr) -> [Name] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Expr
C.ident [Name]
cnames  -- D pars
          (Telescope
tel',Expr
t') = Int -> Expr -> (Telescope, Expr)
A.typeToTele' ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
cnames) Expr
tt'
      cs' <- (Constructor -> ScopeCheck Constructor)
-> [Constructor] -> ScopeCheck [Constructor]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name
-> Name
-> PatCtx
-> Co
-> Expr
-> Constructor
-> ScopeCheck Constructor
scopeCheckConstructor Name
n Name
x (Telescope -> Telescope -> PatCtx
zipTels Telescope
tel Telescope
tel') Co
co Expr
target) [Constructor]
cs
{- NO LONGER INFER DESTRUCTORS
      -- traceM ("constructors: " ++ show cs')
--      when (t' == A.Sort A.Set && length cs' == 1) $ do
--      when (length cs' == 1) $ do  -- TOO STRICT, DOES NOT TREAT Vec right
      let cis = A.analyzeConstructors co n tel' cs'
      flip mapM_ cis $ \ ci -> when (A.cEtaExp ci) $ do
-- Add destructor names
        let fields = A.cFields ci -- A.classifyFields co n (A.typePart c)
        -- TODO Check for recursive occurrence!
        -- when (A.etaExpandable fields) $
        let destrNames =  A.destructorNames fields
        --when (not (null (destrNames))) $
        -- traceM ("fields: " ++ show fields)
        -- traceM ("destructors: " ++ show destrNames)
        mapM_ (addName (FunK True)) $ destrNames -- destructors are also upped
 {-
        let (ctel,_) = A.typeToTele (A.typePart (head cs'))
        let destrNames = map (\(_,x,_) -> x) ctel
        when (all (/= "") destrNames) $
          mapM_ (addName (FunK True)) destrNames -- destructors are also upped
-}
-}
      -- add declared destructor names
      let delta = Stack -> PatCtx
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Stack -> PatCtx) -> Stack -> PatCtx
forall a b. (a -> b) -> a -> b
$ ((Constructor, Constructor) -> PatCtx)
-> [(Constructor, Constructor)] -> Stack
forall a b. (a -> b) -> [a] -> [b]
map ((Constructor -> Constructor -> PatCtx)
-> (Constructor, Constructor) -> PatCtx
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Constructor -> Constructor -> PatCtx
contextFromConstructors) ([(Constructor, Constructor)] -> Stack)
-> [(Constructor, Constructor)] -> Stack
forall a b. (a -> b) -> a -> b
$ [Constructor] -> [Constructor] -> [(Constructor, Constructor)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Constructor]
cs [Constructor]
cs'
      -- fields <- addFields (LetK) delta fields
      -- 2012-01-26 register as projections
      fields <- addFields ProjK delta fields
      let pos = (TBind -> Pol) -> [TBind] -> [Pol]
forall a b. (a -> b) -> [a] -> [b]
map (Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
A.polarity (Dec -> Pol) -> (TBind -> Dec) -> TBind -> Pol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Expr -> Dec
forall a. Dom a -> Dec
A.decor (Dom Expr -> Dec) -> (TBind -> Dom Expr) -> TBind -> Dec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TBind -> Dom Expr
forall a. TBinding a -> Dom a
A.boundDom) ([TBind] -> [Pol]) -> [TBind] -> [Pol]
forall a b. (a -> b) -> a -> b
$ Telescope -> [TBind]
A.telescope Telescope
tel'
      return $ A.DataDecl x sz co pos tel' t' cs' fields

-- check whether all declarations in mutual block are (co)funs
checkFunMutual :: Co -> [C.Declaration] -> ScopeCheck ()
checkFunMutual :: Co -> [Declaration] -> ScopeCheck ()
checkFunMutual Co
co [] = () -> ScopeCheck ()
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkFunMutual Co
co (C.FunDecl Co
co' TypeSig
_ [Clause]
_:[Declaration]
xl) | Co
co Co -> Co -> Bool
forall a. Eq a => a -> a -> Bool
== Co
co' = Co -> [Declaration] -> ScopeCheck ()
checkFunMutual Co
co [Declaration]
xl
checkFunMutual Co
_ [Declaration]
_ = String -> ScopeCheck ()
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg String
"mutual combination not supported"

scopeCheckFunDecls :: Co -> [C.Declaration] -> ScopeCheck A.Declaration
scopeCheckFunDecls :: Co -> [Declaration] -> ScopeCheck Declaration
scopeCheckFunDecls Co
co [Declaration]
l = do
  -- check for uniformity of mutual block (all funs/all cofuns)
  Co -> [Declaration] -> ScopeCheck ()
checkFunMutual Co
co [Declaration]
l
  -- check signatures and look for measures
  r <- (Declaration -> ScopeCheck (Maybe Int, TypeSig))
-> [Declaration] -> ScopeCheck [(Maybe Int, TypeSig)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\ (C.FunDecl Co
_ TypeSig
tysig [Clause]
_) -> TypeSig -> ScopeCheck (Maybe Int, TypeSig)
scopeCheckFunSig TypeSig
tysig) [Declaration]
l
  let (ml:mll, tsl') = unzip r
  let ok = (Maybe Int -> Bool) -> [Maybe Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe Int
mlMaybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
==) [Maybe Int]
mll
  when (not ok) $ throwErrorMsg $ "in a mutual function block, either all functions must be without measure or have a measure of the same length"
  -- add names as internal ids and check bodies
  let nxs = (Declaration -> TypeSig -> Local)
-> [Declaration] -> [TypeSig] -> PatCtx
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ (C.FunDecl Co
_ (C.TypeSig Name
n Expr
_) [Clause]
_) (A.TypeSig Name
x Expr
_) -> (Name
n,Name
x)) [Declaration]
l [TypeSig]
tsl'
  --let addFuns b = mapM (uncurry $ addAName $ FunK b) nxs
--  let addFuns b = mapM (\ (n,x) -> addAName (FunK b) n x) nxs
  -- addFuns False
  mapM_ (uncurry $ addANameU $ FunK False) nxs
  arcll' <- mapM (setDefaultPolarity A.Rec . scopeCheckFunClauses) l
  -- add names as external ids
  --addFuns True
  let nxs' = (Local -> Local) -> PatCtx -> PatCtx
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> Name) -> (Name -> Name) -> Local -> Local
forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
mapPair Name -> Name
forall a. a -> a
id Name -> Name
A.mkExtName) PatCtx
nxs
  mapM_ (uncurry $ addANameU (LetK)) nxs'
--  mapM (uncurry $ addAName (FunK True)) nxs'
  return $ A.MutualFunDecl (isJust ml) co $
    zipWith3 (\ TypeSig
ts (Name
_, Name
x') (Arity
ar, [Clause]
cls) -> TypeSig -> Name -> Arity -> [Clause] -> Fun
A.Fun TypeSig
ts Name
x' Arity
ar [Clause]
cls) tsl' nxs' arcll'

-- | Does not add name to signature.
scopeCheckFunSig :: C.TypeSig -> ScopeCheck (Maybe Int, A.TypeSig)
scopeCheckFunSig :: TypeSig -> ScopeCheck (Maybe Int, TypeSig)
scopeCheckFunSig d :: TypeSig
d@(C.TypeSig Name
n Expr
t) = TypeSig
-> Name
-> (Name -> ScopeCheck (Maybe Int, TypeSig))
-> ScopeCheck (Maybe Int, TypeSig)
forall d a.
Show d =>
d -> Name -> (Name -> ScopeCheck a) -> ScopeCheck a
checkInSig TypeSig
d Name
n ((Name -> ScopeCheck (Maybe Int, TypeSig))
 -> ScopeCheck (Maybe Int, TypeSig))
-> (Name -> ScopeCheck (Maybe Int, TypeSig))
-> ScopeCheck (Maybe Int, TypeSig)
forall a b. (a -> b) -> a -> b
$ \ Name
x -> do
    (ml, t') <- Expr -> ScopeCheck (Maybe Int, Expr)
scopeCheckFunType Expr
t
    return (ml, A.TypeSig x t')

-- scope check type of mutual function, return length of measure (if present)
-- a fun type is a telescope followed by (maybe) a measure and a type expression
scopeCheckFunType :: C.Expr -> ScopeCheck (Maybe Int, A.Expr)
scopeCheckFunType :: Expr -> ScopeCheck (Maybe Int, Expr)
scopeCheckFunType Expr
t =
  case Expr
t of

      -- found a measure: continue normal scope checking
      C.Quant PiSigma
A.Pi [C.TMeasure Measure Expr
mu] Expr
e1 -> do
        mu' <- Measure Expr -> ScopeCheck (Measure Expr)
scopeCheckMeasure Measure Expr
mu
        e1' <- scopeCheckExprN e1
        return (Just $ length (measure mu'), A.pi (A.TMeasure mu') e1')

      -- bounds are allowed here, since we check a function type
      C.Quant PiSigma
A.Pi [C.TBound Bound Expr
beta] Expr
e1 -> do
        beta'     <- Bound Expr -> ScopeCheck (Bound Expr)
scopeCheckBound Bound Expr
beta
        (ml, e1') <- scopeCheckFunType e1
        return (ml, A.pi (A.TBound beta') e1')

      C.Quant PiSigma
A.Pi Telescope
tel Expr
e -> do
        tel <- Telescope -> ScopeCheck Telescope
generalizeTel Telescope
tel
        (tel, (ml, e)) <- setDefaultPolarity A.Rec $ setConstraintAllowed False $
          scopeCheckTele tel $ setConstraintAllowed True $ scopeCheckFunType e
        ml' <- findMeasure tel
        ml <- case (ml,ml') of
                 (Maybe Int
Nothing,Maybe Int
ml') -> Maybe Int -> ScopeCheck (Maybe Int)
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
ml'
                 (Maybe Int
ml, Maybe Int
Nothing) -> Maybe Int -> ScopeCheck (Maybe Int)
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
ml
                 (Just{}, Just{}) -> ScopeCheck (Maybe Int)
forall {m :: * -> *} {a}. MonadError TraceError m => m a
errorOnlyOneMeasure
        return (ml, A.teleToType tel e)

      Expr
t -> (Maybe Int
forall a. Maybe a
Nothing,) (Expr -> (Maybe Int, Expr))
-> ScopeCheck Expr -> ScopeCheck (Maybe Int, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ScopeCheck Expr
scopeCheckExpr Expr
t -- no measure found

findMeasure :: A.Telescope -> ScopeCheck (Maybe Int)
findMeasure :: Telescope -> ScopeCheck (Maybe Int)
findMeasure (A.Telescope [TBind]
tel) =
  case [ Measure Expr
mu | A.TMeasure Measure Expr
mu <- [TBind]
tel ] of
    []           -> Maybe Int -> ScopeCheck (Maybe Int)
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
    [Measure [Expr]
mu] -> Maybe Int -> ScopeCheck (Maybe Int)
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> ScopeCheck (Maybe Int))
-> Maybe Int -> ScopeCheck (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
mu
    [Measure Expr]
_            -> ScopeCheck (Maybe Int)
forall {m :: * -> *} {a}. MonadError TraceError m => m a
errorOnlyOneMeasure

-- | Check whether concrete name is already in signature.
--   If yes, fail. If no, create abstract name and continue.
checkInSig :: Show d => d -> C.Name -> (A.Name -> ScopeCheck a) -> ScopeCheck a
checkInSig :: forall d a.
Show d =>
d -> Name -> (Name -> ScopeCheck a) -> ScopeCheck a
checkInSig d
d Name
n Name -> ScopeCheck a
k = Name -> ScopeCheck a -> ScopeCheck a
forall (m :: * -> *) a b.
(MonadError TraceError m, Show a) =>
a -> m b -> m b
enterShow Name
n (ScopeCheck a -> ScopeCheck a) -> ScopeCheck a -> ScopeCheck a
forall a b. (a -> b) -> a -> b
$ do
  sig <- ScopeCheck Sig
getSig
  case lookupSig (C.QName n) sig of
    Just DefI
_  -> d -> Name -> ScopeCheck a
forall {m :: * -> *} {a} {a} {a}.
(MonadError TraceError m, Show a, Show a) =>
a -> a -> m a
errorAlreadyInSignature d
d Name
n
    Maybe DefI
Nothing -> Name -> ScopeCheck a
k (String -> Name
A.fresh (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ Name -> String
C.theName Name
n)

-- checkInSigU :: Show d => d -> C.Name -> (A.Name -> ScopeCheck a) -> ScopeCheck a
-- checkInSigU d n k = checkInSig d (C.QName n) (k . A.unqual)

scopeCheckFunClauses :: C.Declaration -> ScopeCheck (Arity, [A.Clause])
scopeCheckFunClauses :: Declaration -> ScopeCheck (Arity, [Clause])
scopeCheckFunClauses (C.FunDecl Co
_ (C.TypeSig Name
n Expr
_) [Clause]
cl) = Name
-> ScopeCheck (Arity, [Clause]) -> ScopeCheck (Arity, [Clause])
forall (m :: * -> *) a b.
(MonadError TraceError m, Show a) =>
a -> m b -> m b
enterShow Name
n (ScopeCheck (Arity, [Clause]) -> ScopeCheck (Arity, [Clause]))
-> ScopeCheck (Arity, [Clause]) -> ScopeCheck (Arity, [Clause])
forall a b. (a -> b) -> a -> b
$ do
  cl <- (Clause -> ScopeCheck Clause) -> [Clause] -> ScopeCheck [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Maybe Name -> Clause -> ScopeCheck Clause
scopeCheckClause (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n)) [Clause]
cl
  let m = if [Clause] -> Bool
forall a. Null a => a -> Bool
null [Clause]
cl then Int
0 else
       (Int -> Int -> Int) -> [Int] -> Int
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
List.foldl1 Int -> Int -> Int
forall a. Ord a => a -> a -> a
min ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Clause -> Int) -> [Clause] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ([Pattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Pattern] -> Int) -> (Clause -> [Pattern]) -> Clause -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Pattern]
A.clPatterns) [Clause]
cl
  return (A.Arity m Nothing, cl)
{-
       let b = checkPatternLength cl
       case b of
          Just m  -> return $ (A.Arity m Nothing, cl)
          Nothing -> throwErrorMsg $ " pattern length differs"
-}

-- | Check the type of a signature and generate abstract name.
--   Does not add abstract name to signature.
scopeCheckTypeSig :: C.TypeSig -> ScopeCheck A.TypeSig
scopeCheckTypeSig :: TypeSig -> ScopeCheck TypeSig
scopeCheckTypeSig d :: TypeSig
d@(C.TypeSig Name
n Expr
t) = TypeSig
-> Name -> (Name -> ScopeCheck TypeSig) -> ScopeCheck TypeSig
forall d a.
Show d =>
d -> Name -> (Name -> ScopeCheck a) -> ScopeCheck a
checkInSig TypeSig
d Name
n ((Name -> ScopeCheck TypeSig) -> ScopeCheck TypeSig)
-> (Name -> ScopeCheck TypeSig) -> ScopeCheck TypeSig
forall a b. (a -> b) -> a -> b
$ \ Name
x -> do
    t' <- Expr -> ScopeCheck Expr
scopeCheckExpr Expr
t
    return $ A.TypeSig x t'

-- | Results:
--
--     @Nothing@            Not a function declaration.
--
--     @Just (n, Nothing)@  Unmeasured function.
--
--     @Just (n, Just m)@   Function with measure of length m
checkAndAddTypeSig :: (IKind, C.TypeSig) -> ScopeCheck (Maybe (C.Name, Maybe Int), A.TypeSig)
checkAndAddTypeSig :: (IKind, TypeSig) -> ScopeCheck (Maybe (Name, Maybe Int), TypeSig)
checkAndAddTypeSig (IKind
kind, ts :: TypeSig
ts@(C.TypeSig Name
n Expr
_)) = do
  (mm, ts'@(A.TypeSig x _)) <-
    case IKind
kind of
      FunK Bool
_ -> (Maybe Int -> Maybe (Name, Maybe Int))
-> (TypeSig -> TypeSig)
-> (Maybe Int, TypeSig)
-> (Maybe (Name, Maybe Int), TypeSig)
forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
mapPair ((Name, Maybe Int) -> Maybe (Name, Maybe Int)
forall a. a -> Maybe a
Just ((Name, Maybe Int) -> Maybe (Name, Maybe Int))
-> (Maybe Int -> (Name, Maybe Int))
-> Maybe Int
-> Maybe (Name, Maybe Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
n,)) TypeSig -> TypeSig
forall a. a -> a
id ((Maybe Int, TypeSig) -> (Maybe (Name, Maybe Int), TypeSig))
-> ScopeCheck (Maybe Int, TypeSig)
-> ScopeCheck (Maybe (Name, Maybe Int), TypeSig)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeSig -> ScopeCheck (Maybe Int, TypeSig)
scopeCheckFunSig TypeSig
ts
{-
        do
        (mi, ts) <- scopeCheckFunSig ts
        return (Just mi, ts)
-}
      IKind
_ -> (Maybe (Name, Maybe Int)
forall a. Maybe a
Nothing,) (TypeSig -> (Maybe (Name, Maybe Int), TypeSig))
-> ScopeCheck TypeSig
-> ScopeCheck (Maybe (Name, Maybe Int), TypeSig)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeSig -> ScopeCheck TypeSig
scopeCheckTypeSig TypeSig
ts
  addANameU kind n x  -- or: addTypeSig kind ts ts'
  return (mm, ts')

collectTelescopeNames :: C.Telescope -> [C.Name]
collectTelescopeNames :: Telescope -> [Name]
collectTelescopeNames = [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Name]] -> [Name])
-> (Telescope -> [[Name]]) -> Telescope -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TBind -> [Name]) -> Telescope -> [[Name]]
forall a b. (a -> b) -> [a] -> [b]
map TBind -> [Name]
forall a. TBinding a -> [Name]
C.boundNames

-- | Check whether concrete name is already in signature.
--   If yes, fail. If no, create abstract name and continue.
checkConsInSig :: Show decl => decl -> C.Name -> A.Name -> IKind -> C.Name -> (A.QName -> ScopeCheck a) -> ScopeCheck a
checkConsInSig :: forall decl a.
Show decl =>
decl
-> Name
-> Name
-> IKind
-> Name
-> (QName -> ScopeCheck a)
-> ScopeCheck a
checkConsInSig decl
decl Name
d Name
dx IKind
ki Name
n QName -> ScopeCheck a
cont = Name -> ScopeCheck a -> ScopeCheck a
forall (m :: * -> *) a b.
(MonadError TraceError m, Show a) =>
a -> m b -> m b
enterShow Name
n (ScopeCheck a -> ScopeCheck a) -> ScopeCheck a -> ScopeCheck a
forall a b. (a -> b) -> a -> b
$ do
  -- first check whether the datatype has this constructor already
  ScopeCheck (Maybe DefI)
-> (DefI -> ScopeCheck a) -> ScopeCheck a -> ScopeCheck a
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> (a -> m b) -> m b -> m b
ifJustM (QName -> Sig -> Maybe DefI
lookupSig (Name -> Name -> QName
C.Qual Name
d Name
n) (Sig -> Maybe DefI) -> ScopeCheck Sig -> ScopeCheck (Maybe DefI)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ScopeCheck Sig
getSig) (ScopeCheck a -> DefI -> ScopeCheck a
forall a b. a -> b -> a
const (ScopeCheck a -> DefI -> ScopeCheck a)
-> ScopeCheck a -> DefI -> ScopeCheck a
forall a b. (a -> b) -> a -> b
$ decl -> Name -> ScopeCheck a
forall {m :: * -> *} {a} {a} {a}.
(MonadError TraceError m, Show a, Show a) =>
a -> a -> m a
errorAlreadyInSignature decl
decl Name
n) (ScopeCheck a -> ScopeCheck a) -> ScopeCheck a -> ScopeCheck a
forall a b. (a -> b) -> a -> b
$ do
  -- then check the overloaded name and possibly add it
  x <- IKind -> Name -> ScopeCheck Name
overloadName IKind
ki Name
n
  -- the qualified name is added in the continuation
  cont $ A.Qual dx x

-- | @cxt@ is the data telescope.
scopeCheckConstructor :: C.Name -> A.Name -> Context -> Co -> C.Type -> C.Constructor -> ScopeCheck A.Constructor
scopeCheckConstructor :: Name
-> Name
-> PatCtx
-> Co
-> Expr
-> Constructor
-> ScopeCheck Constructor
scopeCheckConstructor Name
d Name
dx PatCtx
cxt Co
co Expr
t0 a :: Constructor
a@(C.Constructor Name
n Telescope
tel Maybe Expr
mt) = do
  let ki :: IKind
ki = ConK -> IKind
ConK (ConK -> IKind) -> ConK -> IKind
forall a b. (a -> b) -> a -> b
$ Co -> ConK
A.coToConK Co
co
  Constructor
-> Name
-> Name
-> IKind
-> Name
-> (QName -> ScopeCheck Constructor)
-> ScopeCheck Constructor
forall decl a.
Show decl =>
decl
-> Name
-> Name
-> IKind
-> Name
-> (QName -> ScopeCheck a)
-> ScopeCheck a
checkConsInSig Constructor
a Name
d Name
dx IKind
ki Name
n ((QName -> ScopeCheck Constructor) -> ScopeCheck Constructor)
-> (QName -> ScopeCheck Constructor) -> ScopeCheck Constructor
forall a b. (a -> b) -> a -> b
$ \ QName
x -> do

  let finish :: Expr -> Maybe PatCtx -> ScopeCheck Constructor
finish Expr
t Maybe PatCtx
mcxt = (SCCxt -> SCCxt)
-> ScopeCheck Constructor -> ScopeCheck Constructor
forall a. (SCCxt -> SCCxt) -> ScopeCheck a -> ScopeCheck a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (PatCtx -> SCCxt -> SCCxt
addContext (PatCtx -> SCCxt -> SCCxt) -> PatCtx -> SCCxt -> SCCxt
forall a b. (a -> b) -> a -> b
$ PatCtx -> (PatCtx -> PatCtx) -> Maybe PatCtx -> PatCtx
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PatCtx
cxt PatCtx -> PatCtx
forall a. a -> a
id Maybe PatCtx
mcxt) (ScopeCheck Constructor -> ScopeCheck Constructor)
-> ScopeCheck Constructor -> ScopeCheck Constructor
forall a b. (a -> b) -> a -> b
$ do
       t <- Pol -> ScopeCheck Expr -> ScopeCheck Expr
forall a. Pol -> ScopeCheck a -> ScopeCheck a
setDefaultPolarity Pol
A.Param (ScopeCheck Expr -> ScopeCheck Expr)
-> ScopeCheck Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ Expr -> ScopeCheck Expr
scopeCheckExpr (Expr -> ScopeCheck Expr) -> Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
C.teleToType Telescope
tel Expr
t
       t <- adjustTopDecsM defaultToParam t
       addAName ki (C.Qual d n) x
       let dummyDom = Expr -> Kind -> Dec -> Dom Expr
forall a. a -> Kind -> Dec -> Dom a
A.Domain Expr
A.Irr Kind
A.NoKind (Dec -> Dom Expr) -> Dec -> Dom Expr
forall a b. (a -> b) -> a -> b
$ Pol -> Dec
forall pos. pos -> Decoration pos
A.Dec Pol
Param
           mtel     = (PatCtx -> [TBind]) -> Maybe PatCtx -> Maybe [TBind]
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Local -> TBind) -> PatCtx -> [TBind]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n,Name
x) -> Name -> Dom Expr -> TBind
forall a. Name -> Dom a -> TBinding a
A.TBind Name
x Dom Expr
dummyDom)) Maybe PatCtx
mcxt
           ps       = [] -- patterns computed during type checking
       return $ A.Constructor x (fmap ((,ps) . A.Telescope) mtel) t

  case Maybe Expr
mt of

    -- no target given, then add the data tel to the scope
    Maybe Expr
Nothing -> Expr -> Maybe PatCtx -> ScopeCheck Constructor
finish Expr
t0 Maybe PatCtx
forall a. Maybe a
Nothing

    -- target given, then the target binds the parameter names
    Just Expr
t -> do
      -- get the final target
      let (Telescope
_, Expr
target) = Expr -> (Telescope, Expr)
C.typeToTele Expr
t

          fallback :: ScopeCheck Constructor
fallback = Expr -> Maybe PatCtx -> ScopeCheck Constructor
finish Expr
t Maybe PatCtx
forall a. Maybe a
Nothing
          continue :: Name -> [Expr] -> ScopeCheck Constructor
continue Name
d' [Expr]
es = do
            -- unless (d == d') $ errorWrongTarget n d d'
            if (Name
d Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
d') then ScopeCheck Constructor
fallback else do
            -- get the parameters of target
            let ([Expr]
pars, [Expr]
inds) = Int -> [Expr] -> ([Expr], [Expr])
forall a. Int -> [a] -> ([a], [a])
splitAt (PatCtx -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PatCtx
cxt) [Expr]
es
            Bool -> ScopeCheck () -> ScopeCheck ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
pars Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== PatCtx -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PatCtx
cxt) (ScopeCheck () -> ScopeCheck ()) -> ScopeCheck () -> ScopeCheck ()
forall a b. (a -> b) -> a -> b
$ Name -> Expr -> ScopeCheck ()
forall {m :: * -> *} {a} {a} {a}.
(MonadError TraceError m, Show a, Show a) =>
a -> a -> m a
errorNotEnoughParameters Name
n Expr
target
            -- if parameters are just data parameters, do it old style
            if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Local -> Expr -> Bool) -> PatCtx -> [Expr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Local -> Expr -> Bool
forall {b}. (Name, b) -> Expr -> Bool
isTelPar PatCtx
cxt [Expr]
pars) then ScopeCheck Constructor
fallback else do
            -- scopeCheck the parameters as patterns
            Expr -> Maybe PatCtx -> ScopeCheck Constructor
finish Expr
t (Maybe PatCtx -> ScopeCheck Constructor)
-> (PatCtx -> Maybe PatCtx) -> PatCtx -> ScopeCheck Constructor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatCtx -> Maybe PatCtx
forall a. a -> Maybe a
Just (PatCtx -> ScopeCheck Constructor)
-> ScopeCheck PatCtx -> ScopeCheck Constructor
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Expr] -> ScopeCheck PatCtx
parameterVariables [Expr]
pars

      case Expr
target of
        C.Ident (C.QName Name
d')            -> Name -> [Expr] -> ScopeCheck Constructor
continue Name
d' []
        C.App (C.Ident (C.QName Name
d')) [Expr]
es -> Name -> [Expr] -> ScopeCheck Constructor
continue Name
d' [Expr]
es
        Expr
_ -> ScopeCheck Constructor
fallback -- errorTargetMustBeAppliedName n target

{- OLD CODE
scopeCheckConstructor :: C.Telescope -> A.Telescope -> Co -> C.Type -> C.Constructor -> ScopeCheck A.Constructor
scopeCheckConstructor ctel atel co t0 a@(C.Constructor n tel mt) = addTel ctel atel $ checkInSig a n $ \ x -> do
    let t = maybe t0 id mt
    t <- setDefaultPolarity A.Param $ scopeCheckExpr $ C.teleToType tel t
    t <- adjustTopDecsM defaultToParam t
    addAName (ConK $ A.coToConK co) n x
    return $ A.TypeSig x t
-}
  where isTelPar :: (Name, b) -> Expr -> Bool
isTelPar (Name
c,b
_) (C.Ident (C.QName Name
x)) = Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x
        isTelPar (Name, b)
_     Expr
_                     = Bool
False
        defaultToParam :: Dec -> m Dec
defaultToParam Dec
dec = case (Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
A.polarity Dec
dec) of
          Pol
A.Default -> Dec -> m Dec
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dec -> m Dec) -> Dec -> m Dec
forall a b. (a -> b) -> a -> b
$ Pol -> Dec -> Dec
forall a. LensPol a => Pol -> a -> a
setPol Pol
A.Param Dec
dec
          Pol
A.Param   -> Dec -> m Dec
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Dec
dec
          Pol
A.Const   -> Dec -> m Dec
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Dec
dec
          A.PVar{}  -> Dec -> m Dec
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Dec
dec
          Pol
_         -> String -> m Dec
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m Dec) -> String -> m Dec
forall a b. (a -> b) -> a -> b
$ String
"illegal polarity " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pol -> String
forall a. Show a => a -> String
show (Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
polarity Dec
dec) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in type of constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Constructor -> String
forall a. Show a => a -> String
show Constructor
a

-- | Allow shadowing of previous locals.
--   Always if we enter a subexpression which is not the body
--   of a binder.
scopeCheckExprN :: C.Expr -> ScopeCheck A.Expr
scopeCheckExprN :: Expr -> ScopeCheck Expr
scopeCheckExprN = ScopeCheck Expr -> ScopeCheck Expr
forall a. ScopeCheck a -> ScopeCheck a
newLevel (ScopeCheck Expr -> ScopeCheck Expr)
-> (Expr -> ScopeCheck Expr) -> Expr -> ScopeCheck Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ScopeCheck Expr
scopeCheckExpr

scopeCheckExpr :: C.Expr -> ScopeCheck A.Expr
scopeCheckExpr :: Expr -> ScopeCheck Expr
scopeCheckExpr Expr
e = Bool -> ScopeCheck Expr -> ScopeCheck Expr
forall a. LensConstraintAllowed a => Bool -> a -> a
setConstraintAllowed Bool
False (ScopeCheck Expr -> ScopeCheck Expr)
-> ScopeCheck Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ Expr -> ScopeCheck Expr
scopeCheckExpr' Expr
e

scopeCheckExpr' :: C.Expr -> ScopeCheck A.Expr
scopeCheckExpr' :: Expr -> ScopeCheck Expr
scopeCheckExpr' Expr
e =
    case Expr
e of
      -- replace underscore by next meta-variable
      Expr
C.Unknown -> (Int -> ScopeCheck Expr) -> ScopeCheck Expr
forall a. (Int -> ScopeCheck a) -> ScopeCheck a
nextMVar (Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeCheck Expr)
-> (Int -> Expr) -> Int -> ScopeCheck Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Expr
A.Meta)
      C.Set   Expr
e -> Sort Expr -> Expr
A.Sort (Sort Expr -> Expr) -> (Expr -> Sort Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Sort Expr
forall a. a -> Sort a
A.Set   (Expr -> Expr) -> ScopeCheck Expr -> ScopeCheck Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e
      C.CoSet Expr
e -> Sort Expr -> Expr
A.Sort (Sort Expr -> Expr) -> (Expr -> Sort Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Sort Expr
forall a. a -> Sort a
A.CoSet (Expr -> Expr) -> ScopeCheck Expr -> ScopeCheck Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e
      Expr
C.Size    -> Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeCheck Expr) -> Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ Sort Expr -> Expr
A.Sort (Class -> Sort Expr
forall a. Class -> Sort a
A.SortC Class
A.Size)
      C.Succ Expr
e1 -> Expr -> Expr
A.Succ (Expr -> Expr) -> ScopeCheck Expr -> ScopeCheck Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e1
      Expr
C.Zero    -> Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
A.Zero
      Expr
C.Infty   -> Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
A.Infty
      C.Plus Expr
e1 Expr
e2 -> do
        e1 <- Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e1
        e2 <- scopeCheckExprN e2
        return $ A.Plus [e1, e2]
      C.Pair Expr
e1 Expr
e2   -> Expr -> Expr -> Expr
A.Pair (Expr -> Expr -> Expr)
-> ScopeCheck Expr -> ScopeCheck (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e1 ScopeCheck (Expr -> Expr) -> ScopeCheck Expr -> ScopeCheck Expr
forall a b. ScopeCheck (a -> b) -> ScopeCheck a -> ScopeCheck b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e2
      C.Sing Expr
e1 Expr
et   -> Expr -> Expr -> Expr
A.Sing (Expr -> Expr -> Expr)
-> ScopeCheck Expr -> ScopeCheck (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e1 ScopeCheck (Expr -> Expr) -> ScopeCheck Expr -> ScopeCheck Expr
forall a b. ScopeCheck (a -> b) -> ScopeCheck a -> ScopeCheck b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
et
      C.App Expr
C.Max [Expr]
el -> do
        el' <- (Expr -> ScopeCheck Expr) -> [Expr] -> ScopeCheck [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Expr -> ScopeCheck Expr
scopeCheckExprN [Expr]
el
        when (length el' < 2) $ throwErrorMsg "max expects at least 2 arguments"
        return $ A.Max el'
      C.App Expr
e1 [Expr]
el -> (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
A.App (Expr -> [Expr] -> Expr)
-> ScopeCheck Expr -> ScopeCheck ([Expr] -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e1 ScopeCheck ([Expr] -> Expr) -> ScopeCheck [Expr] -> ScopeCheck Expr
forall a b. ScopeCheck (a -> b) -> ScopeCheck a -> ScopeCheck b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr -> ScopeCheck Expr) -> [Expr] -> ScopeCheck [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Expr -> ScopeCheck Expr
scopeCheckExprN [Expr]
el
      C.Case Expr
e Maybe Expr
mt [Clause]
cl -> do
        e'  <- Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e
        mt' <- mapM scopeCheckExprN mt
        cl' <- mapM (scopeCheckClause Nothing) cl
        return $ A.Case e' mt' cl'

      -- measure & bound
      -- measures can only appear in fun sigs!
      C.Quant PiSigma
pisig [C.TMeasure Measure Expr
mu] Expr
e1 -> do
        String -> ScopeCheck Expr
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> ScopeCheck Expr) -> String -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ String
"measure not allowed in expression " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e

      -- measure bound mu < mu'
      C.Quant PiSigma
A.Pi [C.TBound Bound Expr
beta] Expr
e1 -> do
        ScopeCheck Bool -> ScopeCheck () -> ScopeCheck ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((SCCxt -> Bool) -> ScopeCheck Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SCCxt -> Bool
constraintAllowed) (ScopeCheck () -> ScopeCheck ()) -> ScopeCheck () -> ScopeCheck ()
forall a b. (a -> b) -> a -> b
$ Bound Expr -> ScopeCheck ()
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorConstraintNotAllowed Bound Expr
beta
        beta' <- Bound Expr -> ScopeCheck (Bound Expr)
scopeCheckBound Bound Expr
beta
        e1'   <- scopeCheckExpr' e1
        return $ A.pi (A.TBound beta') e1'

      C.Quant PiSigma
A.Sigma [C.TBound Bound Expr
beta] Expr
e1 -> String -> ScopeCheck Expr
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> ScopeCheck Expr) -> String -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$
        String
"measure bound not allowed in expression " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e

      C.Quant PiSigma
pisig Telescope
tel Expr
e -> do
        tel <- Telescope -> ScopeCheck Telescope
generalizeTel Telescope
tel
        pol <- asks defaultPolarity
        (A.Telescope tel, e) <- setDefaultPolarity A.Rec $ setConstraintAllowed False $ scopeCheckTele tel $
           setDefaultPolarity pol $ scopeCheckExpr' e
        return $ quant pisig tel e where
--          quant A.Sigma [tb] = A.Quant A.Sigma tb
          quant :: PiSigma -> [TBind] -> Expr -> Expr
quant PiSigma
A.Sigma [TBind]
tel Expr
e = (TBind -> Expr -> Expr) -> Expr -> [TBind] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (PiSigma -> TBind -> Expr -> Expr
A.Quant PiSigma
A.Sigma) Expr
e [TBind]
tel
          quant PiSigma
A.Pi    [TBind]
tel Expr
e = Telescope -> Expr -> Expr
A.teleToType ([TBind] -> Telescope
A.Telescope [TBind]
tel) Expr
e

      C.Lam Name
n Expr
e1 -> do
        (n, e1') <- Expr -> Name -> ScopeCheck Expr -> ScopeCheck (Name, Expr)
forall e a.
Show e =>
e -> Name -> ScopeCheck a -> ScopeCheck (Name, a)
addBind Expr
e Name
n (ScopeCheck Expr -> ScopeCheck (Name, Expr))
-> ScopeCheck Expr -> ScopeCheck (Name, Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> ScopeCheck Expr
scopeCheckExpr Expr
e1
        return $ A.Lam A.defaultDec n e1' -- dec. in Lam is ignored in t.c.

      C.LLet LetDef
letdef Expr
e2 -> do
        let dec :: Dec
dec = LetDef -> Dec
C.letDefDec LetDef
letdef
        (tel, mt, e1) <- LetDef -> ScopeCheck (Telescope, Maybe Expr, Expr)
scopeCheckLetDef LetDef
letdef
        (x, e2) <- addBind e (C.letDefName letdef) $ scopeCheckExpr e2
        return $ A.LLet (A.TBind x $ A.Domain mt A.defaultKind dec) tel e1 e2

      C.Record [([Name], Expr)]
rs -> do
        let fields :: [[Name]]
fields = (([Name], Expr) -> [Name]) -> [([Name], Expr)] -> [[Name]]
forall a b. (a -> b) -> [a] -> [b]
map ([Name], Expr) -> [Name]
forall a b. (a, b) -> a
fst [([Name], Expr)]
rs
        if ([[Name]] -> Bool
forall a. Eq a => [a] -> Bool
hasDuplicate [[Name]]
fields) then (Expr -> ScopeCheck Expr
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorDuplicateField Expr
e) else do
          rs <- (([Name], Expr) -> ScopeCheck (Name, Expr))
-> [([Name], Expr)] -> ScopeCheck [(Name, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Name], Expr) -> ScopeCheck (Name, Expr)
scopeCheckRecordLine [([Name], Expr)]
rs
          return $ A.Record A.AnonRec rs

      C.Proj Name
n -> PrePost -> Name -> Expr
A.Proj PrePost
Post (Name -> Expr) -> ScopeCheck Name -> ScopeCheck Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> ScopeCheck Name
scopeCheckProj Name
n

      C.Ident n :: QName
n@C.Qual{} -> QName -> ScopeCheck Expr
scopeCheckGlobalVar QName
n

      C.Ident n :: QName
n@C.QName{} -> do
        res <- Name -> ScopeCheck (Maybe Name)
lookupLocal (QName -> Name
C.name QName
n)
        case res of
          Just Name
x -> Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeCheck Expr) -> Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
x
          Maybe Name
Nothing -> QName -> ScopeCheck Expr
scopeCheckGlobalVar QName
n

      Expr
_ -> String -> ScopeCheck Expr
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> ScopeCheck Expr) -> String -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ String
"NYI: scopeCheckExpr " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e

scopeCheckGlobalVar :: C.QName -> ScopeCheck A.Expr
scopeCheckGlobalVar :: QName -> ScopeCheck Expr
scopeCheckGlobalVar QName
n = do
  res <- QName -> ScopeCheck (Maybe DefI)
lookupGlobal QName
n
  case res of
    Just (DefI IKind
k QName
x) -> case IKind
k of
      (ConK ConK
co)  -> Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeCheck Expr) -> Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ ConK -> QName -> Expr
A.con ConK
co QName
x
      IKind
LetK       -> Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeCheck Expr) -> Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.letdef (QName -> Name
A.unqual QName
x)
      -- references to recursive functions are coded differently
      -- outside the mutual block
      FunK Bool
True  -> Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeCheck Expr) -> Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.fun QName
x -- A.letdef x -- A.mkExtRef x
      FunK Bool
False -> Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeCheck Expr) -> Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.fun QName
x
      IKind
DataK      -> Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeCheck Expr) -> Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.dat QName
x
      IKind
ProjK      -> Expr -> ScopeCheck Expr
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ScopeCheck Expr) -> Expr -> ScopeCheck Expr
forall a b. (a -> b) -> a -> b
$ PrePost -> Name -> Expr
A.Proj PrePost
A.Pre (QName -> Name
A.unqual QName
x) -- errorProjectionUsedAsExpression n
    Maybe DefI
Nothing -> QName -> ScopeCheck Expr
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorIdentifierUndefined QName
n

scopeCheckLocalVar :: C.Name -> ScopeCheck A.Name
scopeCheckLocalVar :: Name -> ScopeCheck Name
scopeCheckLocalVar Name
n = ScopeCheck Name
-> (Name -> ScopeCheck Name) -> Maybe Name -> ScopeCheck Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Name -> ScopeCheck Name
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorIdentifierUndefined Name
n) Name -> ScopeCheck Name
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Name -> ScopeCheck Name)
-> ScopeCheck (Maybe Name) -> ScopeCheck Name
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  Name -> ScopeCheck (Maybe Name)
lookupLocal Name
n

scopeCheckRecordLine :: ([C.Name], C.Expr) -> ScopeCheck (A.Name, A.Expr)
scopeCheckRecordLine :: ([Name], Expr) -> ScopeCheck (Name, Expr)
scopeCheckRecordLine (Name
n : [Name]
ns, Expr
e) = do
  x <- Name -> ScopeCheck Name
scopeCheckProj Name
n
  (x,) <$> scopeCheckExprN (foldr C.Lam e ns)

scopeCheckProj :: C.Name -> ScopeCheck A.Name
scopeCheckProj :: Name -> ScopeCheck Name
scopeCheckProj Name
n = do
  sig <- ScopeCheck Sig
getSig
  case lookupSigU n sig of
    Just (DefI IKind
ProjK QName
x) -> Name -> ScopeCheck Name
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> ScopeCheck Name) -> Name -> ScopeCheck Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
A.unqual QName
x
    Maybe DefI
_                   -> Name -> ScopeCheck Name
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorNotAField Name
n


-- | @isProjIdent n = n@ if defined and the name of a projection.
isProjIdent :: C.QName -> ScopeCheck (Maybe A.Name)
isProjIdent :: QName -> ScopeCheck (Maybe Name)
isProjIdent QName
n = do
  sig <- ScopeCheck Sig
getSig
  return $
    case lookupSig n sig of
      Just (DefI IKind
ProjK QName
x) -> Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Maybe Name) -> Name -> Maybe Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
A.unqual QName
x
      Maybe DefI
_ -> Maybe Name
forall a. Maybe a
Nothing

isProjection :: C.Expr -> ScopeCheck (Maybe A.Name)
isProjection :: Expr -> ScopeCheck (Maybe Name)
isProjection (C.Ident QName
n) = QName -> ScopeCheck (Maybe Name)
isProjIdent QName
n
isProjection Expr
_           = Maybe Name -> ScopeCheck (Maybe Name)
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Name
forall a. Maybe a
Nothing

scopeCheckMeasure :: A.Measure C.Expr -> ScopeCheck (A.Measure A.Expr)
scopeCheckMeasure :: Measure Expr -> ScopeCheck (Measure Expr)
scopeCheckMeasure (A.Measure [Expr]
es) = do
  es' <- (Expr -> ScopeCheck Expr) -> [Expr] -> ScopeCheck [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Expr -> ScopeCheck Expr
scopeCheckExprN [Expr]
es
  return $ A.Measure es'

scopeCheckBound :: A.Bound C.Expr -> ScopeCheck (A.Bound A.Expr)
scopeCheckBound :: Bound Expr -> ScopeCheck (Bound Expr)
scopeCheckBound (A.Bound LtLe
ltle Measure Expr
e1 Measure Expr
e2) = do
  e1' <- Measure Expr -> ScopeCheck (Measure Expr)
scopeCheckMeasure Measure Expr
e1
  e2' <- scopeCheckMeasure e2
  return $ A.Bound ltle e1' e2'

checkPatternLength :: [C.Clause] -> Maybe Int
checkPatternLength :: [Clause] -> Maybe Int
checkPatternLength [] = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0 -- arity 0
checkPatternLength (C.Clause Maybe Name
_ [Pattern]
pl Maybe Expr
_:[Clause]
cl) = Int -> [Clause] -> Maybe Int
cpl ([Pattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern]
pl) [Clause]
cl
 where
   cpl :: Int -> [Clause] -> Maybe Int
cpl Int
k [] = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
k
   cpl Int
k (C.Clause Maybe Name
_ [Pattern]
pl Maybe Expr
_ : [Clause]
cl) = if ([Pattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern]
pl Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k) then (Int -> [Clause] -> Maybe Int
cpl Int
k [Clause]
cl) else Maybe Int
forall a. Maybe a
Nothing

scopeCheckClause :: Maybe C.Name -> C.Clause -> ScopeCheck A.Clause
scopeCheckClause :: Maybe Name -> Clause -> ScopeCheck Clause
scopeCheckClause Maybe Name
mname' (C.Clause Maybe Name
mname [Pattern]
pl Maybe Expr
mrhs) = do
  Bool -> ScopeCheck () -> ScopeCheck ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe Name
mname Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Name
mname') (ScopeCheck () -> ScopeCheck ()) -> ScopeCheck () -> ScopeCheck ()
forall a b. (a -> b) -> a -> b
$ Maybe Name -> Maybe Name -> ScopeCheck ()
forall {m :: * -> *} {a} {a} {a}.
(MonadError TraceError m, Show a, Show a) =>
Maybe a -> Maybe a -> m a
errorClauseIdentifier Maybe Name
mname Maybe Name
mname'
  (pl, delta) <- StateT PatCtx ScopeCheck [Pat Expr]
-> PatCtx -> ScopeCheck ([Pat Expr], PatCtx)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ((Pattern -> StateT PatCtx ScopeCheck (Pat Expr))
-> [Pattern] -> StateT PatCtx ScopeCheck [Pat Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Pattern -> StateT PatCtx ScopeCheck (Pat Expr)
scopeCheckPattern [Pattern]
pl) PatCtx
emptyCtx
  local (addContext delta) $ do
    pl <- mapM scopeCheckDotPattern pl
    case mrhs of
      Maybe Expr
Nothing  -> Clause -> ScopeCheck Clause
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> ScopeCheck Clause) -> Clause -> ScopeCheck Clause
forall a b. (a -> b) -> a -> b
$ [Pattern] -> Maybe Expr -> Clause
A.clause [Pattern]
pl Maybe Expr
forall a. Maybe a
Nothing
      Just Expr
rhs -> [Pattern] -> Maybe Expr -> Clause
A.clause [Pattern]
pl (Maybe Expr -> Clause) -> (Expr -> Maybe Expr) -> Expr -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Clause) -> ScopeCheck Expr -> ScopeCheck Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
rhs


type PatCtx = Context
type SPS = StateT PatCtx ScopeCheck

scopeCheckPatVar :: C.QName -> SPS (A.Pat C.Expr)
scopeCheckPatVar :: QName -> StateT PatCtx ScopeCheck (Pat Expr)
scopeCheckPatVar QName
n = do
      sig <- ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig
forall (m :: * -> *) a. Monad m => m a -> StateT PatCtx m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig)
-> ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig
forall a b. (a -> b) -> a -> b
$ ScopeCheck Sig
getSig
      case lookupSig n sig of
        Just (DefI (ConK ConK
co) QName
n) -> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr))
-> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a b. (a -> b) -> a -> b
$ PatternInfo -> QName -> [Pat Expr] -> Pat Expr
forall e. PatternInfo -> QName -> [Pat e] -> Pat e
A.ConP (ConK -> Bool -> Bool -> PatternInfo
A.PatternInfo ConK
co Bool
False Bool
False) QName
n []
                             -- a nullary constructor
        Just DefI
_  -> QName -> StateT PatCtx ScopeCheck (Pat Expr)
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorPatternNotConstructor QName
n
        Maybe DefI
Nothing -> Name -> Pat Expr
forall e. Name -> Pat e
A.VarP (Name -> Pat Expr)
-> StateT PatCtx ScopeCheck Name
-> StateT PatCtx ScopeCheck (Pat Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> StateT PatCtx ScopeCheck Name
addUnique (QName -> Name
C.unqual QName
n)

scopeCheckPattern :: C.Pattern -> SPS (A.Pat C.Expr)
scopeCheckPattern :: Pattern -> StateT PatCtx ScopeCheck (Pat Expr)
scopeCheckPattern Pattern
p =
  case Pattern
p of

    -- case n
    C.IdentP QName
n        -> QName -> StateT PatCtx ScopeCheck (Pat Expr)
scopeCheckPatVar QName
n
    C.ConP Bool
False QName
n [] -> QName -> StateT PatCtx ScopeCheck (Pat Expr)
scopeCheckPatVar QName
n

    -- case (i > j):
    C.SizeP Expr
m Name
n -> do
      -- m   <- lift $ scopeCheckLocalVar m
      Expr -> Name -> Pat Expr
forall e. e -> Name -> Pat e
A.SizeP Expr
m (Name -> Pat Expr)
-> StateT PatCtx ScopeCheck Name
-> StateT PatCtx ScopeCheck (Pat Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> StateT PatCtx ScopeCheck Name
addUnique Name
n

    -- case $p
    C.SuccP Pattern
p2    -> Pat Expr -> Pat Expr
forall e. Pat e -> Pat e
A.SuccP (Pat Expr -> Pat Expr)
-> StateT PatCtx ScopeCheck (Pat Expr)
-> StateT PatCtx ScopeCheck (Pat Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> StateT PatCtx ScopeCheck (Pat Expr)
scopeCheckPattern Pattern
p2

    -- case (p1,p2)
    C.PairP Pattern
p1 Pattern
p2 -> Pat Expr -> Pat Expr -> Pat Expr
forall e. Pat e -> Pat e -> Pat e
A.PairP (Pat Expr -> Pat Expr -> Pat Expr)
-> StateT PatCtx ScopeCheck (Pat Expr)
-> StateT PatCtx ScopeCheck (Pat Expr -> Pat Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> StateT PatCtx ScopeCheck (Pat Expr)
scopeCheckPattern Pattern
p1 StateT PatCtx ScopeCheck (Pat Expr -> Pat Expr)
-> StateT PatCtx ScopeCheck (Pat Expr)
-> StateT PatCtx ScopeCheck (Pat Expr)
forall a b.
StateT PatCtx ScopeCheck (a -> b)
-> StateT PatCtx ScopeCheck a -> StateT PatCtx ScopeCheck b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pattern -> StateT PatCtx ScopeCheck (Pat Expr)
scopeCheckPattern Pattern
p2

    -- case .n
    C.ConP Bool
True QName
n [] -> do
      -- try projection
      StateT PatCtx ScopeCheck (Maybe Name)
-> (Name -> StateT PatCtx ScopeCheck (Pat Expr))
-> StateT PatCtx ScopeCheck (Pat Expr)
-> StateT PatCtx ScopeCheck (Pat Expr)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> (a -> m b) -> m b -> m b
ifJustM (ScopeCheck (Maybe Name) -> StateT PatCtx ScopeCheck (Maybe Name)
forall (m :: * -> *) a. Monad m => m a -> StateT PatCtx m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeCheck (Maybe Name) -> StateT PatCtx ScopeCheck (Maybe Name))
-> ScopeCheck (Maybe Name) -> StateT PatCtx ScopeCheck (Maybe Name)
forall a b. (a -> b) -> a -> b
$ QName -> ScopeCheck (Maybe Name)
isProjIdent QName
n) (Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr))
-> (Name -> Pat Expr)
-> Name
-> StateT PatCtx ScopeCheck (Pat Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Pat Expr
forall e. Name -> Pat e
A.ProjP) (StateT PatCtx ScopeCheck (Pat Expr)
 -> StateT PatCtx ScopeCheck (Pat Expr))
-> StateT PatCtx ScopeCheck (Pat Expr)
-> StateT PatCtx ScopeCheck (Pat Expr)
forall a b. (a -> b) -> a -> b
$ do
      -- try constructor
      sig <- ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig
forall (m :: * -> *) a. Monad m => m a -> StateT PatCtx m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig)
-> ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig
forall a b. (a -> b) -> a -> b
$ ScopeCheck Sig
getSig
      case lookupSig n sig of
        Just (DefI (ConK ConK
co) QName
n) ->
              Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr))
-> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a b. (a -> b) -> a -> b
$ PatternInfo -> QName -> [Pat Expr] -> Pat Expr
forall e. PatternInfo -> QName -> [Pat e] -> Pat e
A.ConP (ConK -> Bool -> Bool -> PatternInfo
A.PatternInfo ConK
co Bool
False Bool
True) QName
n []
      -- fallback: dot pattern
        Maybe DefI
_  -> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr))
-> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Pat Expr
forall e. e -> Pat e
A.DotP (QName -> Expr
C.Ident QName
n)

    -- case [.]c ps
    C.ConP Bool
dotted QName
n [Pattern]
pl -> do
      sig <- ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig
forall (m :: * -> *) a. Monad m => m a -> StateT PatCtx m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig)
-> ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig
forall a b. (a -> b) -> a -> b
$ ScopeCheck Sig
getSig
      case lookupSig n sig of
        Just (DefI (ConK ConK
co) QName
x) ->
          PatternInfo -> QName -> [Pat Expr] -> Pat Expr
forall e. PatternInfo -> QName -> [Pat e] -> Pat e
A.ConP (ConK -> Bool -> Bool -> PatternInfo
A.PatternInfo ConK
co Bool
False Bool
dotted) QName
x ([Pat Expr] -> Pat Expr)
-> StateT PatCtx ScopeCheck [Pat Expr]
-> StateT PatCtx ScopeCheck (Pat Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern -> StateT PatCtx ScopeCheck (Pat Expr))
-> [Pattern] -> StateT PatCtx ScopeCheck [Pat Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Pattern -> StateT PatCtx ScopeCheck (Pat Expr)
scopeCheckPattern [Pattern]
pl
        Maybe DefI
_  -> QName -> StateT PatCtx ScopeCheck (Pat Expr)
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorPatternNotConstructor QName
n

    -- case .e
    C.DotP Expr
e  -> do
      isProj <- ScopeCheck (Maybe Name) -> StateT PatCtx ScopeCheck (Maybe Name)
forall (m :: * -> *) a. Monad m => m a -> StateT PatCtx m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeCheck (Maybe Name) -> StateT PatCtx ScopeCheck (Maybe Name))
-> ScopeCheck (Maybe Name) -> StateT PatCtx ScopeCheck (Maybe Name)
forall a b. (a -> b) -> a -> b
$ Expr -> ScopeCheck (Maybe Name)
isProjection Expr
e
      case isProj of
       Just Name
n  -> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr))
-> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a b. (a -> b) -> a -> b
$ Name -> Pat Expr
forall e. Name -> Pat e
A.ProjP Name
n
       Maybe Name
Nothing -> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr))
-> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Pat Expr
forall e. e -> Pat e
A.DotP Expr
e -- dot patterns checked later

    -- case ()
    Pattern
C.AbsurdP -> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr))
-> Pat Expr -> StateT PatCtx ScopeCheck (Pat Expr)
forall a b. (a -> b) -> a -> b
$ Pat Expr
forall e. Pat e
A.AbsurdP

-- | Add pattern variable to pattern context, must not be present yet.
addUnique :: C.Name -> SPS A.Name
addUnique :: Name -> StateT PatCtx ScopeCheck Name
addUnique = Bool -> Name -> StateT PatCtx ScopeCheck Name
addPatVar Bool
True

addNonUnique :: C.Name -> SPS A.Name
addNonUnique :: Name -> StateT PatCtx ScopeCheck Name
addNonUnique = Bool -> Name -> StateT PatCtx ScopeCheck Name
addPatVar Bool
False

addPatVar :: Bool -> C.Name -> SPS A.Name
addPatVar :: Bool -> Name -> StateT PatCtx ScopeCheck Name
addPatVar Bool
linear Name
n = do
  delta <- StateT PatCtx ScopeCheck PatCtx
forall s (m :: * -> *). MonadState s m => m s
get
  case retrieve n delta of
    Just Name
x -> if Bool
linear then Name -> StateT PatCtx ScopeCheck Name
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorPatternNotLinear Name
n else Name -> StateT PatCtx ScopeCheck Name
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
    Maybe Name
Nothing -> do
      let (Name
x, PatCtx
delta') = Name -> PatCtx -> (Name, PatCtx)
forall b. Push Local b => Name -> b -> (Name, b)
newLocal Name
n PatCtx
delta
      PatCtx -> StateT PatCtx ScopeCheck ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put PatCtx
delta'
      Name -> StateT PatCtx ScopeCheck Name
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x

scopeCheckDotPattern :: A.Pat C.Expr -> ScopeCheck A.Pattern
scopeCheckDotPattern :: Pat Expr -> ScopeCheck Pattern
scopeCheckDotPattern Pat Expr
p =
    case Pat Expr
p of
      A.DotP Expr
e -> Expr -> Pattern
forall e. e -> Pat e
A.DotP (Expr -> Pattern) -> ScopeCheck Expr -> ScopeCheck Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e
      A.PairP Pat Expr
p1 Pat Expr
p2 -> Pattern -> Pattern -> Pattern
forall e. Pat e -> Pat e -> Pat e
A.PairP (Pattern -> Pattern -> Pattern)
-> ScopeCheck Pattern -> ScopeCheck (Pattern -> Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pat Expr -> ScopeCheck Pattern
scopeCheckDotPattern Pat Expr
p1 ScopeCheck (Pattern -> Pattern)
-> ScopeCheck Pattern -> ScopeCheck Pattern
forall a b. ScopeCheck (a -> b) -> ScopeCheck a -> ScopeCheck b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>  Pat Expr -> ScopeCheck Pattern
scopeCheckDotPattern Pat Expr
p2
      A.SuccP Pat Expr
p -> Pattern -> Pattern
forall e. Pat e -> Pat e
A.SuccP (Pattern -> Pattern) -> ScopeCheck Pattern -> ScopeCheck Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pat Expr -> ScopeCheck Pattern
scopeCheckDotPattern Pat Expr
p
      A.ConP PatternInfo
co QName
n [Pat Expr]
pl -> PatternInfo -> QName -> [Pattern] -> Pattern
forall e. PatternInfo -> QName -> [Pat e] -> Pat e
A.ConP PatternInfo
co QName
n ([Pattern] -> Pattern)
-> ScopeCheck [Pattern] -> ScopeCheck Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pat Expr -> ScopeCheck Pattern)
-> [Pat Expr] -> ScopeCheck [Pattern]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Pat Expr -> ScopeCheck Pattern
scopeCheckDotPattern [Pat Expr]
pl
--      A.SizeP m n -> flip A.SizeP n <$> scopeCheckLocalVar m -- return $ A.SizeP m n
      A.SizeP Expr
e Name
n    -> (Expr -> Name -> Pattern) -> Name -> Expr -> Pattern
forall a b c. (a -> b -> c) -> b -> a -> c
flip Expr -> Name -> Pattern
forall e. e -> Name -> Pat e
A.SizeP Name
n (Expr -> Pattern) -> ScopeCheck Expr -> ScopeCheck Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ScopeCheck Expr
scopeCheckExprN Expr
e
      A.VarP Name
n       -> Pattern -> ScopeCheck Pattern
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> ScopeCheck Pattern) -> Pattern -> ScopeCheck Pattern
forall a b. (a -> b) -> a -> b
$ Name -> Pattern
forall e. Name -> Pat e
A.VarP Name
n  -- even though p = A.VarP n, it has wrong type!!
      A.ProjP Name
n      -> Pattern -> ScopeCheck Pattern
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> ScopeCheck Pattern) -> Pattern -> ScopeCheck Pattern
forall a b. (a -> b) -> a -> b
$ Name -> Pattern
forall e. Name -> Pat e
A.ProjP Name
n
      Pat Expr
A.AbsurdP      -> Pattern -> ScopeCheck Pattern
forall a. a -> ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> ScopeCheck Pattern) -> Pattern -> ScopeCheck Pattern
forall a b. (a -> b) -> a -> b
$ Pattern
forall e. Pat e
A.AbsurdP
      -- impossible cases: ErasedP, UnusableP


-- * Scope checking parameters

parameterVariables :: [C.Expr] -> ScopeCheck Context
parameterVariables :: [Expr] -> ScopeCheck PatCtx
parameterVariables [Expr]
es = do
  StateT PatCtx ScopeCheck () -> PatCtx -> ScopeCheck PatCtx
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT ((Expr -> StateT PatCtx ScopeCheck ())
-> [Expr] -> StateT PatCtx ScopeCheck ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Expr -> StateT PatCtx ScopeCheck ()
scopeCheckParameter [Expr]
es) PatCtx
emptyCtx

-- | Extract variables bound by data parameters.
--   We consider a more liberal set of patterns, everything
--   that is injective and does not bind variables.
scopeCheckParameter :: C.Expr -> SPS ()
scopeCheckParameter :: Expr -> StateT PatCtx ScopeCheck ()
scopeCheckParameter Expr
e =
  case Expr
e of
    C.Set Expr
e'             -> Expr -> StateT PatCtx ScopeCheck ()
scopeCheckParameter Expr
e'
    C.CoSet Expr
e'           -> Expr -> StateT PatCtx ScopeCheck ()
scopeCheckParameter Expr
e'
    Expr
C.Size               -> () -> StateT PatCtx ScopeCheck ()
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    C.Succ Expr
e'            -> Expr -> StateT PatCtx ScopeCheck ()
scopeCheckParameter Expr
e'
    Expr
C.Zero               -> () -> StateT PatCtx ScopeCheck ()
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Expr
C.Infty              -> () -> StateT PatCtx ScopeCheck ()
forall a. a -> StateT PatCtx ScopeCheck a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    C.Pair Expr
e1 Expr
e2         -> Expr -> StateT PatCtx ScopeCheck ()
scopeCheckParameter Expr
e1 StateT PatCtx ScopeCheck ()
-> StateT PatCtx ScopeCheck () -> StateT PatCtx ScopeCheck ()
forall a b.
StateT PatCtx ScopeCheck a
-> StateT PatCtx ScopeCheck b -> StateT PatCtx ScopeCheck b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> StateT PatCtx ScopeCheck ()
scopeCheckParameter Expr
e2
    C.Record [([Name], Expr)]
fs          -> (([Name], Expr) -> StateT PatCtx ScopeCheck ())
-> [([Name], Expr)] -> StateT PatCtx ScopeCheck ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Expr -> ([Name], Expr) -> StateT PatCtx ScopeCheck ()
scpField Expr
e) [([Name], Expr)]
fs
    C.Ident QName
n            -> Expr -> QName -> [Expr] -> StateT PatCtx ScopeCheck ()
scpApp Expr
e QName
n []
    C.App (C.Ident QName
n) [Expr]
es -> Expr -> QName -> [Expr] -> StateT PatCtx ScopeCheck ()
scpApp Expr
e QName
n [Expr]
es
    C.App C.App{} [Expr]
es     -> String -> StateT PatCtx ScopeCheck ()
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> StateT PatCtx ScopeCheck ())
-> String -> StateT PatCtx ScopeCheck ()
forall a b. (a -> b) -> a -> b
$ String
"scopeCheckParameter " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": internal invariant violated"
    Expr
_ -> Expr -> StateT PatCtx ScopeCheck ()
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorInvalidParameter Expr
e
  where
    -- we can only treat a record expression as pattern
    -- if it does not bind any variables
    scpField :: C.Expr -> ([C.Name], C.Expr) -> SPS ()
    scpField :: Expr -> ([Name], Expr) -> StateT PatCtx ScopeCheck ()
scpField Expr
e ([Name
f], Expr
e') = Expr -> StateT PatCtx ScopeCheck ()
scopeCheckParameter Expr
e'
    scpField Expr
e ([Name], Expr)
_         = Expr -> StateT PatCtx ScopeCheck ()
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorInvalidParameter Expr
e

    scpApp :: C.Expr -> C.QName -> [C.Expr] -> SPS ()
    scpApp :: Expr -> QName -> [Expr] -> StateT PatCtx ScopeCheck ()
scpApp Expr
e QName
n [Expr]
es = do
      sig <- ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig
forall (m :: * -> *) a. Monad m => m a -> StateT PatCtx m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig)
-> ScopeCheck Sig -> StateT PatCtx ScopeCheck Sig
forall a b. (a -> b) -> a -> b
$ ScopeCheck Sig
getSig
      case lookupSig n sig of
        Just (DefI ConK{} QName
n) -> (Expr -> StateT PatCtx ScopeCheck ())
-> [Expr] -> StateT PatCtx ScopeCheck ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Expr -> StateT PatCtx ScopeCheck ()
scopeCheckParameter [Expr]
es
        Just (DefI IKind
DataK  QName
n) -> (Expr -> StateT PatCtx ScopeCheck ())
-> [Expr] -> StateT PatCtx ScopeCheck ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Expr -> StateT PatCtx ScopeCheck ()
scopeCheckParameter [Expr]
es
        Just DefI
_  -> Expr -> StateT PatCtx ScopeCheck ()
forall {m :: * -> *} {a} {a}.
(MonadError TraceError m, Show a) =>
a -> m a
errorInvalidParameter Expr
e
        Maybe DefI
Nothing -> StateT PatCtx ScopeCheck Name -> StateT PatCtx ScopeCheck ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (StateT PatCtx ScopeCheck Name -> StateT PatCtx ScopeCheck ())
-> StateT PatCtx ScopeCheck Name -> StateT PatCtx ScopeCheck ()
forall a b. (a -> b) -> a -> b
$ Name -> StateT PatCtx ScopeCheck Name
addNonUnique (QName -> Name
C.unqual QName
n) -- allow non-linearity

-- * Scope checking errors

errorAlreadyInSignature :: a -> a -> m a
errorAlreadyInSignature a
s a
n = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
s  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Identifier " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" already in signature"

errorAlreadyInContext :: a -> a -> m a
errorAlreadyInContext a
s a
n = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Identifier " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" already in context"

-- errorPatternNotVariable n = throwErrorMsg $ "pattern " ++ n ++ ": Identifier expected"

errorPatternNotConstructor :: a -> m a
errorPatternNotConstructor a
n = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"pattern " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a constructor"

errorNotAField :: a -> m a
errorNotAField a
n = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"record field " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" unknown"
-- errorUnknownProjection n = throwErrorMsg $ "projection " ++ n ++ " unknown"

errorDuplicateField :: a -> m a
errorDuplicateField a
r = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" assigns a field twice"


errorProjectionUsedAsExpression :: a -> m a
errorProjectionUsedAsExpression a
n = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"projection " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" used as expression"

errorIdentifierUndefined :: a -> m a
errorIdentifierUndefined a
n = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"Identifier " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" undefined"

errorPatternNotLinear :: a -> m a
errorPatternNotLinear a
n = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"pattern not linear: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n

errorClauseIdentifier :: Maybe a -> Maybe a -> m a
errorClauseIdentifier (Just a
n) (Just a
n') = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"Expected identifier " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" as clause head, found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n

errorOnlyOneMeasure :: m a
errorOnlyOneMeasure = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg String
"only one measure allowed in a function type"

errorConstraintNotAllowed :: a -> m a
errorConstraintNotAllowed a
beta = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$
  a -> String
forall a. Show a => a -> String
show a
beta String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": constraints must follow a quantifier"

errorTargetMustBeAppliedName :: a -> a -> m a
errorTargetMustBeAppliedName a
n a
t = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$
  String
"constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": target must be data/record type applied to parameters and indices; however, I found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
t

errorWrongTarget :: a -> a -> a -> m a
errorWrongTarget a
c a
d a
d' = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$
  String
"constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" should target data/record type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"; however, I found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
d'

errorNotEnoughParameters :: a -> a -> m a
errorNotEnoughParameters a
c a
t = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$
  String
"constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": target " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is missing parameters"

errorInvalidParameter :: a -> m a
errorInvalidParameter a
e = String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$
  String
"expression " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not valid in a parameter"