{-# 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 = forall e a. Except e a -> Either e a
runExcept (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ([Decl] -> Check ()
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 = forall k a. Map k a
Map.empty , _stDefs :: Map TypeError Val
_stDefs = forall k a. Map k a
Map.empty }

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

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

-- | Check a type signature.

checkSig :: A.Ident -> A.Exp -> Check ()
checkSig :: Ident -> Exp -> Check ()
checkSig x0 :: Ident
x0@(A.Ident TypeError
x) Exp
a = forall a b. Print a => a -> b -> b
traceCheck (Ident -> Exp -> Decl
A.Sig Ident
x0 Exp
a) 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
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Maybe a -> Bool
isNothing Maybe Val
mt) forall a b. (a -> b) -> a -> b
$
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"Duplicate type signature for " 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 -> Check ()
addTySig TypeError
x forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Check Val
evaluate Type
t

-- | Check a definition.

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

  -- Check that x has a signature
  let noSig :: ReaderT TCEnv (StateT TCSt (Except TypeError)) a
noSig = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"Missing type signature for " forall a. [a] -> [a] -> [a]
++ TypeError
x
  Val
t <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall {a}. ReaderT TCEnv (StateT TCSt (Except TypeError)) a
noSig forall (m :: * -> *) a. Monad m => a -> m a
return 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
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Maybe a -> Bool
isNothing Maybe Val
mv) forall a b. (a -> b) -> a -> b
$
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"Duplicate definition of " 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 -> Check ()
addDef TypeError
x forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Check Val
evaluate Type
v

-- | Check well-formedness of a type.

checkType :: A.Exp -> Check Type
checkType :: Exp -> Check Type
checkType Exp
e = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> Check (Type, Val)
inferType Exp
e

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

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

    -- Universes (shape irrelevant)

    Exp
A.Set  -> forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
Type Type
sZero, Int -> Val
vsConst Int
1)
    Exp
A.Set1 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
Type forall a b. (a -> b) -> a -> b
$ Type -> Type
sSuc Type
sZero, Int -> Val
vsConst Int
2)
    Exp
A.Set2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
Type forall a b. (a -> b) -> a -> b
$ Type -> Type
sSuc 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 <- forall a. ArgInfo -> Check a -> Check a
resurrect ArgInfo
ShapeIrr forall a b. (a -> b) -> a -> b
$ Exp -> Check Type
checkLevel Exp
l
      Val
v <- Type -> Check Val
evaluate Type
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 <- forall a. ArgInfo -> Check a -> Check a
resurrect ArgInfo
ShapeIrr forall a b. (a -> b) -> a -> b
$ Exp -> Check Type
checkSize Exp
s
      Val
v <- Type -> Check Val
evaluate Type
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 -> Check (Type, Val)
inferType Exp
a
      (Type
t, Val
l2) <- Exp -> Check (Type, Val)
inferType Exp
b
      forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type -> Abs Type -> Type
Pi (forall a. a -> Dom a
defaultDom Type
u) (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 = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"Expected list of identifiers, found " forall a. [a] -> [a] -> [a]
++ forall a. Print a => a -> TypeError
printTree Exp
e
      [IdU]
xs <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall {a}. ReaderT TCEnv (StateT TCSt (Except TypeError)) a
failure forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Exp -> Maybe [IdU]
parseIdUs Exp
e
      [(IdU, Dom Exp)] -> Check (Type, Val) -> Check (Type, Val)
inferPisType (forall a b. (a -> b) -> [a] -> [b]
map (, forall a. a -> Dom a
defaultDom Exp
a) [IdU]
xs) forall a b. (a -> b) -> a -> b
$ Exp -> Check (Type, Val)
inferType Exp
b

    A.Forall [Bind]
bs Exp
c -> [(IdU, Dom Exp)] -> Check (Type, Val) -> Check (Type, Val)
inferPisType (Bind -> [(IdU, Dom Exp)]
fromBind forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Bind]
bs) forall a b. (a -> b) -> a -> b
$ Exp -> Check (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  -> forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> IdU
A.Id Ident
x, forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
Irrelevant Exp
A.Size)
        A.BRel   Ident
x  -> forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> IdU
A.Id Ident
x, forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
ShapeIrr   Exp
A.Size)
        A.BAnn [Ident]
xs Exp
a -> forall a b. (a -> b) -> [a] -> [b]
map (\ Ident
x -> (Ident -> IdU
A.Id Ident
x, forall a. a -> Dom a
defaultDom Exp
a)) [Ident]
xs

    -- Neutral types

    Exp
e | Exp -> Bool
A.introduction Exp
e -> forall {a}. ReaderT TCEnv (StateT TCSt (Except TypeError)) a
invalidType

    Exp
e -> do
      (Type
t,Val
v) <- Exp -> Check (Type, Val)
inferExp Exp
e
      case Val
v of
        VType Val
l -> forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t,Val
l)
        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)] -> Check (Type, Val) -> Check (Type, Val)
inferPisType = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry IdU -> Dom Exp -> Check (Type, Val) -> Check (Type, Val)
inferPiType)

inferPiType :: A.IdU -> Dom A.Exp -> Check (Type, VLevel) -> Check (Type, VLevel)
inferPiType :: IdU -> Dom Exp -> Check (Type, Val) -> Check (Type, Val)
inferPiType IdU
x Dom Exp
dom Check (Type, Val)
cont = do

  -- Check the domain
  (Type
u, Val
l1) <- Exp -> Check (Type, Val)
inferType forall a b. (a -> b) -> a -> b
$ forall a. Dom a -> a
unDom Dom Exp
dom

  -- Check the codomain in the extended context.
  Val
v <- Type -> Check Val
evaluate Type
u
  forall a b. AddContext a => a -> Check b -> Check b
addContext (IdU
x, Val
v) forall a b. (a -> b) -> a -> b
$ do
    (Type
t, Val
l2) <- Check (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 forall a. a -> Maybe a -> a
fromMaybe __IMPOSSIBLE__ $ sizeView l0 of
      SVVar Int
k' Int
_ -> do
        Int
k <- forall (t :: * -> *) a. Foldable t => t a -> Int
length forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Int
k' forall a. Ord a => a -> a -> Bool
>= Int
k then Val
VInfty else Val
l0
      SizeView
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Val
l0

    -- Construct the function type
    forall (m :: * -> *) a. Monad m => a -> m a
return ( Dom Type -> Abs Type -> Type
Pi (Dom Exp
dom forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
u) forall a b. (a -> b) -> a -> b
$ 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        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
sZero
  A.App Exp
A.LSuc Exp
e -> Type -> Type
sSuc 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 -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"Not a valid level expression: " forall a. [a] -> [a] -> [a]
++ 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 -> forall a b. AddContext a => a -> Check b -> Check b
addContext (IdU
x, Dom Val
dom) forall a b. (a -> b) -> a -> b
$ do
          Val
t' <- VClos -> Val -> Check Val
applyClosure VClos
cl forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Check Val
lastVal
          Type
u  <- Exp -> Val -> Check Type
checkExp ([IdU] -> Exp -> Exp
A.Lam [IdU]
xs Exp
e) Val
t'
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Type -> Type
Lam (forall a. Dom a -> ArgInfo
_domInfo Dom Val
dom) forall a b. (a -> b) -> a -> b
$ forall a. TypeError -> a -> Abs a
Abs (IdU -> TypeError
fromIdU IdU
x) Type
u
        Val
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"Lambda abstraction expects function type, but got " forall a. [a] -> [a] -> [a]
++ 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
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ArgInfo
r forall a. Eq a => a -> a -> Bool
== ArgInfo
Relevant) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
            TypeError
"Extended lambda constructs relevant function: " forall a. [a] -> [a] -> [a]
++ 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 = 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VClos -> Val -> Check Val
applyClosure VClos
cl (Val -> Val
VZero Val
a)
          (Type
ts0, Type
tS0) <-
            forall a b. AddContext a => a -> Check b -> Check b
addContext (TypeError
x, forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
Relevant forall a b. (a -> b) -> a -> b
$ Val -> Val
VNat Val
a) forall a b. (a -> b) -> a -> b
$ do
              Val
vts <- VClos -> Val -> Check Val
applyClosure VClos
cl forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do Val -> Val -> Val
VSuc Val
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Check Val
lastVal
              Type
tS0 <- Val -> Check Type
reifyType Val
vts
              (,Type
tS0) 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 forall a b. (a -> b) -> a -> b
$ forall a. TypeError -> a -> Abs a
Abs TypeError
x Type
ts0
          let tS :: Type
tS = Dom Type -> Abs Type -> Type
Pi (forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
Relevant forall a b. (a -> b) -> a -> b
$ Type -> Type
Nat Type
ta) forall a b. (a -> b) -> a -> b
$ forall a. TypeError -> a -> Abs a
Abs TypeError
x Type
tS0
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Type -> Type
Lam ArgInfo
Relevant forall a b. (a -> b) -> a -> b
$ forall a. TypeError -> a -> Abs a
Abs TypeError
"x" forall a b. (a -> b) -> a -> b
$ Type -> Elim -> Type
App (Index -> Type
Var Index
0) forall a b. (a -> b) -> a -> b
$ forall a. Substitute a => Int -> a -> a
raise Int
1 forall a b. (a -> b) -> a -> b
$
            forall a. a -> a -> a -> a -> Elim' a
Case Type
tt Type
tz Type
tS Type
ts

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

    Exp
e -> do
      (Type
u, Val
ti) <- Exp -> Check (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 -> Check (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 -> Check (Type, Val)
inferType Exp
e
    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 <- forall a. ArgInfo -> Check a -> Check a
resurrect ArgInfo
Irrelevant forall a b. (a -> b) -> a -> b
$ Exp -> Check Type
checkSize Exp
ea
        (Type -> Type
zero Type
a ,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Val -> Val
VNat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Val -> Val
vsSuc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Check Val
evaluate Type
a
      [Exp]
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"zero expects exactly 1 argument: " forall a. [a] -> [a] -> [a]
++ 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 <- forall a. ArgInfo -> Check a -> Check a
resurrect ArgInfo
Irrelevant forall a b. (a -> b) -> a -> b
$ Exp -> Check Type
checkSize Exp
ea
        Val
va <- Type -> Check Val
evaluate Type
a
        Type
n <- Exp -> Val -> Check Type
checkExp Exp
en forall a b. (a -> b) -> a -> b
$ Val -> Val
VNat Val
va
        forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
suc Type
a Type
n, Val -> Val
VNat forall a b. (a -> b) -> a -> b
$ Val -> Val
vsSuc Val
va)
      [Exp]
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"suc expects exactly 2 arguments: " forall a. [a] -> [a] -> [a]
++ 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Check Val
evaluate Type
tF
        -- Check the argument
        (Type
tn, Val
a) <- Exp -> Check (Type, Val)
inferNat Exp
en
        -- Compute the type of the elimination
        Val
vT <- Type -> Check Val
evaluate Type
tT
        Val -> Check ()
admissible Val
vT
        Val
vn <- Type -> Check Val
evaluate Type
tn
        Val
ve <- Val -> [Arg Val] -> Check Val
applyArgs Val
vT [ forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
ShapeIrr Val
a , forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant Val
vn ]
        -- Return as postfix application
        forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Elim -> Type
App Type
tn forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> a -> Elim' a
Fix Type
tT Type
tF Type
tf, Val
ve)

      [Exp]
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"fix expects exactly 3 arguments: " forall a. [a] -> [a] -> [a]
++ forall a. Print a => a -> TypeError
printTree Exp
e

  (Exp
A.Infty, (Exp, [Exp])
_) -> 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
    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])
_) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TypeError
"Illegal expression: _"
  (A.Var (A.Id Ident
x), (Exp, [Exp])
_) -> Ident -> Check (Type, Val)
inferId Ident
x

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


  (A.Case{}, (Exp, [Exp])
_)  -> forall a. TypeError -> Check a
nyi TypeError
"case"

  (Exp
e, (Exp, [Exp])
_) -> forall a. TypeError -> Check a
nyi forall a b. (a -> b) -> a -> b
$ TypeError
"inferring type of " forall a. [a] -> [a] -> [a]
++ forall a. Print a => a -> TypeError
printTree Exp
e

-- | Infer type of a variable

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

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

inferNat :: A.Exp -> Check (Term, VSize)
inferNat :: Exp -> Check (Type, Val)
inferNat Exp
e = do
  (Type
u,Val
t) <- Exp -> Check (Type, Val)
inferExp Exp
e
  case Val
t of
    VNat Val
a -> forall (m :: * -> *) a. Monad m => a -> m a
return (Type
u, Val
a)
    Val
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"Expected natural number, but found " forall a. [a] -> [a] -> [a]
++ 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 -> Check ()
subType Val
ti Val
tc
  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 = forall a. TypeError -> a -> a
trace forall a b. (a -> b) -> a -> b
$ TypeError
"Checking " forall a. [a] -> [a] -> [a]
++ forall a. Print a => a -> TypeError
printTree a
a

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

-- | Signature auxiliary functions

lookupTySig :: Id -> Check (Maybe VType)
lookupTySig :: TypeError -> Check (Maybe Val)
lookupTySig TypeError
x = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TypeError
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TypeError
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 -> Check ()
addTySig TypeError
x Val
t = Lens TCSt (Map TypeError Val)
stTySigs forall a (m :: * -> *) b.
MonadState a m =>
Lens a b -> (b -> b) -> m ()
%= 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 -> Check ()
addDef TypeError
x Val
v = Lens TCSt (Map TypeError Val)
stDefs forall a (m :: * -> *) b.
MonadState a m =>
Lens a b -> (b -> b) -> m ()
%= 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 = forall a. a -> Maybe a -> a
fromMaybe __IMPOSSIBLE__ . Map.lookup x <$> ask

evaluate :: Term -> Check Val
evaluate :: Type -> Check Val
evaluate Type
t = do
  Map TypeError Val
sig   <- forall {a} {m :: * -> *} {b}. MonadState a m => Lens a b -> m b
use Lens TCSt (Map TypeError Val)
stDefs
  Env
delta <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Env
_envEnv
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r a. Reader r a -> r -> a
runReader (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 -> Check Val
applyClosure VClos
cl Val
v =
  forall r a. Reader r a -> r -> a
runReader (forall (m :: * -> *). MonadEval m => VClos -> Val -> m Val
applyClos VClos
cl Val
v) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 -> Check Val
applyElims Val
v VElims
es =
  forall r a. Reader r a -> r -> a
runReader (forall (m :: * -> *). MonadEval m => Val -> VElims -> m Val
applyEs Val
v VElims
es) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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] -> Check Val
applyArgs Val
v = Val -> VElims -> Check Val
applyElims Val
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply

reifyType :: VType -> Check Type
reifyType :: Val -> Check Type
reifyType Val
t = do
  Int
n <- forall (t :: * -> *) a. Foldable t => t a -> Int
length forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt
  Map TypeError Val
sig <- forall {a} {m :: * -> *} {b}. MonadState a m => Lens a b -> m b
use Lens TCSt (Map TypeError Val)
stDefs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r a. Reader r a -> r -> a
runReader (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (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 <- forall (t :: * -> *) a. Foldable t => t a -> Int
length forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCEnv -> Cxt
_envCxt
  Map TypeError Val
sig <- forall {a} {m :: * -> *} {b}. MonadState a m => Lens a b -> m b
use Lens TCSt (Map TypeError Val)
stDefs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r a. Reader r a -> r -> a
runReader (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (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 = 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
    [] -> forall a. Maybe a
Nothing
    ((TypeError
y,b
t) : [(TypeError, b)]
cxt)
      | TypeError
x forall a. Eq a => a -> a -> Bool
== TypeError
y    -> forall a. a -> Maybe a
Just (t
i,b
t)
      | Bool
otherwise -> t -> [(TypeError, b)] -> Maybe (t, b)
loop (forall a. Enum a => a -> a
succ t
i) [(TypeError, b)]
cxt


-- | Value of last variable added to context.

lastVal :: Check Val
lastVal :: Check Val
lastVal = forall a. [a] -> a
head forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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) = 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) = 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) = 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 -> Check Val
evaluate Type
t
    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) = forall a b. AddContext a => a -> Check b -> Check b
addContext (TypeError
x, 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) = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local
    forall a b. (a -> b) -> a -> b
$ forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over Lens TCEnv Cxt
envCxt ((TypeError
x,Dom Val
t)forall a. a -> [a] -> [a]
:)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall a. Dom a -> a
unDom Dom Val
t) (forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
delta) 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   -> forall a. a -> a
id
  -- Irrelevant application: resurrect everything.
  ArgInfo
Irrelevant -> forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over Lens TCEnv Cxt
envCxt forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over forall {a} {b}. Lens (a, b) b
_2 forall a b. (a -> b) -> a -> b
$ forall {a} {b}. Lens a b -> b -> a -> a
set forall a. Lens (Dom a) ArgInfo
domInfo ArgInfo
Relevant
  -- Shape irrelevant application: resurrect shape-irrelevant variables.
  ArgInfo
ShapeIrr   -> forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over Lens TCEnv Cxt
envCxt forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over forall {a} {b}. Lens (a, b) b
_2 forall a b. (a -> b) -> a -> b
$ forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over forall a. Lens (Dom a) ArgInfo
domInfo 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 -> Check ()
subType Val
ti Val
tc = do
  let failure :: ReaderT TCEnv (StateT TCSt (Except TypeError)) a
failure = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TypeError
"Subtyping failed: type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TypeError
show Val
ti
        forall a. [a] -> [a] -> [a]
++ TypeError
" is not a subtype of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TypeError
show Val
tc
  case (Val
ti, Val
tc) of
    (VNat  Val
a, VNat  Val
b) -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Val -> Val -> Bool
leqSize Val
a Val
b) forall {a}. ReaderT TCEnv (StateT TCSt (Except TypeError)) a
failure
    (VType Val
a, VType Val
b) -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Val -> Val -> Bool
leqSize Val
a Val
b) forall {a}. ReaderT TCEnv (StateT TCSt (Except TypeError)) a
failure
    (VPi Dom Val
dom1 VClos
cl1, VPi Dom Val
dom2 VClos
cl2) -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Dom a -> ArgInfo
_domInfo Dom Val
dom2 forall a. Ord a => a -> a -> Bool
<= forall a. Dom a -> ArgInfo
_domInfo Dom Val
dom1) forall {a}. ReaderT TCEnv (StateT TCSt (Except TypeError)) a
failure
      Val -> Val -> Check ()
subType (forall a. Dom a -> a
unDom Dom Val
dom2) (forall a. Dom a -> a
unDom Dom Val
dom1)
      forall a b. AddContext a => a -> Check b -> Check b
addContext (forall a. Abs a -> TypeError
absName forall a b. (a -> b) -> a -> b
$ VClos -> Abs Type
closBody VClos
cl2, Dom Val
dom2) forall a b. (a -> b) -> a -> b
$ do
        Val
v  <- Check Val
lastVal
        Val
b1 <- VClos -> Val -> Check Val
applyClosure VClos
cl1 Val
v
        Val
b2 <- VClos -> Val -> Check Val
applyClosure VClos
cl2 Val
v
        Val -> Val -> Check ()
subType Val
b1 Val
b2
    (Val, Val)
_ -> Val -> Val -> Check ()
equalType Val
ti Val
tc

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

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

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

debug :: String -> VGen -> VType -> Check ()
debug :: TypeError -> Int -> Val -> Check ()
debug TypeError
txt Int
k Val
tv = do
    Type
a <- Val -> Check Type
reifySize forall a b. (a -> b) -> a -> b
$ Int -> Val
vsVar Int
k
    Type
t <- Val -> Check Type
reifyType Val
tv
    forall (f :: * -> *). Applicative f => TypeError -> f ()
traceM forall a b. (a -> b) -> a -> b
$ TypeError
txt forall a. [a] -> [a] -> [a]
++ TypeError
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TypeError
show Type
a forall a. [a] -> [a] -> [a]
++ TypeError
"  " forall a. [a] -> [a] -> [a]
++ 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 -> Check ()
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 forall a b. (a -> b) -> a -> b
$ forall a. Dom a -> a
unDom Dom Val
dom
      forall a b. AddContext a => a -> Check b -> Check b
addContext (forall a. Abs a -> TypeError
absName forall a b. (a -> b) -> a -> b
$ VClos -> Abs Type
closBody VClos
cl, Dom Val
dom) forall a b. (a -> b) -> a -> b
$ do
        Val
v <- Check Val
lastVal
        Int -> Val -> Check Bool
upperSemi Int
k forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VClos -> Val -> Check Val
applyClosure VClos
cl Val
v
    VType{}         -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Val
VSize           -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VNat{}          -> 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
     forall (f :: * -> *). Applicative f => TypeError -> f ()
traceM forall a b. (a -> b) -> a -> b
$ TypeError
"upperSemi " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TypeError
show Int
k forall a. [a] -> [a] -> [a]
++ TypeError
"  " forall a. [a] -> [a] -> [a]
++ 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 -> Check ()
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{}         -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Val
VSize           -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VNat{}          -> 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
     forall (f :: * -> *). Applicative f => TypeError -> f ()
traceM forall a b. (a -> b) -> a -> b
$ TypeError
"lowerSemi " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TypeError
show Int
k forall a. [a] -> [a] -> [a]
++ TypeError
"  " forall a. [a] -> [a] -> [a]
++ 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 -> Check ()
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) forall a b. (a -> b) -> a -> b
$ forall a. Dom a -> a
unDom Dom Val
dom
      forall a b. AddContext a => a -> Check b -> Check b
addContext (forall a. Abs a -> TypeError
absName forall a b. (a -> b) -> a -> b
$ VClos -> Abs Type
closBody VClos
cl, Dom Val
dom) forall a b. (a -> b) -> a -> b
$ do
        Val
u <- Check Val
lastVal
        Int -> Bool -> Val -> Check Bool
monotone Int
k Bool
b forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VClos -> Val -> Check 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   -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VUp (VType Val
_) VNe
_ -> 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 -> Check ()
debugSize (if Bool
b then TypeError
"monotone" else TypeError
"antitone") Int
k Val
t
  case Val
t of
    Val
VInfty  -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    VZero Val
_ -> 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 forall a. Eq a => a -> a -> Bool
== Int
k'   -> do
          forall (f :: * -> *). Applicative f => TypeError -> f ()
traceM forall a b. (a -> b) -> a -> b
$ TypeError
"same var"
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TypeError
"admissibility check failed"
          forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
      | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Val
_ -> __IMPOSSIBLE__

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