{-# 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 (Val -> Val -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Val -> Val -> Bool
$c/= :: Val -> Val -> Bool
== :: Val -> Val -> Bool
$c== :: Val -> Val -> Bool
Eq, Int -> Val -> ShowS
[Val] -> ShowS
Val -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Val] -> ShowS
$cshowList :: [Val] -> ShowS
show :: Val -> String
$cshow :: Val -> String
showsPrec :: Int -> Val -> ShowS
$cshowsPrec :: Int -> Val -> ShowS
Show)

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

data VClos = VClos
  { VClos -> Abs Term
closBody :: Abs Term
  , VClos -> [Val]
closEnv  :: Env
  }
  deriving (VClos -> VClos -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VClos -> VClos -> Bool
$c/= :: VClos -> VClos -> Bool
== :: VClos -> VClos -> Bool
$c== :: VClos -> VClos -> Bool
Eq, Int -> VClos -> ShowS
[VClos] -> ShowS
VClos -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VClos] -> ShowS
$cshowList :: [VClos] -> ShowS
show :: VClos -> String
$cshow :: VClos -> String
showsPrec :: Int -> VClos -> ShowS
$cshowsPrec :: Int -> 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 :: Val -> Int -> Val
vVar Val
t Int
x = Val -> VNe -> Val
VUp Val
t forall a b. (a -> b) -> a -> b
$ Int -> VElims -> VNe
VNe Int
x []

-- * Size arithmetic

-- | Zero size.

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

-- | Successor size.

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

-- | Variable size.

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

-- | Size increment.

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

-- | Constant size.

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

-- | View a value as a size expression.

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

-- | Successor size on view.

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

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

-- | Compute the maximum of two sizes.

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

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

-- | Evaluation.

evalIn :: MonadEval m => Term -> Env -> m Val
evalIn :: forall (m :: * -> *). MonadEval m => Term -> [Val] -> m Val
evalIn Term
t [Val]
rho = forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall a b (m :: * -> *).
(Evaluate a b, MonadEval m) =>
a -> ReaderT [Val] m b
eval Term
t) [Val]
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 [Val] m Val
eval (Index Int
i) = (forall a. [a] -> Int -> a
!! Int
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *). MonadReader r m => m r
ask

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

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

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

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

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

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

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

-- | Apply a function to an argument.

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

-- | Apply a closure to a value.

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

-- | Unfold a fixed-point.

unfoldFix :: MonadEval m => VType -> VType -> Val -> VSize -> Val -> m Val
unfoldFix :: forall (m :: * -> *).
MonadEval m =>
Val -> Val -> Val -> Val -> Val -> m Val
unfoldFix Val
t Val
tf Val
f Val
a Val
v = forall (m :: * -> *). MonadEval m => Val -> VElims -> m Val
applyEs Val
f forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply
  [ forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Irrelevant Val
a
  , forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ VElim -> Val
VElimBy forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> a -> Elim' a
Fix Val
t Val
tf Val
f
  , forall a. a -> Arg a
defaultArg Val
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 => Val -> VNe -> VElim -> m Val
elimNeNat Val
a VNe
n VElim
e = case VElim
e of
  Apply{} -> __IMPOSSIBLE__

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

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

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

fixKindV :: VType
fixKindV :: Val
fixKindV = Term -> Val
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ Int
n -> Int
n forall a. Num a => a -> a -> a
- (Int
k forall a. Num a => a -> a -> a
+ Int
1)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *). MonadReader r m => m r
ask

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

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

    VDown (VUp Val
_ VNe
_) (VUp Val
_ VNe
n) -> 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b (m :: * -> *).
(Readback a b, 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b (m :: * -> *).
(Readback a b, 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b (m :: * -> *).
(Readback a b, 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
readback

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

readbackNat  :: MonadEval m => Val -> ReaderT Int m Term
readbackNat :: forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackNat = \case
  VZero Val
a        -> Term -> Term
zero forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackSize Val
a
  VSuc Val
a Val
t       -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Term -> Term -> Term
suc (forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackSize Val
a) (forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackNat Val
t)
  VUp (VNat Val
_) VNe
n -> forall (m :: * -> *). MonadEval m => VNe -> ReaderT Int m Term
readbackNe VNe
n
  Val
_ -> __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            <- forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
readback Int
x
  Elims
es' :: Elims <- forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
readback VElims
es
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> 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 => Val -> ReaderT Int m Term
readbackSize = \case
  Val
VInfty   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
Infty
  VZero Val
_  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
sZero
  VSuc Val
_ Val
a -> Term -> Term
sSuc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackSize Val
a
  VUp Val
VSize (VNe Int
x []) -> Index -> Term
Var forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
readback Int
x
  Val
_ -> __IMPOSSIBLE__

-- * Comparison

-- | Size values are partially ordered

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

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

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