{-# 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 TypeError Val
_stTySigs :: Map Id VType
  , TCSt -> Map TypeError Val
_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 TypeError ()
typeCheck [Decl]
decls = Except TypeError () -> Either TypeError ()
forall e a. Except e a -> Either e a
runExcept (StateT TCSt (Except TypeError) () -> TCSt -> Except TypeError ()
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
-> TCEnv -> StateT TCSt (Except TypeError) ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ([Decl] -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
checkDecls [Decl]
decls) TCEnv
initEnv) TCSt
initSt)
  where
  initEnv :: TCEnv
initEnv = TCEnv { _envCxt :: Cxt
_envCxt   = []        , _envEnv :: Env
_envEnv = []        }
  initSt :: TCSt
initSt  = TCSt  { _stTySigs :: Map TypeError Val
_stTySigs = Map TypeError Val
forall k a. Map k a
Map.empty , _stDefs :: Map TypeError Val
_stDefs = Map TypeError Val
forall k a. Map k a
Map.empty }

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

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

-- | Check a type signature.

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

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

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

-- | Check a definition.

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

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

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

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

-- | Check well-formedness of a type.

checkType :: A.Exp -> Check Type
checkType :: Exp -> Check Type
checkType Exp
e = (Type, Val) -> Type
forall a b. (a, b) -> a
fst ((Type, Val) -> Type)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
-> Check Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
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 TypeError)) (Type, Val)
inferType Exp
e = do
  let invalidType :: ReaderT TCEnv (StateT TCSt (Except TypeError)) a
invalidType = TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall a.
TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a)
-> TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall a b. (a -> b) -> a -> b
$ TypeError
"Not a valid type expression: " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ Exp -> TypeError
forall a. Print a => a -> TypeError
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, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
Size, Int -> Val
vsConst Int
0)

    -- Universes (shape irrelevant)

    Exp
A.Set  -> (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
Type Type
sZero, Int -> Val
vsConst Int
1)
    Exp
A.Set1 -> (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
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 -> Val
vsConst Int
2)
    Exp
A.Set2 -> (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
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 -> Val
vsConst Int
3)
    A.App Exp
A.Set Exp
l -> do
      Type
a <- ArgInfo -> Check Type -> Check Type
forall a. ArgInfo -> Check a -> Check a
resurrect ArgInfo
ShapeIrr (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Exp -> Check Type
checkLevel Exp
l
      Val
v <- Type -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
evaluate Type
a
      (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
Type Type
a, Val -> Val
vsSuc Val
v)

    -- Natural number type (shape irrelevant)

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

    -- Function types

    A.Arrow Exp
a Exp
b -> do
      (Type
u, Val
l1) <- Exp -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
inferType Exp
a
      (Type
t, Val
l2) <- Exp -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
inferType Exp
b
      (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
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) (TypeError -> Type -> Abs Type
forall a. TypeError -> a -> Abs a
NoAbs TypeError
"_" Type
t) , Val -> Val -> Val
maxSize Val
l1 Val
l2)

    A.Pi Exp
e Exp
a Exp
b -> do
      let failure :: ReaderT TCEnv (StateT TCSt (Except TypeError)) a
failure = TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall a.
TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a)
-> TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall a b. (a -> b) -> a -> b
$ TypeError
"Expected list of identifiers, found " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ Exp -> TypeError
forall a. Print a => a -> TypeError
printTree Exp
e
      [IdU]
xs <- ReaderT TCEnv (StateT TCSt (Except TypeError)) [IdU]
-> ([IdU] -> ReaderT TCEnv (StateT TCSt (Except TypeError)) [IdU])
-> Maybe [IdU]
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) [IdU]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReaderT TCEnv (StateT TCSt (Except TypeError)) [IdU]
forall {a}. ReaderT TCEnv (StateT TCSt (Except TypeError)) a
failure [IdU] -> ReaderT TCEnv (StateT TCSt (Except TypeError)) [IdU]
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [IdU]
 -> ReaderT TCEnv (StateT TCSt (Except TypeError)) [IdU])
-> Maybe [IdU]
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) [IdU]
forall a b. (a -> b) -> a -> b
$ Exp -> Maybe [IdU]
parseIdUs Exp
e
      [(IdU, Dom Exp)]
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
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 TypeError)) (Type, Val)
 -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val))
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a b. (a -> b) -> a -> b
$ Exp -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
inferType Exp
b

    A.Forall [Bind]
bs Exp
c -> [(IdU, Dom Exp)]
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
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 TypeError)) (Type, Val)
 -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val))
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a b. (a -> b) -> a -> b
$ Exp -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
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 a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> IdU
A.Id Ident
x, ArgInfo -> Exp -> Dom Exp
forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
Irrelevant Exp
A.Size)
        A.BRel   Ident
x  -> (IdU, Dom Exp) -> [(IdU, Dom Exp)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> IdU
A.Id Ident
x, ArgInfo -> Exp -> Dom Exp
forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
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 TypeError)) (Type, Val)
forall {a}. ReaderT TCEnv (StateT TCSt (Except TypeError)) a
invalidType

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

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

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

  -- Check the domain
  (Type
u, Val
l1) <- Exp -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
inferType (Exp -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val))
-> Exp
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
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.
  Val
v <- Type -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
evaluate Type
u
  (IdU, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall b. (IdU, Val) -> Check b -> Check b
forall a b. AddContext a => a -> Check b -> Check b
addContext (IdU
x, Val
v) (ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
 -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val))
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a b. (a -> b) -> a -> b
$ do
    (Type
t, Val
l2) <- ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
cont

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

    -- Check that the level does not mention the bound variable
    -- If yes, return oo instead.
    Val
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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Cxt -> Int)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) Cxt
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Cxt)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) Cxt
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt
        Val -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val)
-> Val -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
forall a b. (a -> b) -> a -> b
$ if Int
k' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
k then Val
VInfty else Val
l0
      SizeView
_ -> Val -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Val
l0

    -- Construct the function type
    (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
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
$ TypeError -> Type -> Abs Type
forall a. TypeError -> a -> Abs a
Abs (IdU -> TypeError
fromIdU IdU
x) Type
t , Val
l )

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

checkLevel :: A.Exp -> Check Level
checkLevel :: Exp -> Check Type
checkLevel = \case
  Exp
A.LZero        -> Type -> Check Type
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
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 -> Val -> Check Type
checkExp Exp
e Val
VSize
  Exp
e -> TypeError -> Check Type
forall a.
TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> Check Type) -> TypeError -> Check Type
forall a b. (a -> b) -> a -> b
$ TypeError
"Not a valid level expression: " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ Exp -> TypeError
forall a. Print a => a -> TypeError
printTree Exp
e

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

    -- Functions

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

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

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

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

-- | Infers neutrals, natural numbers, types.

inferExp :: A.Exp -> Check (Term, VType)
inferExp :: Exp -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
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, Val
l) <- Exp -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
inferType Exp
e
    (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, Val -> Val
VType Val
l)

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

  (Exp
e, (Exp
A.Suc, [Exp]
es)) -> do
    case [Exp]
es of
      [ Exp
ea, Exp
en ] -> do
        Type
a <- ArgInfo -> Check Type -> Check Type
forall a. ArgInfo -> Check a -> Check a
resurrect ArgInfo
Irrelevant (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Exp -> Check Type
checkSize Exp
ea
        Val
va <- Type -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
evaluate Type
a
        Type
n <- Exp -> Val -> Check Type
checkExp Exp
en (Val -> Check Type) -> Val -> Check Type
forall a b. (a -> b) -> a -> b
$ Val -> Val
VNat Val
va
        (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
suc Type
a Type
n, Val -> Val
VNat (Val -> Val) -> Val -> Val
forall a b. (a -> b) -> a -> b
$ Val -> Val
vsSuc Val
va)
      [Exp]
_ -> TypeError
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a.
TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError
 -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val))
-> TypeError
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a b. (a -> b) -> a -> b
$ TypeError
"suc expects exactly 2 arguments: " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ Exp -> TypeError
forall a. Print a => a -> TypeError
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 -> Val -> Check Type
checkExp Exp
et Val
fixKindV
        -- Check the functional
        let tF :: Type
tF = Type -> Type
fixType Type
tT
        Type
tf <- Exp -> Val -> Check Type
checkExp Exp
ef (Val -> Check Type)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val -> Check Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
evaluate Type
tF
        -- Check the argument
        (Type
tn, Val
a) <- Exp -> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
inferNat Exp
en
        -- Compute the type of the elimination
        Val
vT <- Type -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
evaluate Type
tT
        Val -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
admissible Val
vT
        Val
vn <- Type -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
evaluate Type
tn
        Val
ve <- Val
-> [Arg Val] -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
applyArgs Val
vT [ ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
ShapeIrr Val
a , ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant Val
vn ]
        -- Return as postfix application
        (Type, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) (Type, Val)
forall a. a -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
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, Val
ve)

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

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

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

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

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


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

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

-- | Infer type of a variable

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

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

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

-- | Coercion / subtype checking.

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

-- | Type checker auxiliary functions.

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

nyi :: String -> Check a
nyi :: forall a.
TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
nyi = TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall a.
TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a)
-> (TypeError -> TypeError)
-> TypeError
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeError
"Not yet implemented: " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++)

-- | Signature auxiliary functions

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

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

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

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

-- * Invoking evaluation

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

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

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

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

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

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

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

-- * Context manipulation

-- | Looking up in the typing context

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


-- | Value of last variable added to context.

lastVal :: Check Val
lastVal :: ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
lastVal = Env -> Val
forall a. HasCallStack => [a] -> a
head (Env -> Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) Env
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Env)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) 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 :: forall b. [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 a b. (a -> b -> b) -> b -> [a] -> 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 b. 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 :: forall b. (IdU, Type) -> Check b -> Check b
addContext (IdU
x,Type
t) = (TypeError, Type) -> Check b -> Check b
forall b. (TypeError, Type) -> Check b -> Check b
forall a b. AddContext a => a -> Check b -> Check b
addContext (IdU -> TypeError
fromIdU IdU
x, Type
t)

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

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

-- Id instances

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

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

instance AddContext (Id, Dom VType) where
  addContext :: forall b. (TypeError, Dom Val) -> Check b -> Check b
addContext (TypeError
x,Dom Val
t) = (TCEnv -> TCEnv)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) b
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) b
forall a.
(TCEnv -> TCEnv)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local
    ((TCEnv -> TCEnv)
 -> ReaderT TCEnv (StateT TCSt (Except TypeError)) b
 -> ReaderT TCEnv (StateT TCSt (Except TypeError)) b)
-> (TCEnv -> TCEnv)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) b
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) 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 ((TypeError
x,Dom Val
t)(TypeError, Dom Val) -> 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 = Val -> Int -> Val
vVar (Dom Val -> Val
forall a. Dom a -> a
unDom Dom Val
t) (Env -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
delta) Val -> Env -> Env
forall a. a -> [a] -> [a]
: Env
delta

-- | Context: resurrecting irrelevant variables
resurrect :: Relevance -> Check a -> Check a
resurrect :: forall a. ArgInfo -> Check a -> Check a
resurrect = \case
  -- Relevant application: resurrect nothing.
  ArgInfo
Relevant   -> Check a -> Check a
forall a. a -> a
id
  -- Irrelevant application: resurrect everything.
  ArgInfo
Irrelevant -> (TCEnv -> TCEnv) -> Check a -> Check a
forall a.
(TCEnv -> TCEnv)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) 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
$ ((TypeError, Dom Val) -> (TypeError, Dom Val)) -> Cxt -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (((TypeError, Dom Val) -> (TypeError, Dom Val)) -> Cxt -> Cxt)
-> ((TypeError, Dom Val) -> (TypeError, Dom Val)) -> Cxt -> Cxt
forall a b. (a -> b) -> a -> b
$ Lens (TypeError, Dom Val) (Dom Val)
-> (Dom Val -> Dom Val)
-> (TypeError, Dom Val)
-> (TypeError, Dom Val)
forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over Lens (TypeError, Dom Val) (Dom Val)
forall {a} {b}. Lens (a, b) b
_2 ((Dom Val -> Dom Val)
 -> (TypeError, Dom Val) -> (TypeError, Dom Val))
-> (Dom Val -> Dom Val)
-> (TypeError, Dom Val)
-> (TypeError, Dom Val)
forall a b. (a -> b) -> a -> b
$ Lens (Dom Val) ArgInfo -> ArgInfo -> Dom Val -> Dom Val
forall {a} {b}. Lens a b -> b -> a -> a
set Lens (Dom Val) ArgInfo
forall a. Lens (Dom a) ArgInfo
domInfo ArgInfo
Relevant
  -- Shape irrelevant application: resurrect shape-irrelevant variables.
  ArgInfo
ShapeIrr   -> (TCEnv -> TCEnv) -> Check a -> Check a
forall a.
(TCEnv -> TCEnv)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) 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
$ ((TypeError, Dom Val) -> (TypeError, Dom Val)) -> Cxt -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (((TypeError, Dom Val) -> (TypeError, Dom Val)) -> Cxt -> Cxt)
-> ((TypeError, Dom Val) -> (TypeError, Dom Val)) -> Cxt -> Cxt
forall a b. (a -> b) -> a -> b
$ Lens (TypeError, Dom Val) (Dom Val)
-> (Dom Val -> Dom Val)
-> (TypeError, Dom Val)
-> (TypeError, Dom Val)
forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over Lens (TypeError, Dom Val) (Dom Val)
forall {a} {b}. Lens (a, b) b
_2 ((Dom Val -> Dom Val)
 -> (TypeError, Dom Val) -> (TypeError, Dom Val))
-> (Dom Val -> Dom Val)
-> (TypeError, Dom Val)
-> (TypeError, Dom Val)
forall a b. (a -> b) -> a -> b
$ Lens (Dom Val) ArgInfo
-> (ArgInfo -> ArgInfo) -> Dom Val -> Dom Val
forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over Lens (Dom Val) ArgInfo
forall a. Lens (Dom a) ArgInfo
domInfo ((ArgInfo -> ArgInfo) -> Dom Val -> Dom Val)
-> (ArgInfo -> ArgInfo) -> Dom Val -> Dom Val
forall a b. (a -> b) -> a -> b
$ ArgInfo -> ArgInfo
resSI
    where
    resSI :: ArgInfo -> ArgInfo
resSI = \case
      ArgInfo
ShapeIrr -> ArgInfo
Relevant
      ArgInfo
r -> ArgInfo
r

-- * Subtyping and type equality

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

equalType :: Val -> Val -> Check ()
equalType :: Val -> Val -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
equalType Val
v Val
v' = do
  Type
t  <- Val -> Check Type
reifyType Val
v
  Type
t' <- Val -> Check Type
reifyType Val
v'
  Bool
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
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 TypeError)) ()
 -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ())
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
forall a b. (a -> b) -> a -> b
$
    TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
forall a.
TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ())
-> TypeError -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
forall a b. (a -> b) -> a -> b
$ TypeError
"Inferred type " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ Type -> TypeError
forall a. Show a => a -> TypeError
show Type
t TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
" is not equal to expected type " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ Type -> TypeError
forall a. Show a => a -> TypeError
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 :: Val -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
admissible Val
v = do
  Int
k <- Cxt -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Cxt -> Int)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) Cxt
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Cxt)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) Cxt
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt
  (TypeError, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
forall b. (TypeError, Val) -> Check b -> Check b
forall a b. AddContext a => a -> Check b -> Check b
addContext (TypeError
"i", Val
VSize) (ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
 -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ())
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
forall a b. (a -> b) -> a -> b
$ do
    Val
va <- ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
lastVal
    (TypeError, Val)
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
forall b. (TypeError, Val) -> Check b -> Check b
forall a b. AddContext a => a -> Check b -> Check b
addContext (TypeError
"x", Val -> Val
VNat (Val -> Val) -> Val -> Val
forall a b. (a -> b) -> a -> b
$ Val
va) (ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
 -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ())
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
-> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
forall a b. (a -> b) -> a -> b
$ do
      Val
u  <- ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
lastVal
      Val
t1  <- Val
-> [Arg Val] -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
applyArgs Val
v [ ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
ShapeIrr Val
va, ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant Val
u]
      Val
t2  <- Val
-> [Arg Val] -> ReaderT TCEnv (StateT TCSt (Except TypeError)) Val
applyArgs Val
v [ ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
ShapeIrr Val
VInfty, ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant Val
u]
      Val -> Val -> ReaderT TCEnv (StateT TCSt (Except TypeError)) ()
subType Val
t1 Val
t2

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

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

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

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

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

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

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

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

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