{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}

module TypeChecker where

import Control.Applicative
import Control.Monad
import Control.Monad.Except
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State

import Data.Functor
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set

import Debug.Trace

import qualified Sit.Abs as A
import Sit.Print

import Abstract as A
import Internal
import Substitute
import Evaluation

import Lens
import Impossible
#include "undefined.h"

-- | Type errors are just strings.
type TypeError = String

-- | Local context

type Cxt = [ (Id, Dom VType) ]

data TCEnv = TCEnv
  { TCEnv -> Cxt
_envCxt :: Cxt  -- ^ Typing context.
  , TCEnv -> Env
_envEnv :: Env  -- ^ Default environment.
  }

makeLens ''TCEnv

-- | Global state

data TCSt = TCSt
  { TCSt -> Map Id VType
_stTySigs :: Map Id VType
  , TCSt -> Map Id VType
_stDefs   :: Map Id Val
  }

makeLens ''TCSt

-- | The type checking monad
type Check = ReaderT TCEnv (StateT TCSt (Except TypeError))

-- * Type checker

typeCheck :: [A.Decl] -> Either String ()
typeCheck :: [Decl] -> Either Id ()
typeCheck [Decl]
decls = Except Id () -> Either Id ()
forall e a. Except e a -> Either e a
runExcept (StateT TCSt (Except Id) () -> TCSt -> Except Id ()
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> TCEnv -> StateT TCSt (Except Id) ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ([Decl] -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
checkDecls [Decl]
decls) TCEnv
initEnv) TCSt
initSt)
  where
  initEnv :: TCEnv
initEnv = TCEnv :: Cxt -> Env -> TCEnv
TCEnv { _envCxt :: Cxt
_envCxt   = []        , _envEnv :: Env
_envEnv = []        }
  initSt :: TCSt
initSt  = TCSt :: Map Id VType -> Map Id VType -> TCSt
TCSt  { _stTySigs :: Map Id VType
_stTySigs = Map Id VType
forall k a. Map k a
Map.empty , _stDefs :: Map Id VType
_stDefs = Map Id VType
forall k a. Map k a
Map.empty }

checkDecls :: [A.Decl] -> Check ()
checkDecls :: [Decl] -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
checkDecls = (Decl -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> [Decl] -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Decl -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
checkDecl

checkDecl :: A.Decl -> Check ()
checkDecl :: Decl -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
checkDecl = \case
  A.Blank{} -> () -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  A.Open{}  -> () -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  A.Sig Ident
x Exp
a -> Ident -> Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
checkSig Ident
x Exp
a
  A.Def Ident
x Exp
e -> Ident -> Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
checkDef Ident
x Exp
e

-- | Check a type signature.

checkSig :: A.Ident -> A.Exp -> Check ()
checkSig :: Ident -> Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
checkSig x0 :: Ident
x0@(A.Ident Id
x) Exp
a = Decl
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. Print a => a -> b -> b
traceCheck (Ident -> Exp -> Decl
A.Sig Ident
x0 Exp
a) (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ do

  -- Check that x is not already defined
  Maybe VType
mt <- Id -> Check (Maybe VType)
lookupTySig Id
x
  Bool
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Maybe VType -> Bool
forall a. Maybe a -> Bool
isNothing Maybe VType
mt) (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$
    Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ Id
"Duplicate type signature for " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
x

  -- Check type and add to signature
  Type
t <- Exp -> Check Type
checkType Exp
a
  -- traceM $ "Adding  " ++ show x ++ "  of type  " ++ show t
  Id -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
addTySig Id
x (VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
t

-- | Check a definition.

checkDef :: A.Ident -> A.Exp -> Check ()
checkDef :: Ident -> Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
checkDef x0 :: Ident
x0@(A.Ident Id
x) Exp
e = Decl
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. Print a => a -> b -> b
traceCheck (Ident -> Exp -> Decl
A.Def Ident
x0 Exp
e) (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ do

  -- Check that x has a signature
  let noSig :: ReaderT TCEnv (StateT TCSt (Except Id)) a
noSig = Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a)
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a
forall a b. (a -> b) -> a -> b
$ Id
"Missing type signature for " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
x
  VType
t <- ReaderT TCEnv (StateT TCSt (Except Id)) VType
-> (VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType)
-> Maybe VType
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall a. ReaderT TCEnv (StateT TCSt (Except Id)) a
noSig VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType)
-> Check (Maybe VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Id -> Check (Maybe VType)
lookupTySig Id
x

  -- Check that x has not yet a definition
  Maybe VType
mv <- Id -> Check (Maybe VType)
lookupDef Id
x
  Bool
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Maybe VType -> Bool
forall a. Maybe a -> Bool
isNothing Maybe VType
mv) (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$
    Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ Id
"Duplicate definition of " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
x

  -- Check definition and add to signature
  Type
v <- Exp -> VType -> Check Type
checkExp Exp
e VType
t
  -- traceM $ "Adding  " ++ show x ++ "  of value  " ++ show v
  Id -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
addDef Id
x (VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
v

-- | Check well-formedness of a type.

checkType :: A.Exp -> Check Type
checkType :: Exp -> Check Type
checkType Exp
e = (Type, VType) -> Type
forall a b. (a, b) -> a
fst ((Type, VType) -> Type)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> Check Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferType Exp
e

-- | Check that something is a type and infer its universe level.

inferType :: A.Exp -> Check (Type, VLevel)
inferType :: Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferType Exp
e = do
  let invalidType :: ReaderT TCEnv (StateT TCSt (Except Id)) a
invalidType = Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a)
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a
forall a b. (a -> b) -> a -> b
$ Id
"Not a valid type expression: " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Exp -> Id
forall a. Print a => a -> Id
printTree Exp
e
  case Exp
e of

    -- Size type (internal use only).

    -- Each universe is closed under size quantification.
    -- Thus, we place Size in Set0.

    Exp
A.Size -> (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
Size, Int -> VType
vsConst Int
0)

    -- Universes (shape irrelevant)

    Exp
A.Set  -> (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
Type Type
sZero, Int -> VType
vsConst Int
1)
    Exp
A.Set1 -> (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
Type (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
sSuc Type
sZero, Int -> VType
vsConst Int
2)
    Exp
A.Set2 -> (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
Type (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
sSuc (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
sSuc Type
sZero, Int -> VType
vsConst Int
3)
    A.App Exp
A.Set Exp
l -> do
      Type
a <- Relevance -> Check Type -> Check Type
forall a. Relevance -> Check a -> Check a
resurrect Relevance
ShapeIrr (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Exp -> Check Type
checkLevel Exp
l
      VType
v <- Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
a
      (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
Type Type
a, VType -> VType
vsSuc VType
v)

    -- Natural number type (shape irrelevant)

    A.App Exp
A.Nat Exp
s -> do
      Type
a <- Relevance -> Check Type -> Check Type
forall a. Relevance -> Check a -> Check a
resurrect Relevance
ShapeIrr (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Exp -> Check Type
checkSize Exp
s
      VType
v <- Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
a
      (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
Nat Type
a, VType
vsZero)

    -- Function types

    A.Arrow Exp
a Exp
b -> do
      (Type
u, VType
l1) <- Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferType Exp
a
      (Type
t, VType
l2) <- Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferType Exp
b
      (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type -> Abs Type -> Type
Pi (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
u) (Id -> Type -> Abs Type
forall a. Id -> a -> Abs a
NoAbs Id
"_" Type
t) , VType -> VType -> VType
maxSize VType
l1 VType
l2)

    A.Pi Exp
e Exp
a Exp
b -> do
      let failure :: ReaderT TCEnv (StateT TCSt (Except Id)) a
failure = Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a)
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a
forall a b. (a -> b) -> a -> b
$ Id
"Expected list of identifiers, found " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Exp -> Id
forall a. Print a => a -> Id
printTree Exp
e
      [IdU]
xs <- ReaderT TCEnv (StateT TCSt (Except Id)) [IdU]
-> ([IdU] -> ReaderT TCEnv (StateT TCSt (Except Id)) [IdU])
-> Maybe [IdU]
-> ReaderT TCEnv (StateT TCSt (Except Id)) [IdU]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReaderT TCEnv (StateT TCSt (Except Id)) [IdU]
forall a. ReaderT TCEnv (StateT TCSt (Except Id)) a
failure [IdU] -> ReaderT TCEnv (StateT TCSt (Except Id)) [IdU]
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [IdU] -> ReaderT TCEnv (StateT TCSt (Except Id)) [IdU])
-> Maybe [IdU] -> ReaderT TCEnv (StateT TCSt (Except Id)) [IdU]
forall a b. (a -> b) -> a -> b
$ Exp -> Maybe [IdU]
parseIdUs Exp
e
      [(IdU, Dom Exp)]
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferPisType ((IdU -> (IdU, Dom Exp)) -> [IdU] -> [(IdU, Dom Exp)]
forall a b. (a -> b) -> [a] -> [b]
map (, Exp -> Dom Exp
forall a. a -> Dom a
defaultDom Exp
a) [IdU]
xs) (ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferType Exp
b

    A.Forall [Bind]
bs Exp
c -> [(IdU, Dom Exp)]
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferPisType (Bind -> [(IdU, Dom Exp)]
fromBind (Bind -> [(IdU, Dom Exp)]) -> [Bind] -> [(IdU, Dom Exp)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Bind]
bs) (ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferType Exp
c
      where
      fromBind :: A.Bind -> [(A.IdU, Dom A.Exp)]
      fromBind :: Bind -> [(IdU, Dom Exp)]
fromBind = \case
        A.BIrrel Ident
x  -> (IdU, Dom Exp) -> [(IdU, Dom Exp)]
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> IdU
A.Id Ident
x, Relevance -> Exp -> Dom Exp
forall a. Relevance -> a -> Dom a
Dom Relevance
Irrelevant Exp
A.Size)
        A.BRel   Ident
x  -> (IdU, Dom Exp) -> [(IdU, Dom Exp)]
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> IdU
A.Id Ident
x, Relevance -> Exp -> Dom Exp
forall a. Relevance -> a -> Dom a
Dom Relevance
ShapeIrr   Exp
A.Size)
        A.BAnn [Ident]
xs Exp
a -> (Ident -> (IdU, Dom Exp)) -> [Ident] -> [(IdU, Dom Exp)]
forall a b. (a -> b) -> [a] -> [b]
map (\ Ident
x -> (Ident -> IdU
A.Id Ident
x, Exp -> Dom Exp
forall a. a -> Dom a
defaultDom Exp
a)) [Ident]
xs

    -- Neutral types

    Exp
e | Exp -> Bool
A.introduction Exp
e -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a. ReaderT TCEnv (StateT TCSt (Except Id)) a
invalidType

    Exp
e -> do
      (Type
t,VType
v) <- Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferExp Exp
e
      case VType
v of
        VType VType
l -> (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t,VType
l)
        VType
_ -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a. ReaderT TCEnv (StateT TCSt (Except Id)) a
invalidType

inferPisType :: [(A.IdU, Dom A.Exp)] -> Check (Type, VLevel) -> Check (Type, VLevel)
inferPisType :: [(IdU, Dom Exp)]
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferPisType = ((ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
  -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
 -> (ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
     -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> (ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
    -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> [ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
    -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)]
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> (ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
    -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a. a -> a
id ([ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
  -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)]
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> ([(IdU, Dom Exp)]
    -> [ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
        -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)])
-> [(IdU, Dom Exp)]
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((IdU, Dom Exp)
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> [(IdU, Dom Exp)]
-> [ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
    -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)]
forall a b. (a -> b) -> [a] -> [b]
map ((IdU
 -> Dom Exp
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> (IdU, Dom Exp)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry IdU
-> Dom Exp
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferPiType)

inferPiType :: A.IdU -> Dom A.Exp -> Check (Type, VLevel) -> Check (Type, VLevel)
inferPiType :: IdU
-> Dom Exp
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferPiType IdU
x Dom Exp
dom ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
cont = do

  -- Check the domain
  (Type
u, VType
l1) <- Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferType (Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Dom Exp -> Exp
forall a. Dom a -> a
unDom Dom Exp
dom

  -- Check the codomain in the extended context.
  VType
v <- Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
u
  (IdU, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. AddContext a => a -> Check b -> Check b
addContext (IdU
x, VType
v) (ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
 -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ do
    (Type
t, VType
l2) <- ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
cont

    -- Compute the universe level of the Pi-type.
    let l0 :: VType
l0 = VType -> VType -> VType
maxSize VType
l1 VType
l2

    -- Check that the level does not mention the bound variable
    -- If yes, return oo instead.
    VType
l <- case SizeView -> Maybe SizeView -> SizeView
forall a. a -> Maybe a -> a
fromMaybe __IMPOSSIBLE__ $ sizeView l0 of
      SVVar Int
k' Int
_ -> do
        Int
k <- Cxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Cxt -> Int)
-> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
-> ReaderT TCEnv (StateT TCSt (Except Id)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Cxt) -> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt
        VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (m :: * -> *) a. Monad m => a -> m a
return (VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType)
-> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall a b. (a -> b) -> a -> b
$ if Int
k' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
k then VType
VInfty else VType
l0
      SizeView
_ -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (m :: * -> *) a. Monad m => a -> m a
return VType
l0

    -- Construct the function type
    (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Dom Type -> Abs Type -> Type
Pi (Dom Exp
dom Dom Exp -> Type -> Dom Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
u) (Abs Type -> Type) -> Abs Type -> Type
forall a b. (a -> b) -> a -> b
$ Id -> Type -> Abs Type
forall a. Id -> a -> Abs a
Abs (IdU -> Id
fromIdU IdU
x) Type
t , VType
l )

checkSize :: A.Exp -> Check Size
checkSize :: Exp -> Check Type
checkSize Exp
e = Exp -> VType -> Check Type
checkExp Exp
e VType
VSize

checkLevel :: A.Exp -> Check Level
checkLevel :: Exp -> Check Type
checkLevel = \case
  Exp
A.LZero        -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Type
sZero
  A.App Exp
A.LSuc Exp
e -> Type -> Type
sSuc (Type -> Type) -> Check Type -> Check Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> Check Type
checkLevel Exp
e
  e :: Exp
e@(A.Var IdU
x)    -> Exp -> VType -> Check Type
checkExp Exp
e VType
VSize
  Exp
e -> Id -> Check Type
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> Check Type) -> Id -> Check Type
forall a b. (a -> b) -> a -> b
$ Id
"Not a valid level expression: " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Exp -> Id
forall a. Print a => a -> Id
printTree Exp
e

checkExp :: A.Exp -> VType -> Check Term
checkExp :: Exp -> VType -> Check Type
checkExp Exp
e0 VType
t = do
  case Exp
e0 of

    -- Functions

    A.Lam []     Exp
e -> Exp -> VType -> Check Type
checkExp Exp
e VType
t
    A.Lam (IdU
x:[IdU]
xs) Exp
e -> do
      case VType
t of
        VPi Dom VType
dom VClos
cl -> (IdU, Dom VType) -> Check Type -> Check Type
forall a b. AddContext a => a -> Check b -> Check b
addContext (IdU
x, Dom VType
dom) (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$ do
          VType
t' <- VClos -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyClosure VClos
cl (VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT TCEnv (StateT TCSt (Except Id)) VType
lastVal
          Type
u  <- Exp -> VType -> Check Type
checkExp ([IdU] -> Exp -> Exp
A.Lam [IdU]
xs Exp
e) VType
t'
          Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Relevance -> Abs Type -> Type
Lam (Dom VType -> Relevance
forall a. Dom a -> Relevance
_domInfo Dom VType
dom) (Abs Type -> Type) -> Abs Type -> Type
forall a b. (a -> b) -> a -> b
$ Id -> Type -> Abs Type
forall a. Id -> a -> Abs a
Abs (IdU -> Id
fromIdU IdU
x) Type
u
        VType
_ -> Id -> Check Type
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> Check Type) -> Id -> Check Type
forall a b. (a -> b) -> a -> b
$ Id
"Lambda abstraction expects function type, but got " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ VType -> Id
forall a. Show a => a -> Id
show VType
t

    e :: Exp
e@(A.ELam Exp
ez IdU
x0 Exp
es) -> do
      case VType
t of
        VPi (Dom Relevance
r (VNat VType
b)) VClos
cl -> do
          let x :: Id
x = IdU -> Id
A.fromIdU IdU
x0
          Bool
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Relevance
r Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
Relevant) (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$
            Id
"Extended lambda constructs relevant function: " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Exp -> Id
forall a. Print a => a -> Id
printTree Exp
e
          -- Infer the type of the case expression
          Type
tt <- VType -> Check Type
reifyType VType
t
          -- Make sure that b is a successor size
          let a :: VType
a = VType -> Maybe VType -> VType
forall a. a -> Maybe a -> a
fromMaybe __IMPOSSIBLE__ $ sizePred b
          Type
ta <- VType -> Check Type
reifySize VType
a
          Type
tz <- Exp -> VType -> Check Type
checkExp Exp
ez (VType -> Check Type)
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType -> Check Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VClos -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyClosure VClos
cl (VType -> VType
VZero VType
a)
          (Type
ts0, Type
tS0) <-
            (Id, Dom VType) -> Check (Type, Type) -> Check (Type, Type)
forall a b. AddContext a => a -> Check b -> Check b
addContext (Id
x, Relevance -> VType -> Dom VType
forall a. Relevance -> a -> Dom a
Dom Relevance
Relevant (VType -> Dom VType) -> VType -> Dom VType
forall a b. (a -> b) -> a -> b
$ VType -> VType
VNat VType
a) (Check (Type, Type) -> Check (Type, Type))
-> Check (Type, Type) -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ do
              VType
vts <- VClos -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyClosure VClos
cl (VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do VType -> VType -> VType
VSuc VType
a (VType -> VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT TCEnv (StateT TCSt (Except Id)) VType
lastVal
              Type
tS0 <- VType -> Check Type
reifyType VType
vts
              (,Type
tS0) (Type -> (Type, Type)) -> Check Type -> Check (Type, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> VType -> Check Type
checkExp Exp
es VType
vts
          let ts :: Type
ts = Relevance -> Abs Type -> Type
Lam Relevance
Relevant (Abs Type -> Type) -> Abs Type -> Type
forall a b. (a -> b) -> a -> b
$ Id -> Type -> Abs Type
forall a. Id -> a -> Abs a
Abs Id
x Type
ts0
          let tS :: Type
tS = Dom Type -> Abs Type -> Type
Pi (Relevance -> Type -> Dom Type
forall a. Relevance -> a -> Dom a
Dom Relevance
Relevant (Type -> Dom Type) -> Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Nat Type
ta) (Abs Type -> Type) -> Abs Type -> Type
forall a b. (a -> b) -> a -> b
$ Id -> Type -> Abs Type
forall a. Id -> a -> Abs a
Abs Id
x Type
tS0
          Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Relevance -> Abs Type -> Type
Lam Relevance
Relevant (Abs Type -> Type) -> Abs Type -> Type
forall a b. (a -> b) -> a -> b
$ Id -> Type -> Abs Type
forall a. Id -> a -> Abs a
Abs Id
"x" (Type -> Abs Type) -> Type -> Abs Type
forall a b. (a -> b) -> a -> b
$ Type -> Elim -> Type
App (Index -> Type
Var Index
0) (Elim -> Type) -> Elim -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Elim -> Elim
forall a. Substitute a => Int -> a -> a
raise Int
1 (Elim -> Elim) -> Elim -> Elim
forall a b. (a -> b) -> a -> b
$
            Type -> Type -> Type -> Type -> Elim
forall a. a -> a -> a -> a -> Elim' a
Case Type
tt Type
tz Type
tS Type
ts

        VType
_ -> Id -> Check Type
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> Check Type) -> Id -> Check Type
forall a b. (a -> b) -> a -> b
$ Id
"Extended lambda is function from Nat _, but here it got type " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ VType -> Id
forall a. Show a => a -> Id
show VType
t

    Exp
e -> do
      (Type
u, VType
ti) <- Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferExp Exp
e
      Type -> VType -> VType -> Check Type
coerce Type
u VType
ti VType
t

-- | Infers neutrals, natural numbers, types.

inferExp :: A.Exp -> Check (Term, VType)
inferExp :: Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferExp Exp
e0 = case (Exp
e0, Exp -> (Exp, [Exp])
appView Exp
e0) of

  (Exp
e,(Exp, [Exp])
_) | Exp -> Bool
mustBeType Exp
e -> do
    (Type
t, VType
l) <- Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferType Exp
e
    (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, VType -> VType
VType VType
l)

  (Exp
e, (Exp
A.Zero, [Exp]
es)) -> do
    case [Exp]
es of
      [ Exp
ea ] -> do
        Type
a <- Relevance -> Check Type -> Check Type
forall a. Relevance -> Check a -> Check a
resurrect Relevance
Irrelevant (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Exp -> Check Type
checkSize Exp
ea
        (Type -> Type
zero Type
a ,) (VType -> (Type, VType))
-> (VType -> VType) -> VType -> (Type, VType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VType -> VType
VNat (VType -> VType) -> (VType -> VType) -> VType -> VType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VType -> VType
vsSuc (VType -> (Type, VType))
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
a
      [Exp]
_ -> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Id
"zero expects exactly 1 argument: " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Exp -> Id
forall a. Print a => a -> Id
printTree Exp
e

  (Exp
e, (Exp
A.Suc, [Exp]
es)) -> do
    case [Exp]
es of
      [ Exp
ea, Exp
en ] -> do
        Type
a <- Relevance -> Check Type -> Check Type
forall a. Relevance -> Check a -> Check a
resurrect Relevance
Irrelevant (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Exp -> Check Type
checkSize Exp
ea
        VType
va <- Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
a
        Type
n <- Exp -> VType -> Check Type
checkExp Exp
en (VType -> Check Type) -> VType -> Check Type
forall a b. (a -> b) -> a -> b
$ VType -> VType
VNat VType
va
        (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
suc Type
a Type
n, VType -> VType
VNat (VType -> VType) -> VType -> VType
forall a b. (a -> b) -> a -> b
$ VType -> VType
vsSuc VType
va)
      [Exp]
_ -> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Id
"suc expects exactly 2 arguments: " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Exp -> Id
forall a. Print a => a -> Id
printTree Exp
e

  (Exp
e, (Exp
A.Fix, [Exp]
es)) -> do
    case [Exp]
es of
      (Exp
et : Exp
ef : Exp
en : []) -> do
        -- Check the motive of elimination
        Type
tT <- Exp -> VType -> Check Type
checkExp Exp
et VType
fixKindV
        -- Check the functional
        let tF :: Type
tF = Type -> Type
fixType Type
tT
        Type
tf <- Exp -> VType -> Check Type
checkExp Exp
ef (VType -> Check Type)
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType -> Check Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
tF
        -- Check the argument
        (Type
tn, VType
a) <- Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferNat Exp
en
        -- Compute the type of the elimination
        VType
vT <- Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
tT
        VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
admissible VType
vT
        VType
vn <- Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
tn
        VType
ve <- VType
-> [Arg VType] -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyArgs VType
vT [ Relevance -> VType -> Arg VType
forall a. Relevance -> a -> Arg a
Arg Relevance
ShapeIrr VType
a , Relevance -> VType -> Arg VType
forall a. Relevance -> a -> Arg a
Arg Relevance
Relevant VType
vn ]
        -- Return as postfix application
        (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Elim -> Type
App Type
tn (Elim -> Type) -> Elim -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> Elim
forall a. a -> a -> a -> Elim' a
Fix Type
tT Type
tF Type
tf, VType
ve)

      [Exp]
_ -> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Id
"fix expects exactly 3 arguments: " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Exp -> Id
forall a. Print a => a -> Id
printTree Exp
e

  (Exp
A.Infty, (Exp, [Exp])
_) -> (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
Infty, VType
VSize)

  (A.Plus Exp
e Integer
k, (Exp, [Exp])
_) -> do
    Type
u <- Exp -> Check Type
checkSize Exp
e
    (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Integer -> Type
sPlus Type
u Integer
k, VType
VSize)

  (A.Var IdU
A.Under, (Exp, [Exp])
_) -> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Id
"Illegal expression: _"
  (A.Var (A.Id Ident
x), (Exp, [Exp])
_) -> Ident -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferId Ident
x

  (e0 :: Exp
e0@(A.App Exp
f Exp
e), (Exp, [Exp])
_) -> do
    (Type
tf, VType
t) <- Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferExp Exp
f
    case VType
t of
      VPi (Dom Relevance
r VType
tdom) VClos
cl -> do
        Type
te <- Relevance -> Check Type -> Check Type
forall a. Relevance -> Check a -> Check a
resurrect Relevance
r (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Exp -> VType -> Check Type
checkExp Exp
e VType
tdom
        VType
v  <- Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
te
        (Type -> Elim -> Type
App Type
tf (Elim -> Type) -> Elim -> Type
forall a b. (a -> b) -> a -> b
$ Arg Type -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Type -> Elim) -> Arg Type -> Elim
forall a b. (a -> b) -> a -> b
$ Relevance -> Type -> Arg Type
forall a. Relevance -> a -> Arg a
Arg Relevance
r Type
te,) (VType -> (Type, VType))
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VClos -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyClosure VClos
cl VType
v
      VType
_ -> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Id
"Function type expected in application " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Exp -> Id
forall a. Print a => a -> Id
printTree Exp
e0
             Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
" ; but found type" Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ VType -> Id
forall a. Show a => a -> Id
show VType
t


  (A.Case{}, (Exp, [Exp])
_)  -> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a. Id -> Check a
nyi Id
"case"

  (Exp
e, (Exp, [Exp])
_) -> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a. Id -> Check a
nyi (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Id
"inferring type of " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Exp -> Id
forall a. Print a => a -> Id
printTree Exp
e

-- | Infer type of a variable

inferId :: A.Ident -> Check (Term, VType)
inferId :: Ident -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferId (A.Ident Id
x) = do
  (Id -> Cxt -> Maybe (Int, Dom VType)
lookupCxt Id
x (Cxt -> Maybe (Int, Dom VType))
-> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Maybe (Int, Dom VType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Cxt) -> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt) ReaderT TCEnv (StateT TCSt (Except Id)) (Maybe (Int, Dom VType))
-> (Maybe (Int, Dom VType)
    -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (Int
i, Dom Relevance
r VType
t)
      | Relevance
r Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
Relevant -> (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Index -> Type
Var (Index -> Type) -> Index -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Index
Index Int
i, VType
t)
      | Bool
otherwise     -> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Id
"Illegal reference to " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Relevance -> Id
forall a. Show a => a -> Id
show Relevance
r Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
" variable: " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id -> Id
forall a. Print a => a -> Id
printTree Id
x

    Maybe (Int, Dom VType)
Nothing     -> do
      (Id -> Map Id VType -> Maybe VType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
x (Map Id VType -> Maybe VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
-> Check (Maybe VType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens TCSt (Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
use Lens TCSt (Map Id VType)
stTySigs) Check (Maybe VType)
-> (Maybe VType
    -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe VType
Nothing -> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Id
"Identifier not in scope: " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
x
        Just VType
t  -> (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> Type
Def Id
x, VType
t)

inferNat :: A.Exp -> Check (Term, VSize)
inferNat :: Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferNat Exp
e = do
  (Type
u,VType
t) <- Exp -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
inferExp Exp
e
  case VType
t of
    VNat VType
a -> (Type, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
u, VType
a)
    VType
_ -> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType))
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) (Type, VType)
forall a b. (a -> b) -> a -> b
$ Id
"Expected natural number, but found " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Exp -> Id
forall a. Print a => a -> Id
printTree Exp
e

-- | Coercion / subtype checking.

coerce :: Term -> VType -> VType -> Check Term
coerce :: Type -> VType -> VType -> Check Type
coerce Type
u VType
ti VType
tc = do
  VType -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
subType VType
ti VType
tc
  Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
u

-- | Type checker auxiliary functions.

traceCheck :: Print a => a -> b -> b
traceCheck :: a -> b -> b
traceCheck a
a = Id -> b -> b
forall a. Id -> a -> a
trace (Id -> b -> b) -> Id -> b -> b
forall a b. (a -> b) -> a -> b
$ Id
"Checking " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ a -> Id
forall a. Print a => a -> Id
printTree a
a

nyi :: String -> Check a
nyi :: Id -> Check a
nyi = Id -> Check a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> Check a) -> (Id -> Id) -> Id -> Check a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id
"Not yet implemented: " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++)

-- | Signature auxiliary functions

lookupTySig :: Id -> Check (Maybe VType)
lookupTySig :: Id -> Check (Maybe VType)
lookupTySig Id
x = Id -> Map Id VType -> Maybe VType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
x (Map Id VType -> Maybe VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
-> Check (Maybe VType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens TCSt (Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
use Lens TCSt (Map Id VType)
stTySigs

lookupDef :: Id -> Check (Maybe Val)
lookupDef :: Id -> Check (Maybe VType)
lookupDef Id
x = Id -> Map Id VType -> Maybe VType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
x (Map Id VType -> Maybe VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
-> Check (Maybe VType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens TCSt (Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
use Lens TCSt (Map Id VType)
stDefs

addTySig :: Id -> VType -> Check ()
addTySig :: Id -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
addTySig Id
x VType
t = Lens TCSt (Map Id VType)
stTySigs Lens TCSt (Map Id VType)
-> (Map Id VType -> Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a (m :: * -> *) b.
MonadState a m =>
Lens a b -> (b -> b) -> m ()
%= Id -> VType -> Map Id VType -> Map Id VType
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
x VType
t

addDef :: Id -> Val -> Check ()
addDef :: Id -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
addDef Id
x VType
v = Lens TCSt (Map Id VType)
stDefs Lens TCSt (Map Id VType)
-> (Map Id VType -> Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a (m :: * -> *) b.
MonadState a m =>
Lens a b -> (b -> b) -> m ()
%= Id -> VType -> Map Id VType -> Map Id VType
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
x VType
v

-- * Invoking evaluation

instance MonadEval (Reader (Map Id Val)) where
  getDef :: Id -> Reader (Map Id VType) VType
getDef Id
x = VType -> Maybe VType -> VType
forall a. a -> Maybe a -> a
fromMaybe __IMPOSSIBLE__ . Map.lookup x <$> ask

evaluate :: Term -> Check Val
evaluate :: Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
t = do
  Map Id VType
sig   <- Lens TCSt (Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
use Lens TCSt (Map Id VType)
stDefs
  Env
delta <- (TCEnv -> Env) -> ReaderT TCEnv (StateT TCSt (Except Id)) Env
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Env
_envEnv
  VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (m :: * -> *) a. Monad m => a -> m a
return (VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType)
-> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall a b. (a -> b) -> a -> b
$ Reader (Map Id VType) VType -> Map Id VType -> VType
forall r a. Reader r a -> r -> a
runReader (Type -> Env -> Reader (Map Id VType) VType
forall (m :: * -> *). MonadEval m => Type -> Env -> m VType
evalIn Type
t Env
delta) Map Id VType
sig

applyClosure :: VClos -> Val -> Check Val
applyClosure :: VClos -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyClosure VClos
cl VType
v =
  Reader (Map Id VType) VType -> Map Id VType -> VType
forall r a. Reader r a -> r -> a
runReader (VClos -> VType -> Reader (Map Id VType) VType
forall (m :: * -> *). MonadEval m => VClos -> VType -> m VType
applyClos VClos
cl VType
v) (Map Id VType -> VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens TCSt (Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
use Lens TCSt (Map Id VType)
stDefs

applyElims :: Val -> VElims -> Check Val
applyElims :: VType -> VElims -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyElims VType
v VElims
es =
  Reader (Map Id VType) VType -> Map Id VType -> VType
forall r a. Reader r a -> r -> a
runReader (VType -> VElims -> Reader (Map Id VType) VType
forall (m :: * -> *). MonadEval m => VType -> VElims -> m VType
applyEs VType
v VElims
es) (Map Id VType -> VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens TCSt (Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
use Lens TCSt (Map Id VType)
stDefs

applyArgs :: Val -> [Arg Val] -> Check Val
applyArgs :: VType
-> [Arg VType] -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyArgs VType
v = VType -> VElims -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyElims VType
v (VElims -> ReaderT TCEnv (StateT TCSt (Except Id)) VType)
-> ([Arg VType] -> VElims)
-> [Arg VType]
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg VType -> Elim' VType) -> [Arg VType] -> VElims
forall a b. (a -> b) -> [a] -> [b]
map Arg VType -> Elim' VType
forall a. Arg a -> Elim' a
Apply

reifyType :: VType -> Check Type
reifyType :: VType -> Check Type
reifyType VType
t = do
  Int
n <- Cxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Cxt -> Int)
-> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
-> ReaderT TCEnv (StateT TCSt (Except Id)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Cxt) -> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt
  Map Id VType
sig <- Lens TCSt (Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
use Lens TCSt (Map Id VType)
stDefs
  Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Reader (Map Id VType) Type -> Map Id VType -> Type
forall r a. Reader r a -> r -> a
runReader (ReaderT Int (Reader (Map Id VType)) Type
-> Int -> Reader (Map Id VType) Type
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (VType -> ReaderT Int (Reader (Map Id VType)) Type
forall (m :: * -> *). MonadEval m => VType -> ReaderT Int m Type
readbackType VType
t) Int
n) Map Id VType
sig

reifySize :: VSize -> Check Size
reifySize :: VType -> Check Type
reifySize VType
t = do
  Int
n <- Cxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Cxt -> Int)
-> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
-> ReaderT TCEnv (StateT TCSt (Except Id)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Cxt) -> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt
  Map Id VType
sig <- Lens TCSt (Map Id VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) (Map Id VType)
forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
use Lens TCSt (Map Id VType)
stDefs
  Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Reader (Map Id VType) Type -> Map Id VType -> Type
forall r a. Reader r a -> r -> a
runReader (ReaderT Int (Reader (Map Id VType)) Type
-> Int -> Reader (Map Id VType) Type
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (VType -> ReaderT Int (Reader (Map Id VType)) Type
forall (m :: * -> *). MonadEval m => VType -> ReaderT Int m Type
readbackSize VType
t) Int
n) Map Id VType
sig

-- * Context manipulation

-- | Looking up in the typing context

lookupCxt :: Id -> Cxt -> Maybe (Int, Dom VType)
lookupCxt :: Id -> Cxt -> Maybe (Int, Dom VType)
lookupCxt Id
x Cxt
cxt = Int -> Cxt -> Maybe (Int, Dom VType)
forall t b. Enum t => t -> [(Id, b)] -> Maybe (t, b)
loop Int
0 Cxt
cxt
  where
  loop :: t -> [(Id, b)] -> Maybe (t, b)
loop t
i = \case
    [] -> Maybe (t, b)
forall a. Maybe a
Nothing
    ((Id
y,b
t) : [(Id, b)]
cxt)
      | Id
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
y    -> (t, b) -> Maybe (t, b)
forall a. a -> Maybe a
Just (t
i,b
t)
      | Bool
otherwise -> t -> [(Id, b)] -> Maybe (t, b)
loop (t -> t
forall a. Enum a => a -> a
succ t
i) [(Id, b)]
cxt


-- | Value of last variable added to context.

lastVal :: Check Val
lastVal :: ReaderT TCEnv (StateT TCSt (Except Id)) VType
lastVal = Env -> VType
forall a. [a] -> a
head (Env -> VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) Env
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Env) -> ReaderT TCEnv (StateT TCSt (Except Id)) Env
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Env
_envEnv

-- | Extending the typing context

class AddContext a where
  addContext :: a -> Check b -> Check b

instance AddContext a => AddContext [a] where
  addContext :: [a] -> Check b -> Check b
addContext [a]
as = ((Check b -> Check b)
 -> (Check b -> Check b) -> Check b -> Check b)
-> (Check b -> Check b)
-> [Check b -> Check b]
-> Check b
-> Check b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Check b -> Check b) -> (Check b -> Check b) -> Check b -> Check b
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Check b -> Check b
forall a. a -> a
id ([Check b -> Check b] -> Check b -> Check b)
-> [Check b -> Check b] -> Check b -> Check b
forall a b. (a -> b) -> a -> b
$ (a -> Check b -> Check b) -> [a] -> [Check b -> Check b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Check b -> Check b
forall a b. AddContext a => a -> Check b -> Check b
addContext [a]
as

-- A.IdU instances

instance AddContext (A.IdU, Type) where
  addContext :: (IdU, Type) -> Check b -> Check b
addContext (IdU
x,Type
t) = (Id, Type) -> Check b -> Check b
forall a b. AddContext a => a -> Check b -> Check b
addContext (IdU -> Id
fromIdU IdU
x, Type
t)

instance AddContext (A.IdU, VType) where
  addContext :: (IdU, VType) -> Check b -> Check b
addContext (IdU
x,VType
t) = (Id, VType) -> Check b -> Check b
forall a b. AddContext a => a -> Check b -> Check b
addContext (IdU -> Id
fromIdU IdU
x, VType
t)

instance AddContext (A.IdU, Dom VType) where
  addContext :: (IdU, Dom VType) -> Check b -> Check b
addContext (IdU
x,Dom VType
t) = (Id, Dom VType) -> Check b -> Check b
forall a b. AddContext a => a -> Check b -> Check b
addContext (IdU -> Id
fromIdU IdU
x, Dom VType
t)

-- Id instances

instance AddContext (Id, Type) where
  addContext :: (Id, Type) -> Check b -> Check b
addContext (Id
x,Type
t) Check b
cont = do
    VType
t <- Type -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
evaluate Type
t
    (Id, VType) -> Check b -> Check b
forall a b. AddContext a => a -> Check b -> Check b
addContext (Id
x,VType
t) Check b
cont

instance AddContext (Id, VType) where
  addContext :: (Id, VType) -> Check b -> Check b
addContext (Id
x,VType
t) = (Id, Dom VType) -> Check b -> Check b
forall a b. AddContext a => a -> Check b -> Check b
addContext (Id
x, VType -> Dom VType
forall a. a -> Dom a
defaultDom VType
t)

instance AddContext (Id, Dom VType) where
  addContext :: (Id, Dom VType) -> Check b -> Check b
addContext (Id
x,Dom VType
t) = (TCEnv -> TCEnv) -> Check b -> Check b
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local
    ((TCEnv -> TCEnv) -> Check b -> Check b)
-> (TCEnv -> TCEnv) -> Check b -> Check b
forall a b. (a -> b) -> a -> b
$ Lens TCEnv Cxt -> (Cxt -> Cxt) -> TCEnv -> TCEnv
forall a b. Lens a b -> (b -> b) -> a -> a
over Lens TCEnv Cxt
envCxt ((Id
x,Dom VType
t)(Id, Dom VType) -> Cxt -> Cxt
forall a. a -> [a] -> [a]
:)
    (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens TCEnv Env -> (Env -> Env) -> TCEnv -> TCEnv
forall a b. Lens a b -> (b -> b) -> a -> a
over Lens TCEnv Env
envEnv Env -> Env
nextVar
    where nextVar :: Env -> Env
nextVar Env
delta = VType -> Int -> VType
vVar (Dom VType -> VType
forall a. Dom a -> a
unDom Dom VType
t) (Env -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
delta) VType -> Env -> Env
forall a. a -> [a] -> [a]
: Env
delta

-- | Context: resurrecting irrelevant variables
resurrect :: Relevance -> Check a -> Check a
resurrect :: Relevance -> Check a -> Check a
resurrect = \case
  -- Relevant application: resurrect nothing.
  Relevance
Relevant   -> Check a -> Check a
forall a. a -> a
id
  -- Irrelevant application: resurrect everything.
  Relevance
Irrelevant -> (TCEnv -> TCEnv) -> Check a -> Check a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((TCEnv -> TCEnv) -> Check a -> Check a)
-> (TCEnv -> TCEnv) -> Check a -> Check a
forall a b. (a -> b) -> a -> b
$ Lens TCEnv Cxt -> (Cxt -> Cxt) -> TCEnv -> TCEnv
forall a b. Lens a b -> (b -> b) -> a -> a
over Lens TCEnv Cxt
envCxt ((Cxt -> Cxt) -> TCEnv -> TCEnv) -> (Cxt -> Cxt) -> TCEnv -> TCEnv
forall a b. (a -> b) -> a -> b
$ ((Id, Dom VType) -> (Id, Dom VType)) -> Cxt -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (((Id, Dom VType) -> (Id, Dom VType)) -> Cxt -> Cxt)
-> ((Id, Dom VType) -> (Id, Dom VType)) -> Cxt -> Cxt
forall a b. (a -> b) -> a -> b
$ Lens (Id, Dom VType) (Dom VType)
-> (Dom VType -> Dom VType) -> (Id, Dom VType) -> (Id, Dom VType)
forall a b. Lens a b -> (b -> b) -> a -> a
over Lens (Id, Dom VType) (Dom VType)
forall a b. Lens (a, b) b
_2 ((Dom VType -> Dom VType) -> (Id, Dom VType) -> (Id, Dom VType))
-> (Dom VType -> Dom VType) -> (Id, Dom VType) -> (Id, Dom VType)
forall a b. (a -> b) -> a -> b
$ Lens (Dom VType) Relevance -> Relevance -> Dom VType -> Dom VType
forall a b. Lens a b -> b -> a -> a
set Lens (Dom VType) Relevance
forall a. Lens (Dom a) Relevance
domInfo Relevance
Relevant
  -- Shape irrelevant application: resurrect shape-irrelevant variables.
  Relevance
ShapeIrr   -> (TCEnv -> TCEnv) -> Check a -> Check a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((TCEnv -> TCEnv) -> Check a -> Check a)
-> (TCEnv -> TCEnv) -> Check a -> Check a
forall a b. (a -> b) -> a -> b
$ Lens TCEnv Cxt -> (Cxt -> Cxt) -> TCEnv -> TCEnv
forall a b. Lens a b -> (b -> b) -> a -> a
over Lens TCEnv Cxt
envCxt ((Cxt -> Cxt) -> TCEnv -> TCEnv) -> (Cxt -> Cxt) -> TCEnv -> TCEnv
forall a b. (a -> b) -> a -> b
$ ((Id, Dom VType) -> (Id, Dom VType)) -> Cxt -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (((Id, Dom VType) -> (Id, Dom VType)) -> Cxt -> Cxt)
-> ((Id, Dom VType) -> (Id, Dom VType)) -> Cxt -> Cxt
forall a b. (a -> b) -> a -> b
$ Lens (Id, Dom VType) (Dom VType)
-> (Dom VType -> Dom VType) -> (Id, Dom VType) -> (Id, Dom VType)
forall a b. Lens a b -> (b -> b) -> a -> a
over Lens (Id, Dom VType) (Dom VType)
forall a b. Lens (a, b) b
_2 ((Dom VType -> Dom VType) -> (Id, Dom VType) -> (Id, Dom VType))
-> (Dom VType -> Dom VType) -> (Id, Dom VType) -> (Id, Dom VType)
forall a b. (a -> b) -> a -> b
$ Lens (Dom VType) Relevance
-> (Relevance -> Relevance) -> Dom VType -> Dom VType
forall a b. Lens a b -> (b -> b) -> a -> a
over Lens (Dom VType) Relevance
forall a. Lens (Dom a) Relevance
domInfo ((Relevance -> Relevance) -> Dom VType -> Dom VType)
-> (Relevance -> Relevance) -> Dom VType -> Dom VType
forall a b. (a -> b) -> a -> b
$ Relevance -> Relevance
resSI
    where
    resSI :: Relevance -> Relevance
resSI = \case
      Relevance
ShapeIrr -> Relevance
Relevant
      Relevance
r -> Relevance
r

-- * Subtyping and type equality

subType :: Val -> Val -> Check ()
subType :: VType -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
subType VType
ti VType
tc = do
  let failure :: ReaderT TCEnv (StateT TCSt (Except Id)) a
failure = Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a)
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) a
forall a b. (a -> b) -> a -> b
$ Id
"Subtyping failed: type " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ VType -> Id
forall a. Show a => a -> Id
show VType
ti
        Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
" is not a subtype of " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ VType -> Id
forall a. Show a => a -> Id
show VType
tc
  case (VType
ti, VType
tc) of
    (VNat  VType
a, VNat  VType
b) -> Bool
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (VType -> VType -> Bool
leqSize VType
a VType
b) ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a. ReaderT TCEnv (StateT TCSt (Except Id)) a
failure
    (VType VType
a, VType VType
b) -> Bool
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (VType -> VType -> Bool
leqSize VType
a VType
b) ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a. ReaderT TCEnv (StateT TCSt (Except Id)) a
failure
    (VPi Dom VType
dom1 VClos
cl1, VPi Dom VType
dom2 VClos
cl2) -> do
      Bool
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Dom VType -> Relevance
forall a. Dom a -> Relevance
_domInfo Dom VType
dom2 Relevance -> Relevance -> Bool
forall a. Ord a => a -> a -> Bool
<= Dom VType -> Relevance
forall a. Dom a -> Relevance
_domInfo Dom VType
dom1) ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a. ReaderT TCEnv (StateT TCSt (Except Id)) a
failure
      VType -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
subType (Dom VType -> VType
forall a. Dom a -> a
unDom Dom VType
dom2) (Dom VType -> VType
forall a. Dom a -> a
unDom Dom VType
dom1)
      (Id, Dom VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. AddContext a => a -> Check b -> Check b
addContext (Abs Type -> Id
forall a. Abs a -> Id
absName (Abs Type -> Id) -> Abs Type -> Id
forall a b. (a -> b) -> a -> b
$ VClos -> Abs Type
closBody VClos
cl2, Dom VType
dom2) (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ do
        VType
v  <- ReaderT TCEnv (StateT TCSt (Except Id)) VType
lastVal
        VType
b1 <- VClos -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyClosure VClos
cl1 VType
v
        VType
b2 <- VClos -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyClosure VClos
cl2 VType
v
        VType -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
subType VType
b1 VType
b2
    (VType, VType)
_ -> VType -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
equalType VType
ti VType
tc

equalType :: Val -> Val -> Check ()
equalType :: VType -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
equalType VType
v VType
v' = do
  Type
t  <- VType -> Check Type
reifyType VType
v
  Type
t' <- VType -> Check Type
reifyType VType
v'
  Bool
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t') (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$
    Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ Id
"Inferred type " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Type -> Id
forall a. Show a => a -> Id
show Type
t Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
" is not equal to expected type " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Type -> Id
forall a. Show a => a -> Id
show Type
t'

-- * Admissibility check for the type of @fix@.

-- | A simple positivity check.
--
--   For the type constructor T of fix we check that
--   @
--     i : ..Size, x : Nat i |- T i x <= T oo x
--   @
--   This does not introduce a new concept an is sound, but excludes
--   @
--     min : forall .i -> Nat i -> Nat i -> Nat i
--   @

admissible :: Val -> Check ()
admissible :: VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
admissible VType
v = do
  Int
k <- Cxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Cxt -> Int)
-> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
-> ReaderT TCEnv (StateT TCSt (Except Id)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Cxt) -> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt
  (Id, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. AddContext a => a -> Check b -> Check b
addContext (Id
"i", VType
VSize) (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ do
    VType
va <- ReaderT TCEnv (StateT TCSt (Except Id)) VType
lastVal
    (Id, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. AddContext a => a -> Check b -> Check b
addContext (Id
"x", VType -> VType
VNat (VType -> VType) -> VType -> VType
forall a b. (a -> b) -> a -> b
$ VType
va) (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ do
      VType
u  <- ReaderT TCEnv (StateT TCSt (Except Id)) VType
lastVal
      VType
t1  <- VType
-> [Arg VType] -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyArgs VType
v [ Relevance -> VType -> Arg VType
forall a. Relevance -> a -> Arg a
Arg Relevance
ShapeIrr VType
va, Relevance -> VType -> Arg VType
forall a. Relevance -> a -> Arg a
Arg Relevance
Relevant VType
u]
      VType
t2  <- VType
-> [Arg VType] -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyArgs VType
v [ Relevance -> VType -> Arg VType
forall a. Relevance -> a -> Arg a
Arg Relevance
ShapeIrr VType
VInfty, Relevance -> VType -> Arg VType
forall a. Relevance -> a -> Arg a
Arg Relevance
Relevant VType
u]
      VType -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
subType VType
t1 VType
t2

-- | Semi-continuity check (to be completed)

admissibleSemi :: Val -> Check ()
admissibleSemi :: VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
admissibleSemi VType
v = do
  Int
k <- Cxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Cxt -> Int)
-> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
-> ReaderT TCEnv (StateT TCSt (Except Id)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Cxt) -> ReaderT TCEnv (StateT TCSt (Except Id)) Cxt
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt
  (Id, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. AddContext a => a -> Check b -> Check b
addContext (Id
"i", VType
VSize) (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ do
    VType
va <- ReaderT TCEnv (StateT TCSt (Except Id)) VType
lastVal
    (Id, VType)
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. AddContext a => a -> Check b -> Check b
addContext (Id
"x", VType -> VType
VNat (VType -> VType) -> VType -> VType
forall a b. (a -> b) -> a -> b
$ VType
va) (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ do
      VType
u  <- ReaderT TCEnv (StateT TCSt (Except Id)) VType
lastVal
      VType
tv  <- VType
-> [Arg VType] -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyArgs VType
v [ Relevance -> VType -> Arg VType
forall a. Relevance -> a -> Arg a
Arg Relevance
ShapeIrr VType
va, Relevance -> VType -> Arg VType
forall a. Relevance -> a -> Arg a
Arg Relevance
Relevant VType
u]
      Id -> Int -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
debug Id
"testing upperSemi" Int
k VType
tv
      Bool
ok <- Int -> VType -> Check Bool
upperSemi Int
k VType
tv
      Bool
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ do
        Type
t <- VType -> Check Type
reifyType VType
tv
        Type
a <- VType -> Check Type
reifySize VType
va
        Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$
          Id
"Type " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Type -> Id
forall a. Show a => a -> Id
show Type
t Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
" of fix needs to be upper semi-continuous in size " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Type -> Id
forall a. Show a => a -> Id
show Type
a

debug :: String -> VGen -> VType -> Check ()
debug :: Id -> Int -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
debug Id
txt Int
k VType
tv = do
    Type
a <- VType -> Check Type
reifySize (VType -> Check Type) -> VType -> Check Type
forall a b. (a -> b) -> a -> b
$ Int -> VType
vsVar Int
k
    Type
t <- VType -> Check Type
reifyType VType
tv
    Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Id -> f ()
traceM (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ Id
txt Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
" " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Type -> Id
forall a. Show a => a -> Id
show Type
a Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
"  " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Type -> Id
forall a. Show a => a -> Id
show Type
t

-- | For a function type to be upper semi-continuous,
--   its codomain needs to be so, and
--   the domain needs to be lower semi-continous.

upperSemi :: VGen -> VType -> Check Bool
upperSemi :: Int -> VType -> Check Bool
upperSemi Int
k VType
t = do
  Id -> Int -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
debug Id
"upperSemi" Int
k VType
t
  case VType
t of
    VPi Dom VType
dom VClos
cl -> do
      Int -> VType -> Check Bool
lowerSemi Int
k (VType -> Check Bool) -> VType -> Check Bool
forall a b. (a -> b) -> a -> b
$ Dom VType -> VType
forall a. Dom a -> a
unDom Dom VType
dom
      (Id, Dom VType) -> Check Bool -> Check Bool
forall a b. AddContext a => a -> Check b -> Check b
addContext (Abs Type -> Id
forall a. Abs a -> Id
absName (Abs Type -> Id) -> Abs Type -> Id
forall a b. (a -> b) -> a -> b
$ VClos -> Abs Type
closBody VClos
cl, Dom VType
dom) (Check Bool -> Check Bool) -> Check Bool -> Check Bool
forall a b. (a -> b) -> a -> b
$ do
        VType
v <- ReaderT TCEnv (StateT TCSt (Except Id)) VType
lastVal
        Int -> VType -> Check Bool
upperSemi Int
k (VType -> Check Bool)
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType -> Check Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VClos -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyClosure VClos
cl VType
v
    VType{}         -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VType
VSize           -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VNat{}          -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    t :: VType
t@(VUp (VType VType
_) VNe
_) -> Int -> Bool -> VType -> Check Bool
monotone Int
k Bool
True VType
t
    VType
t -> do
     Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Id -> f ()
traceM (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ Id
"upperSemi " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Int -> Id
forall a. Show a => a -> Id
show Int
k Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
"  " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ VType -> Id
forall a. Show a => a -> Id
show VType
t
     __IMPOSSIBLE__

-- | Base types and antitone types are lower semi-continuous.

lowerSemi :: VGen -> VType -> Check Bool
lowerSemi :: Int -> VType -> Check Bool
lowerSemi Int
k VType
t = do
  Id -> Int -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
debug Id
"lowerSemi" Int
k VType
t
  case VType
t of
    t :: VType
t@(VPi Dom VType
dom VClos
cl)  -> Int -> Bool -> VType -> Check Bool
monotone Int
k Bool
False VType
t
    VType{}         -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VType
VSize           -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VNat{}          -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    t :: VType
t@(VUp (VType VType
_) VNe
_) -> Int -> Bool -> VType -> Check Bool
monotone Int
k Bool
False VType
t
    VType
t -> do
     Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Id -> f ()
traceM (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ Id
"lowerSemi " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Int -> Id
forall a. Show a => a -> Id
show Int
k Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
"  " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ VType -> Id
forall a. Show a => a -> Id
show VType
t
     __IMPOSSIBLE__

monotone :: VGen -> Bool -> VType -> Check Bool
monotone :: Int -> Bool -> VType -> Check Bool
monotone Int
k Bool
b VType
t = do
  Id -> Int -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
debug (if Bool
b then Id
"monotone" else Id
"antitone") Int
k VType
t
  case VType
t of
    VPi Dom VType
dom VClos
cl -> do
      Int -> Bool -> VType -> Check Bool
monotone Int
k (Bool -> Bool
not Bool
b) (VType -> Check Bool) -> VType -> Check Bool
forall a b. (a -> b) -> a -> b
$ Dom VType -> VType
forall a. Dom a -> a
unDom Dom VType
dom
      (Id, Dom VType) -> Check Bool -> Check Bool
forall a b. AddContext a => a -> Check b -> Check b
addContext (Abs Type -> Id
forall a. Abs a -> Id
absName (Abs Type -> Id) -> Abs Type -> Id
forall a b. (a -> b) -> a -> b
$ VClos -> Abs Type
closBody VClos
cl, Dom VType
dom) (Check Bool -> Check Bool) -> Check Bool -> Check Bool
forall a b. (a -> b) -> a -> b
$ do
        VType
u <- ReaderT TCEnv (StateT TCSt (Except Id)) VType
lastVal
        Int -> Bool -> VType -> Check Bool
monotone Int
k Bool
b (VType -> Check Bool)
-> ReaderT TCEnv (StateT TCSt (Except Id)) VType -> Check Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VClos -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) VType
applyClosure VClos
cl VType
u
    VType VType
a -> Int -> Bool -> VType -> Check Bool
monotoneSize Int
k Bool
b VType
a
    VNat  VType
a -> Int -> Bool -> VType -> Check Bool
monotoneSize Int
k Bool
b VType
a
    VType
VSize   -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VUp (VType VType
_) VNe
_ -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VType
_ -> __IMPOSSIBLE__

  -- traceM $ "\nmonotone " ++ show k ++ "  " ++ show t
  -- return True

monotoneSize :: VGen -> Bool -> VSize -> Check Bool
monotoneSize :: Int -> Bool -> VType -> Check Bool
monotoneSize Int
k Bool
b VType
t = do
  Id -> Int -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
debugSize (if Bool
b then Id
"monotone" else Id
"antitone") Int
k VType
t
  case VType
t of
    VType
VInfty  -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VZero VType
_ -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VSuc VType
_ VType
v -> Int -> Bool -> VType -> Check Bool
monotoneSize Int
k Bool
b VType
v
    VUp VType
_ (VNe Int
k' VElims
es)
      | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k'   -> do
          Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Id -> f ()
traceM (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ Id
"same var"
          Bool
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (ReaderT TCEnv (StateT TCSt (Except Id)) ()
 -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
-> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Id
"admissibility check failed"
          Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
      | Bool
otherwise -> Bool -> Check Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VType
_ -> __IMPOSSIBLE__

debugSize :: String -> VGen -> VType -> Check ()
debugSize :: Id -> Int -> VType -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
debugSize Id
txt Int
k VType
v = do
    Type
a <- VType -> Check Type
reifySize (VType -> Check Type) -> VType -> Check Type
forall a b. (a -> b) -> a -> b
$ Int -> VType
vsVar Int
k
    Type
b <- VType -> Check Type
reifySize VType
v
    Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall (f :: * -> *). Applicative f => Id -> f ()
traceM (Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ())
-> Id -> ReaderT TCEnv (StateT TCSt (Except Id)) ()
forall a b. (a -> b) -> a -> b
$ Id
txt Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
" " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Type -> Id
forall a. Show a => a -> Id
show Type
a Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Id
"  " Id -> Id -> Id
forall a. [a] -> [a] -> [a]
++ Type -> Id
forall a. Show a => a -> Id
show Type
b