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

-- | Values and weak head evaluation

module Evaluation where

import Control.Applicative
import Control.Monad
import Control.Monad.Identity
import Control.Monad.Reader

import Data.Maybe
import Data.Traversable (traverse)

import Debug.Trace

import Internal
import Substitute

import Lens
import Impossible
#include "undefined.h"

-- * Values

-- | Generic values are de Bruijn levels.
type VGen   = Int

-- | We have just a single type of values, including size values.
type VSize  = Val
type VLevel = VSize

type VType  = Val
type VElim  = Elim' Val
type VElims = [VElim]

data Val
  = VType VLevel
  | VSize
  | VNat VSize
  | VZero VSize
  | VSuc VSize Val
  | VInfty
  | VPi (Dom VType) VClos
  | -- | Lambda abstraction
    VLam VClos
  | -- | @\ x -> x e@ for internal use in fix.
    VElimBy VElim
  | -- | Neutrals.
    VUp VType VNe
  | -- | Type annotation for readback (normal form).
    VDown VType Val
  deriving (VSize -> VSize -> Bool
(VSize -> VSize -> Bool) -> (VSize -> VSize -> Bool) -> Eq VSize
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VSize -> VSize -> Bool
== :: VSize -> VSize -> Bool
$c/= :: VSize -> VSize -> Bool
/= :: VSize -> VSize -> Bool
Eq, Int -> VSize -> ShowS
[VSize] -> ShowS
VSize -> String
(Int -> VSize -> ShowS)
-> (VSize -> String) -> ([VSize] -> ShowS) -> Show VSize
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VSize -> ShowS
showsPrec :: Int -> VSize -> ShowS
$cshow :: VSize -> String
show :: VSize -> String
$cshowList :: [VSize] -> ShowS
showList :: [VSize] -> ShowS
Show)

data VNe = VNe
  { VNe -> Int
_neVar :: VGen
  , VNe -> VElims
_neElims :: VElims
  }
  deriving (VNe -> VNe -> Bool
(VNe -> VNe -> Bool) -> (VNe -> VNe -> Bool) -> Eq VNe
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VNe -> VNe -> Bool
== :: VNe -> VNe -> Bool
$c/= :: VNe -> VNe -> Bool
/= :: VNe -> VNe -> Bool
Eq, Int -> VNe -> ShowS
[VNe] -> ShowS
VNe -> String
(Int -> VNe -> ShowS)
-> (VNe -> String) -> ([VNe] -> ShowS) -> Show VNe
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VNe -> ShowS
showsPrec :: Int -> VNe -> ShowS
$cshow :: VNe -> String
show :: VNe -> String
$cshowList :: [VNe] -> ShowS
showList :: [VNe] -> ShowS
Show)

data VClos = VClos
  { VClos -> Abs Term
closBody :: Abs Term
  , VClos -> [VSize]
closEnv  :: Env
  }
  deriving (VClos -> VClos -> Bool
(VClos -> VClos -> Bool) -> (VClos -> VClos -> Bool) -> Eq VClos
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VClos -> VClos -> Bool
== :: VClos -> VClos -> Bool
$c/= :: VClos -> VClos -> Bool
/= :: VClos -> VClos -> Bool
Eq, Int -> VClos -> ShowS
[VClos] -> ShowS
VClos -> String
(Int -> VClos -> ShowS)
-> (VClos -> String) -> ([VClos] -> ShowS) -> Show VClos
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VClos -> ShowS
showsPrec :: Int -> VClos -> ShowS
$cshow :: VClos -> String
show :: VClos -> String
$cshowList :: [VClos] -> ShowS
showList :: [VClos] -> ShowS
Show)

-- | An environment maps de Bruijn indices to values.
--   The first entry in the list is the binding for index 0.

type Env = [Val]

makeLens ''VNe

-- | Variable

vVar :: VType -> VGen -> Val
vVar :: VSize -> Int -> VSize
vVar VSize
t Int
x = VSize -> VNe -> VSize
VUp VSize
t (VNe -> VSize) -> VNe -> VSize
forall a b. (a -> b) -> a -> b
$ Int -> VElims -> VNe
VNe Int
x []

-- * Size arithmetic

-- | Zero size.

vsZero :: VSize
vsZero :: VSize
vsZero = VSize -> VSize
VZero VSize
VInfty

-- | Successor size.

vsSuc :: VSize -> VSize
vsSuc :: VSize -> VSize
vsSuc = VSize -> VSize -> VSize
VSuc VSize
VInfty

-- | Variable size.

vsVar :: VGen -> VSize
vsVar :: Int -> VSize
vsVar = VSize -> Int -> VSize
vVar VSize
VSize

-- | Size increment.

vsPlus :: Int -> VSize -> VSize
vsPlus :: Int -> VSize -> VSize
vsPlus Int
n VSize
v = (VSize -> VSize) -> VSize -> [VSize]
forall a. (a -> a) -> a -> [a]
iterate VSize -> VSize
vsSuc VSize
v [VSize] -> Int -> VSize
forall a. HasCallStack => [a] -> Int -> a
!! Int
n

-- | Constant size.

vsConst :: Int -> VSize
vsConst :: Int -> VSize
vsConst Int
n = Int -> VSize -> VSize
vsPlus Int
n VSize
vsZero

-- | View a value as a size expression.

data SizeView
  = SVConst Int
    -- ^ @n@
  | SVVar VGen Int
    -- ^ @i + n@
  | SVInfty
    -- ^ @oo@
  deriving (SizeView -> SizeView -> Bool
(SizeView -> SizeView -> Bool)
-> (SizeView -> SizeView -> Bool) -> Eq SizeView
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SizeView -> SizeView -> Bool
== :: SizeView -> SizeView -> Bool
$c/= :: SizeView -> SizeView -> Bool
/= :: SizeView -> SizeView -> Bool
Eq, Int -> SizeView -> ShowS
[SizeView] -> ShowS
SizeView -> String
(Int -> SizeView -> ShowS)
-> (SizeView -> String) -> ([SizeView] -> ShowS) -> Show SizeView
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SizeView -> ShowS
showsPrec :: Int -> SizeView -> ShowS
$cshow :: SizeView -> String
show :: SizeView -> String
$cshowList :: [SizeView] -> ShowS
showList :: [SizeView] -> ShowS
Show)

-- | Successor size on view.

svSuc :: SizeView -> SizeView
svSuc :: SizeView -> SizeView
svSuc = \case
  SVConst Int
n -> Int -> SizeView
SVConst (Int -> SizeView) -> Int -> SizeView
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Enum a => a -> a
succ Int
n
  SVVar Int
x Int
n -> Int -> Int -> SizeView
SVVar Int
x (Int -> SizeView) -> Int -> SizeView
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Enum a => a -> a
succ Int
n
  SizeView
SVInfty   -> SizeView
SVInfty

-- | View a value as a size expression.

sizeView :: Val -> Maybe SizeView
sizeView :: VSize -> Maybe SizeView
sizeView = \case
  VZero VSize
_              -> SizeView -> Maybe SizeView
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeView -> Maybe SizeView) -> SizeView -> Maybe SizeView
forall a b. (a -> b) -> a -> b
$ Int -> SizeView
SVConst Int
0
  VSuc VSize
_ VSize
v             -> SizeView -> SizeView
svSuc (SizeView -> SizeView) -> Maybe SizeView -> Maybe SizeView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VSize -> Maybe SizeView
sizeView VSize
v
  VSize
VInfty               -> SizeView -> Maybe SizeView
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeView -> Maybe SizeView) -> SizeView -> Maybe SizeView
forall a b. (a -> b) -> a -> b
$ SizeView
SVInfty
  VUp VSize
VSize (VNe Int
k []) -> SizeView -> Maybe SizeView
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeView -> Maybe SizeView) -> SizeView -> Maybe SizeView
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SizeView
SVVar Int
k Int
0
  VSize
_ -> Maybe SizeView
forall a. Maybe a
Nothing

unSizeView :: SizeView -> Val
unSizeView :: SizeView -> VSize
unSizeView = \case
  SizeView
SVInfty -> VSize
VInfty
  SVConst Int
n -> Int -> VSize
vsConst Int
n
  SVVar Int
x Int
n -> Int -> VSize -> VSize
vsPlus Int
n (VSize -> VSize) -> VSize -> VSize
forall a b. (a -> b) -> a -> b
$ Int -> VSize
vsVar Int
x

-- | Compute the maximum of two sizes.

maxSize :: VSize -> VSize -> VSize
maxSize :: VSize -> VSize -> VSize
maxSize VSize
v1 VSize
v2 =
  case ( SizeView -> Maybe SizeView -> SizeView
forall a. a -> Maybe a -> a
fromMaybe __IMPOSSIBLE__ $ sizeView v1
       , SizeView -> Maybe SizeView -> SizeView
forall a. a -> Maybe a -> a
fromMaybe __IMPOSSIBLE__ $ sizeView v2) of
    (SVConst Int
n, SVConst Int
m)          -> SizeView -> VSize
unSizeView (SizeView -> VSize) -> SizeView -> VSize
forall a b. (a -> b) -> a -> b
$ Int -> SizeView
SVConst (Int -> SizeView) -> Int -> SizeView
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n Int
m
    (SVVar Int
x Int
n, SVVar Int
y Int
m) | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y -> SizeView -> VSize
unSizeView (SizeView -> VSize) -> SizeView -> VSize
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SizeView
SVVar Int
x (Int -> SizeView) -> Int -> SizeView
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n Int
m
    (SVConst Int
n, SVVar Int
y Int
m) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
m -> SizeView -> VSize
unSizeView (SizeView -> VSize) -> SizeView -> VSize
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SizeView
SVVar Int
y Int
m
    (SVVar Int
x Int
n, SVConst Int
m) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
m -> SizeView -> VSize
unSizeView (SizeView -> VSize) -> SizeView -> VSize
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SizeView
SVVar Int
x Int
n
    (SizeView, SizeView)
_ -> VSize
VInfty

-- * Evaluation

-- | Evaluation monad.

class (Functor m, Applicative m, Monad m) => MonadEval m where
  getDef :: Id -> m Val

instance MonadEval Identity where
  getDef :: String -> Identity VSize
getDef String
x = __IMPOSSIBLE__

evaluateClosed :: Term -> Val
evaluateClosed :: Term -> VSize
evaluateClosed Term
t = Identity VSize -> VSize
forall a. Identity a -> a
runIdentity (Identity VSize -> VSize) -> Identity VSize -> VSize
forall a b. (a -> b) -> a -> b
$ Term -> [VSize] -> Identity VSize
forall (m :: * -> *). MonadEval m => Term -> [VSize] -> m VSize
evalIn Term
t []

-- | Evaluation.

evalIn :: MonadEval m => Term -> Env -> m Val
evalIn :: forall (m :: * -> *). MonadEval m => Term -> [VSize] -> m VSize
evalIn Term
t [VSize]
rho = ReaderT [VSize] m VSize -> [VSize] -> m VSize
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Term -> ReaderT [VSize] m VSize
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Term -> ReaderT [VSize] m VSize
eval Term
t) [VSize]
rho

class Evaluate a b where -- -- | a -> b where
  eval :: MonadEval m => a -> ReaderT Env m b

instance Evaluate Index Val where
  eval :: forall (m :: * -> *).
MonadEval m =>
Index -> ReaderT [VSize] m VSize
eval (Index Int
i) = ([VSize] -> Int -> VSize
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) ([VSize] -> VSize)
-> ReaderT [VSize] m [VSize] -> ReaderT [VSize] m VSize
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT [VSize] m [VSize]
forall r (m :: * -> *). MonadReader r m => m r
ask

instance Evaluate Term Val where
  eval :: forall (m :: * -> *).
MonadEval m =>
Term -> ReaderT [VSize] m VSize
eval = \case
    Type Term
l   -> VSize -> VSize
VType (VSize -> VSize)
-> ReaderT [VSize] m VSize -> ReaderT [VSize] m VSize
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReaderT [VSize] m VSize
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Term -> ReaderT [VSize] m VSize
eval Term
l
    Nat Term
a    -> VSize -> VSize
VNat (VSize -> VSize)
-> ReaderT [VSize] m VSize -> ReaderT [VSize] m VSize
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReaderT [VSize] m VSize
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Term -> ReaderT [VSize] m VSize
eval Term
a
    Term
Size     -> VSize -> ReaderT [VSize] m VSize
forall a. a -> ReaderT [VSize] m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VSize
VSize
    Term
Infty    -> VSize -> ReaderT [VSize] m VSize
forall a. a -> ReaderT [VSize] m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VSize
VInfty
    Zero Arg Term
a   -> VSize -> VSize
VZero (VSize -> VSize)
-> ReaderT [VSize] m VSize -> ReaderT [VSize] m VSize
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReaderT [VSize] m VSize
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Term -> ReaderT [VSize] m VSize
eval (Arg Term -> Term
forall a. Arg a -> a
unArg Arg Term
a)
    Suc Arg Term
a Term
t  -> (VSize -> VSize -> VSize)
-> ReaderT [VSize] m VSize
-> ReaderT [VSize] m VSize
-> ReaderT [VSize] m VSize
forall a b c.
(a -> b -> c)
-> ReaderT [VSize] m a
-> ReaderT [VSize] m b
-> ReaderT [VSize] m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 VSize -> VSize -> VSize
VSuc (Term -> ReaderT [VSize] m VSize
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Term -> ReaderT [VSize] m VSize
eval (Term -> ReaderT [VSize] m VSize)
-> Term -> ReaderT [VSize] m VSize
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall a. Arg a -> a
unArg Arg Term
a) (Term -> ReaderT [VSize] m VSize
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Term -> ReaderT [VSize] m VSize
eval Term
t)
    Pi Dom Term
u Abs Term
t   -> (Dom VSize -> VClos -> VSize)
-> ReaderT [VSize] m (Dom VSize)
-> ReaderT [VSize] m VClos
-> ReaderT [VSize] m VSize
forall a b c.
(a -> b -> c)
-> ReaderT [VSize] m a
-> ReaderT [VSize] m b
-> ReaderT [VSize] m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Dom VSize -> VClos -> VSize
VPi (Dom Term -> ReaderT [VSize] m (Dom VSize)
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Dom Term -> ReaderT [VSize] m (Dom VSize)
eval Dom Term
u) (Abs Term -> ReaderT [VSize] m VClos
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Abs Term -> ReaderT [VSize] m VClos
eval Abs Term
t)
    Lam ArgInfo
ai Abs Term
t -> VClos -> VSize
VLam (VClos -> VSize)
-> ReaderT [VSize] m VClos -> ReaderT [VSize] m VSize
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Term -> ReaderT [VSize] m VClos
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Abs Term -> ReaderT [VSize] m VClos
eval Abs Term
t
    Var Index
x -> Index -> ReaderT [VSize] m VSize
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Index -> ReaderT [VSize] m VSize
eval Index
x
    Def String
f -> m VSize -> ReaderT [VSize] m VSize
forall (m :: * -> *) a. Monad m => m a -> ReaderT [VSize] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VSize -> ReaderT [VSize] m VSize)
-> m VSize -> ReaderT [VSize] m VSize
forall a b. (a -> b) -> a -> b
$ String -> m VSize
forall (m :: * -> *). MonadEval m => String -> m VSize
getDef String
f
    App Term
t Elim
e -> do
      VSize
h <- Term -> ReaderT [VSize] m VSize
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Term -> ReaderT [VSize] m VSize
eval Term
t
      VElim
e <- Elim -> ReaderT [VSize] m VElim
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *).
MonadEval m =>
Elim -> ReaderT [VSize] m VElim
eval Elim
e
      m VSize -> ReaderT [VSize] m VSize
forall (m :: * -> *) a. Monad m => m a -> ReaderT [VSize] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VSize -> ReaderT [VSize] m VSize)
-> m VSize -> ReaderT [VSize] m VSize
forall a b. (a -> b) -> a -> b
$ VSize -> VElim -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> VElim -> m VSize
applyE VSize
h VElim
e

instance Evaluate (Abs Term) VClos where
  eval :: forall (m :: * -> *).
MonadEval m =>
Abs Term -> ReaderT [VSize] m VClos
eval Abs Term
t = Abs Term -> [VSize] -> VClos
VClos Abs Term
t ([VSize] -> VClos)
-> ReaderT [VSize] m [VSize] -> ReaderT [VSize] m VClos
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT [VSize] m [VSize]
forall r (m :: * -> *). MonadReader r m => m r
ask

instance Evaluate a b => Evaluate [a] [b] where
  eval :: forall (m :: * -> *). MonadEval m => [a] -> ReaderT [VSize] m [b]
eval = (a -> ReaderT [VSize] m b) -> [a] -> ReaderT [VSize] m [b]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> ReaderT [VSize] m b
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *). MonadEval m => a -> ReaderT [VSize] m b
eval

instance Evaluate a b => Evaluate (Dom a) (Dom b) where
  eval :: forall (m :: * -> *).
MonadEval m =>
Dom a -> ReaderT [VSize] m (Dom b)
eval = (a -> ReaderT [VSize] m b) -> Dom a -> ReaderT [VSize] m (Dom b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom a -> f (Dom b)
traverse a -> ReaderT [VSize] m b
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *). MonadEval m => a -> ReaderT [VSize] m b
eval

instance Evaluate a b => Evaluate (Elim' a) (Elim' b) where
  eval :: forall (m :: * -> *).
MonadEval m =>
Elim' a -> ReaderT [VSize] m (Elim' b)
eval = (a -> ReaderT [VSize] m b)
-> Elim' a -> ReaderT [VSize] m (Elim' b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
traverse a -> ReaderT [VSize] m b
forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [VSize] m b
forall (m :: * -> *). MonadEval m => a -> ReaderT [VSize] m b
eval

applyEs :: MonadEval m => Val -> VElims -> m Val
applyEs :: forall (m :: * -> *). MonadEval m => VSize -> VElims -> m VSize
applyEs VSize
v []       = VSize -> m VSize
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return VSize
v
applyEs VSize
v (VElim
e : VElims
es) = VSize -> VElim -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> VElim -> m VSize
applyE VSize
v VElim
e m VSize -> (VSize -> m VSize) -> m VSize
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (VSize -> VElims -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> VElims -> m VSize
`applyEs` VElims
es)

applyE :: MonadEval m => Val -> VElim -> m Val
applyE :: forall (m :: * -> *). MonadEval m => VSize -> VElim -> m VSize
applyE VSize
v VElim
e =
  case (VSize
v, VElim
e) of
    (VSize
_        , Apply Arg VSize
u     ) -> VSize -> Arg VSize -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> Arg VSize -> m VSize
apply VSize
v Arg VSize
u
    (VZero VSize
_  , Case VSize
_ VSize
u VSize
_ VSize
_) -> VSize -> m VSize
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return VSize
u
    (VSuc VSize
_ VSize
n , Case VSize
_ VSize
_ VSize
_ VSize
f) -> VSize -> Arg VSize -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> Arg VSize -> m VSize
apply VSize
f (Arg VSize -> m VSize) -> Arg VSize -> m VSize
forall a b. (a -> b) -> a -> b
$ VSize -> Arg VSize
forall a. a -> Arg a
defaultArg VSize
n
    (VZero VSize
a  , Fix VSize
t VSize
tf VSize
f  ) -> VSize -> VSize -> VSize -> VSize -> VSize -> m VSize
forall (m :: * -> *).
MonadEval m =>
VSize -> VSize -> VSize -> VSize -> VSize -> m VSize
unfoldFix VSize
t VSize
tf VSize
f VSize
a VSize
v
    (VSuc VSize
a VSize
n , Fix VSize
t VSize
tf VSize
f  ) -> VSize -> VSize -> VSize -> VSize -> VSize -> m VSize
forall (m :: * -> *).
MonadEval m =>
VSize -> VSize -> VSize -> VSize -> VSize -> m VSize
unfoldFix VSize
t VSize
tf VSize
f VSize
a VSize
v
    (VUp (VNat VSize
a) VNe
n , VElim
_)      -> VSize -> VNe -> VElim -> m VSize
forall (m :: * -> *).
MonadEval m =>
VSize -> VNe -> VElim -> m VSize
elimNeNat VSize
a VNe
n VElim
e
    (VSize, VElim)
_ -> __IMPOSSIBLE__

-- | Apply a function to an argument.

apply :: MonadEval m => Val -> Arg Val -> m Val
apply :: forall (m :: * -> *). MonadEval m => VSize -> Arg VSize -> m VSize
apply VSize
v arg :: Arg VSize
arg@(Arg ArgInfo
ai VSize
u) = case VSize
v of
  VPi Dom VSize
_ VClos
cl  -> VClos -> VSize -> m VSize
forall (m :: * -> *). MonadEval m => VClos -> VSize -> m VSize
applyClos VClos
cl VSize
u  -- we also allow instantiation of Pi-types by apply
  VLam VClos
cl   -> VClos -> VSize -> m VSize
forall (m :: * -> *). MonadEval m => VClos -> VSize -> m VSize
applyClos VClos
cl VSize
u
  VElimBy VElim
e -> VSize -> VElim -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> VElim -> m VSize
applyE VSize
u VElim
e
  -- VConst f  -> return f
  VUp (VPi Dom VSize
a VClos
b) (VNe Int
x VElims
es) -> do
    VSize
t' <- VClos -> VSize -> m VSize
forall (m :: * -> *). MonadEval m => VClos -> VSize -> m VSize
applyClos VClos
b VSize
u
    VSize -> m VSize
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (VSize -> m VSize) -> VSize -> m VSize
forall a b. (a -> b) -> a -> b
$ VSize -> VNe -> VSize
VUp VSize
t' (VNe -> VSize) -> VNe -> VSize
forall a b. (a -> b) -> a -> b
$ Int -> VElims -> VNe
VNe Int
x (VElims -> VNe) -> VElims -> VNe
forall a b. (a -> b) -> a -> b
$ VElims
es VElims -> VElims -> VElims
forall a. [a] -> [a] -> [a]
++ [ Arg VSize -> VElim
forall a. Arg a -> Elim' a
Apply (Arg VSize -> VElim) -> Arg VSize -> VElim
forall a b. (a -> b) -> a -> b
$ ArgInfo -> VSize -> Arg VSize
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
ai (VSize -> Arg VSize) -> VSize -> Arg VSize
forall a b. (a -> b) -> a -> b
$ VSize -> VSize -> VSize
VDown (Dom VSize -> VSize
forall a. Dom a -> a
unDom Dom VSize
a) VSize
u ]
  VSize
_ -> do
    String -> m ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"apply  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VSize -> String
forall a. Show a => a -> String
show VSize
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"  to  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VSize -> String
forall a. Show a => a -> String
show VSize
u
    __IMPOSSIBLE__

-- | Apply a closure to a value.

applyClos :: MonadEval m => VClos -> Val -> m Val
applyClos :: forall (m :: * -> *). MonadEval m => VClos -> VSize -> m VSize
applyClos (VClos Abs Term
b [VSize]
rho) VSize
u = case Abs Term
b of
  NoAbs String
_ Term
t -> Term -> [VSize] -> m VSize
forall (m :: * -> *). MonadEval m => Term -> [VSize] -> m VSize
evalIn Term
t [VSize]
rho
  Abs   String
_ Term
t -> Term -> [VSize] -> m VSize
forall (m :: * -> *). MonadEval m => Term -> [VSize] -> m VSize
evalIn Term
t ([VSize] -> m VSize) -> [VSize] -> m VSize
forall a b. (a -> b) -> a -> b
$ VSize
u VSize -> [VSize] -> [VSize]
forall a. a -> [a] -> [a]
: [VSize]
rho

-- | Unfold a fixed-point.

unfoldFix :: MonadEval m => VType -> VType -> Val -> VSize -> Val -> m Val
unfoldFix :: forall (m :: * -> *).
MonadEval m =>
VSize -> VSize -> VSize -> VSize -> VSize -> m VSize
unfoldFix VSize
t VSize
tf VSize
f VSize
a VSize
v = VSize -> VElims -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> VElims -> m VSize
applyEs VSize
f (VElims -> m VSize) -> VElims -> m VSize
forall a b. (a -> b) -> a -> b
$ (Arg VSize -> VElim) -> [Arg VSize] -> VElims
forall a b. (a -> b) -> [a] -> [b]
map Arg VSize -> VElim
forall a. Arg a -> Elim' a
Apply
  [ ArgInfo -> VSize -> Arg VSize
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Irrelevant VSize
a
  , VSize -> Arg VSize
forall a. a -> Arg a
defaultArg (VSize -> Arg VSize) -> VSize -> Arg VSize
forall a b. (a -> b) -> a -> b
$ VElim -> VSize
VElimBy (VElim -> VSize) -> VElim -> VSize
forall a b. (a -> b) -> a -> b
$ VSize -> VSize -> VSize -> VElim
forall a. a -> a -> a -> Elim' a
Fix VSize
t VSize
tf VSize
f
  , VSize -> Arg VSize
forall a. a -> Arg a
defaultArg VSize
v
  ]

-- | Eliminate a neutral natural number.
--   Here we need to compute the correct type of the elimination

elimNeNat :: MonadEval m => VSize -> VNe -> VElim -> m Val
elimNeNat :: forall (m :: * -> *).
MonadEval m =>
VSize -> VNe -> VElim -> m VSize
elimNeNat VSize
a VNe
n VElim
e = case VElim
e of
  Apply{} -> __IMPOSSIBLE__

  Case VSize
t VSize
u VSize
tf VSize
f -> do
    -- Compute the type of the result of the elimination application
    VSize
tr <- VSize -> Arg VSize -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> Arg VSize -> m VSize
apply VSize
t (Arg VSize -> m VSize) -> Arg VSize -> m VSize
forall a b. (a -> b) -> a -> b
$ ArgInfo -> VSize -> Arg VSize
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant (VSize -> Arg VSize) -> VSize -> Arg VSize
forall a b. (a -> b) -> a -> b
$ VSize -> VNe -> VSize
VUp (VSize -> VSize
VNat VSize
a) VNe
n
    -- Compute the type of the zero branch
    VSize
tz <- VSize -> Arg VSize -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> Arg VSize -> m VSize
apply VSize
t (Arg VSize -> m VSize) -> Arg VSize -> m VSize
forall a b. (a -> b) -> a -> b
$ ArgInfo -> VSize -> Arg VSize
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant VSize
u
    -- Compute the type of the suc branch
    VSize
ts <- VSize -> m VSize
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return VSize
t -- TODO: must be (x : Nat a) -> t (suc a x)
    -- Assemble the elimination
    let e :: VElim
e = VSize -> VSize -> VSize -> VSize -> VElim
forall a. a -> a -> a -> a -> Elim' a
Case (VSize -> VSize -> VSize
VDown (VSize -> VSize
VType VSize
VInfty) VSize
t) (VSize -> VSize -> VSize
VDown VSize
tz VSize
u) (VSize -> VSize -> VSize
VDown (VSize -> VSize
VType VSize
VInfty) VSize
tf) (VSize -> VSize -> VSize
VDown VSize
tf VSize
f)
    -- Assemble the result
    VSize -> m VSize
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (VSize -> m VSize) -> VSize -> m VSize
forall a b. (a -> b) -> a -> b
$ VSize -> VNe -> VSize
VUp VSize
tr (VNe -> VSize) -> VNe -> VSize
forall a b. (a -> b) -> a -> b
$ Lens VNe VElims -> (VElims -> VElims) -> VNe -> VNe
forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over Lens VNe VElims
neElims (VElims -> VElims -> VElims
forall a. [a] -> [a] -> [a]
++ [VElim
e]) VNe
n

  Fix VSize
t VSize
tf VSize
f -> do
    -- Compute the type of the result of the elimination application
    VSize
tr <- VSize -> VElims -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> VElims -> m VSize
applyEs VSize
t (VElims -> m VSize) -> VElims -> m VSize
forall a b. (a -> b) -> a -> b
$ (Arg VSize -> VElim) -> [Arg VSize] -> VElims
forall a b. (a -> b) -> [a] -> [b]
map Arg VSize -> VElim
forall a. Arg a -> Elim' a
Apply [ ArgInfo -> VSize -> Arg VSize
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
ShapeIrr VSize
a, ArgInfo -> VSize -> Arg VSize
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant (VSize -> Arg VSize) -> VSize -> Arg VSize
forall a b. (a -> b) -> a -> b
$ VSize -> VNe -> VSize
VUp (VSize -> VSize
VNat VSize
a) VNe
n ]
    -- Assemble the elimination
    let e :: VElim
e = VSize -> VSize -> VSize -> VElim
forall a. a -> a -> a -> Elim' a
Fix (VSize -> VSize -> VSize
VDown VSize
fixKindV VSize
t) (VSize -> VSize -> VSize
VDown (VSize -> VSize
VType VSize
VInfty) VSize
tf) (VSize -> VSize -> VSize
VDown VSize
tf VSize
f)
    -- Assemble the result
    VSize -> m VSize
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (VSize -> m VSize) -> VSize -> m VSize
forall a b. (a -> b) -> a -> b
$ VSize -> VNe -> VSize
VUp VSize
tr (VNe -> VSize) -> VNe -> VSize
forall a b. (a -> b) -> a -> b
$ Lens VNe VElims -> (VElims -> VElims) -> VNe -> VNe
forall {a} {b}. Lens a b -> (b -> b) -> a -> a
over Lens VNe VElims
neElims (VElims -> VElims -> VElims
forall a. [a] -> [a] -> [a]
++ [VElim
e]) VNe
n

-- | Type of type of fix motive.
--   @fixKind = ..(i : Size) -> Nat i -> Setω@

fixKindV :: VType
fixKindV :: VSize
fixKindV = Term -> VSize
evaluateClosed Term
fixKind

-- * Readback

-- | Readback.

class Readback a b where
  readback :: MonadEval m => a -> ReaderT Int m b

instance Readback VGen Index where
  readback :: forall (m :: * -> *). MonadEval m => Int -> ReaderT Int m Index
readback Int
k = Int -> Index
Index (Int -> Index) -> (Int -> Int) -> Int -> Index
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ Int
n -> Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) (Int -> Index) -> ReaderT Int m Int -> ReaderT Int m Index
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT Int m Int
forall r (m :: * -> *). MonadReader r m => m r
ask

instance Readback Val Term where
  readback :: forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readback = \case
    VDown VSize
VSize     VSize
d -> VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackSize VSize
d
    VDown (VType VSize
_) VSize
d -> VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackType VSize
d
    VDown (VNat VSize
_ ) VSize
d -> VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackNat  VSize
d

    VDown (VPi Dom VSize
a VClos
b) VSize
d -> do
      VSize
v0 <- VSize -> Int -> VSize
vVar (Dom VSize -> VSize
forall a. Dom a -> a
unDom Dom VSize
a) (Int -> VSize) -> ReaderT Int m Int -> ReaderT Int m VSize
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT Int m Int
forall r (m :: * -> *). MonadReader r m => m r
ask
      VSize
c <- m VSize -> ReaderT Int m VSize
forall (m :: * -> *) a. Monad m => m a -> ReaderT Int m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VSize -> ReaderT Int m VSize) -> m VSize -> ReaderT Int m VSize
forall a b. (a -> b) -> a -> b
$ VClos -> VSize -> m VSize
forall (m :: * -> *). MonadEval m => VClos -> VSize -> m VSize
applyClos VClos
b VSize
v0
      ArgInfo -> Abs Term -> Term
Lam (Dom VSize -> ArgInfo
forall a. Dom a -> ArgInfo
_domInfo Dom VSize
a) (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
"x" (Term -> Term) -> ReaderT Int m Term -> ReaderT Int m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        (Int -> Int) -> ReaderT Int m Term -> ReaderT Int m Term
forall a. (Int -> Int) -> ReaderT Int m a -> ReaderT Int m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local Int -> Int
forall a. Enum a => a -> a
succ (ReaderT Int m Term -> ReaderT Int m Term)
-> (VSize -> ReaderT Int m Term) -> VSize -> ReaderT Int m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VSize -> ReaderT Int m Term
forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readback (VSize -> ReaderT Int m Term)
-> (VSize -> VSize) -> VSize -> ReaderT Int m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VSize -> VSize -> VSize
VDown VSize
c (VSize -> ReaderT Int m Term)
-> ReaderT Int m VSize -> ReaderT Int m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          m VSize -> ReaderT Int m VSize
forall (m :: * -> *) a. Monad m => m a -> ReaderT Int m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VSize -> ReaderT Int m VSize) -> m VSize -> ReaderT Int m VSize
forall a b. (a -> b) -> a -> b
$ VSize -> Arg VSize -> m VSize
forall (m :: * -> *). MonadEval m => VSize -> Arg VSize -> m VSize
apply VSize
d (Arg VSize -> m VSize) -> Arg VSize -> m VSize
forall a b. (a -> b) -> a -> b
$ ArgInfo -> VSize -> Arg VSize
forall a. ArgInfo -> a -> Arg a
Arg (Dom VSize -> ArgInfo
forall a. Dom a -> ArgInfo
_domInfo Dom VSize
a) VSize
v0

    VDown (VUp VSize
_ VNe
_) (VUp VSize
_ VNe
n) -> VNe -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VNe -> ReaderT Int m Term
readbackNe VNe
n

instance Readback a b => Readback [a] [b] where
  readback :: forall (m :: * -> *). MonadEval m => [a] -> ReaderT Int m [b]
readback = (a -> ReaderT Int m b) -> [a] -> ReaderT Int m [b]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> ReaderT Int m b
forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
forall (m :: * -> *). MonadEval m => a -> ReaderT Int m b
readback

instance Readback a b => Readback (Dom a) (Dom b) where
  readback :: forall (m :: * -> *). MonadEval m => Dom a -> ReaderT Int m (Dom b)
readback = (a -> ReaderT Int m b) -> Dom a -> ReaderT Int m (Dom b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom a -> f (Dom b)
traverse a -> ReaderT Int m b
forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
forall (m :: * -> *). MonadEval m => a -> ReaderT Int m b
readback

instance Readback a b => Readback (Arg a) (Arg b) where
  readback :: forall (m :: * -> *). MonadEval m => Arg a -> ReaderT Int m (Arg b)
readback = (a -> ReaderT Int m b) -> Arg a -> ReaderT Int m (Arg b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse a -> ReaderT Int m b
forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
forall (m :: * -> *). MonadEval m => a -> ReaderT Int m b
readback

instance Readback a b => Readback (Elim' a) (Elim' b) where
  readback :: forall (m :: * -> *).
MonadEval m =>
Elim' a -> ReaderT Int m (Elim' b)
readback = (a -> ReaderT Int m b) -> Elim' a -> ReaderT Int m (Elim' b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
traverse a -> ReaderT Int m b
forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
forall (m :: * -> *). MonadEval m => a -> ReaderT Int m b
readback

readbackType :: MonadEval m => Val -> ReaderT Int m Term
readbackType :: forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackType = \case
  VSize
VSize   -> Term -> ReaderT Int m Term
forall a. a -> ReaderT Int m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
Size
  VType VSize
a -> Term -> Term
Type (Term -> Term) -> ReaderT Int m Term -> ReaderT Int m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackSize VSize
a
  VNat VSize
a  -> Term -> Term
Nat  (Term -> Term) -> ReaderT Int m Term -> ReaderT Int m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackSize VSize
a
  VPi Dom VSize
a VClos
b -> do
    Dom Term
u  <- (VSize -> ReaderT Int m Term)
-> Dom VSize -> ReaderT Int m (Dom Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom a -> f (Dom b)
traverse VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackType Dom VSize
a
    VSize
v0 <- VSize -> Int -> VSize
vVar (Dom VSize -> VSize
forall a. Dom a -> a
unDom Dom VSize
a) (Int -> VSize) -> ReaderT Int m Int -> ReaderT Int m VSize
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT Int m Int
forall r (m :: * -> *). MonadReader r m => m r
ask
    Dom Term -> Abs Term -> Term
Pi Dom Term
u (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
"x" (Term -> Term) -> ReaderT Int m Term -> ReaderT Int m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      (Int -> Int) -> ReaderT Int m Term -> ReaderT Int m Term
forall a. (Int -> Int) -> ReaderT Int m a -> ReaderT Int m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local Int -> Int
forall a. Enum a => a -> a
succ (ReaderT Int m Term -> ReaderT Int m Term)
-> (VSize -> ReaderT Int m Term) -> VSize -> ReaderT Int m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackType (VSize -> ReaderT Int m Term)
-> ReaderT Int m VSize -> ReaderT Int m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        m VSize -> ReaderT Int m VSize
forall (m :: * -> *) a. Monad m => m a -> ReaderT Int m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VSize -> ReaderT Int m VSize) -> m VSize -> ReaderT Int m VSize
forall a b. (a -> b) -> a -> b
$ VClos -> VSize -> m VSize
forall (m :: * -> *). MonadEval m => VClos -> VSize -> m VSize
applyClos VClos
b VSize
v0
  VUp VSize
_ VNe
n -> VNe -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VNe -> ReaderT Int m Term
readbackNe VNe
n
  VSize
_ -> __IMPOSSIBLE__

readbackNat  :: MonadEval m => Val -> ReaderT Int m Term
readbackNat :: forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackNat = \case
  VZero VSize
a        -> Term -> Term
zero (Term -> Term) -> ReaderT Int m Term -> ReaderT Int m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackSize VSize
a
  VSuc VSize
a VSize
t       -> (Term -> Term -> Term)
-> ReaderT Int m Term -> ReaderT Int m Term -> ReaderT Int m Term
forall a b c.
(a -> b -> c)
-> ReaderT Int m a -> ReaderT Int m b -> ReaderT Int m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Term -> Term -> Term
suc (VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackSize VSize
a) (VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackNat VSize
t)
  VUp (VNat VSize
_) VNe
n -> VNe -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VNe -> ReaderT Int m Term
readbackNe VNe
n
  VSize
_ -> __IMPOSSIBLE__

readbackNe  :: MonadEval m => VNe -> ReaderT Int m Term
readbackNe :: forall (m :: * -> *). MonadEval m => VNe -> ReaderT Int m Term
readbackNe (VNe Int
x VElims
es) = do
  Index
i            <- Int -> ReaderT Int m Index
forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
forall (m :: * -> *). MonadEval m => Int -> ReaderT Int m Index
readback Int
x
  Elims
es' :: Elims <- VElims -> ReaderT Int m Elims
forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
forall (m :: * -> *). MonadEval m => VElims -> ReaderT Int m Elims
readback VElims
es
  Term -> ReaderT Int m Term
forall a. a -> ReaderT Int m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ReaderT Int m Term) -> Term -> ReaderT Int m Term
forall a b. (a -> b) -> a -> b
$ (Term -> Elim -> Term) -> Term -> Elims -> Term
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Elim -> Term
App (Index -> Term
Var Index
i) Elims
es'

readbackSize  :: MonadEval m => Val -> ReaderT Int m Term
readbackSize :: forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackSize = \case
  VSize
VInfty   -> Term -> ReaderT Int m Term
forall a. a -> ReaderT Int m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
Infty
  VZero VSize
_  -> Term -> ReaderT Int m Term
forall a. a -> ReaderT Int m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
sZero
  VSuc VSize
_ VSize
a -> Term -> Term
sSuc (Term -> Term) -> ReaderT Int m Term -> ReaderT Int m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VSize -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VSize -> ReaderT Int m Term
readbackSize VSize
a
  VUp VSize
VSize (VNe Int
x []) -> Index -> Term
Var (Index -> Term) -> ReaderT Int m Index -> ReaderT Int m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ReaderT Int m Index
forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
forall (m :: * -> *). MonadEval m => Int -> ReaderT Int m Index
readback Int
x
  VSize
_ -> __IMPOSSIBLE__

-- * Comparison

-- | Size values are partially ordered

cmpSizes :: VSize -> VSize -> Maybe Ordering
cmpSizes :: VSize -> VSize -> Maybe Ordering
cmpSizes VSize
v1 VSize
v2 = do
  SizeView
s1 <- VSize -> Maybe SizeView
sizeView VSize
v1
  SizeView
s2 <- VSize -> Maybe SizeView
sizeView VSize
v2
  case (SizeView
s1, SizeView
s2) of
    (SizeView
a,SizeView
b) | SizeView
a SizeView -> SizeView -> Bool
forall a. Eq a => a -> a -> Bool
== SizeView
b -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
EQ
    (SizeView
SVInfty, SizeView
_) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
GT
    (SizeView
_, SizeView
SVInfty) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
LT
    (SVConst Int
n, SVConst Int
m) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n Int
m
    (SVVar Int
x Int
n, SVVar Int
y Int
m) | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ordering -> Maybe Ordering) -> Ordering -> Maybe Ordering
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n Int
m
    (SVConst Int
n, SVVar Int
y Int
m) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
m -> __IMPOSSIBLE__  -- Here, LT is too strong.
    (SizeView, SizeView)
_ -> __IMPOSSIBLE__  -- TODO

leqSize :: VSize -> VSize -> Bool
leqSize :: VSize -> VSize -> Bool
leqSize VSize
a VSize
b = VSize -> VSize -> VSize
maxSize VSize
a VSize
b VSize -> VSize -> Bool
forall a. Eq a => a -> a -> Bool
== VSize
b

-- | Compute predecessor size, if possible.
sizePred :: VSize -> Maybe VSize
sizePred :: VSize -> Maybe VSize
sizePred VSize
v = do
  VSize -> Maybe SizeView
sizeView VSize
v Maybe SizeView -> (SizeView -> Maybe VSize) -> Maybe VSize
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    SizeView
SVInfty -> VSize -> Maybe VSize
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (VSize -> Maybe VSize) -> VSize -> Maybe VSize
forall a b. (a -> b) -> a -> b
$ VSize
VInfty
    SVConst Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> VSize -> Maybe VSize
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (VSize -> Maybe VSize) -> VSize -> Maybe VSize
forall a b. (a -> b) -> a -> b
$ SizeView -> VSize
unSizeView (SizeView -> VSize) -> SizeView -> VSize
forall a b. (a -> b) -> a -> b
$ Int -> SizeView
SVConst (Int -> SizeView) -> Int -> SizeView
forall a b. (a -> b) -> a -> b
$ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1
    SVVar Int
x Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> VSize -> Maybe VSize
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (VSize -> Maybe VSize) -> VSize -> Maybe VSize
forall a b. (a -> b) -> a -> b
$ SizeView -> VSize
unSizeView (SizeView -> VSize) -> SizeView -> VSize
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SizeView
SVVar Int
x (Int -> SizeView) -> Int -> SizeView
forall a b. (a -> b) -> a -> b
$ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1
    SizeView
_ -> VSize -> Maybe VSize
forall a. a -> Maybe a
Just VSize
v