{-# 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
(Val -> Val -> Bool) -> (Val -> Val -> Bool) -> Eq Val
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
(Int -> Val -> ShowS)
-> (Val -> String) -> ([Val] -> ShowS) -> Show Val
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
(VNe -> VNe -> Bool) -> (VNe -> VNe -> Bool) -> Eq VNe
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
(Int -> VNe -> ShowS)
-> (VNe -> String) -> ([VNe] -> ShowS) -> Show VNe
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
(VClos -> VClos -> Bool) -> (VClos -> VClos -> Bool) -> Eq VClos
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
(Int -> VClos -> ShowS)
-> (VClos -> String) -> ([VClos] -> ShowS) -> Show VClos
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 (VNe -> Val) -> VNe -> Val
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 = (Val -> Val) -> Val -> [Val]
forall a. (a -> a) -> a -> [a]
iterate Val -> Val
vsSuc Val
v [Val] -> Int -> Val
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
(SizeView -> SizeView -> Bool)
-> (SizeView -> SizeView -> Bool) -> Eq SizeView
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
(Int -> SizeView -> ShowS)
-> (SizeView -> String) -> ([SizeView] -> ShowS) -> Show SizeView
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 (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 :: Val -> Maybe SizeView
sizeView = \case
  VZero Val
_              -> SizeView -> Maybe SizeView
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 Val
_ Val
v             -> SizeView -> SizeView
svSuc (SizeView -> SizeView) -> Maybe SizeView -> Maybe SizeView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Val -> Maybe SizeView
sizeView Val
v
  Val
VInfty               -> SizeView -> Maybe SizeView
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 Val
VSize (VNe Int
k []) -> SizeView -> Maybe SizeView
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
  Val
_ -> Maybe SizeView
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 (Val -> Val) -> Val -> Val
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 ( 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 -> Val
unSizeView (SizeView -> Val) -> SizeView -> Val
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 -> Val
unSizeView (SizeView -> Val) -> SizeView -> Val
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 -> Val
unSizeView (SizeView -> Val) -> SizeView -> Val
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 -> Val
unSizeView (SizeView -> Val) -> SizeView -> Val
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 = Identity Val -> Val
forall a. Identity a -> a
runIdentity (Identity Val -> Val) -> Identity Val -> Val
forall a b. (a -> b) -> a -> b
$ Term -> [Val] -> Identity Val
forall (m :: * -> *). MonadEval m => Term -> [Val] -> m Val
evalIn Term
t []

-- | Evaluation.

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

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

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

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

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

applyE :: MonadEval m => Val -> VElim -> m Val
applyE :: Val -> VElim -> m Val
applyE Val
v VElim
e =
  case (Val
v, VElim
e) of
    (Val
_        , Apply Arg Val
u     ) -> Val -> Arg Val -> m Val
forall (m :: * -> *). MonadEval m => Val -> Arg Val -> m Val
apply Val
v Arg Val
u
    (VZero Val
_  , Case Val
_ Val
u Val
_ Val
_) -> Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return Val
u
    (VSuc Val
_ Val
n , Case Val
_ Val
_ Val
_ Val
f) -> Val -> Arg Val -> m Val
forall (m :: * -> *). MonadEval m => Val -> Arg Val -> m Val
apply Val
f (Arg Val -> m Val) -> Arg Val -> m Val
forall a b. (a -> b) -> a -> b
$ Val -> Arg Val
forall a. a -> Arg a
defaultArg Val
n
    (VZero Val
a  , Fix Val
t Val
tf Val
f  ) -> Val -> Val -> Val -> Val -> Val -> m Val
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  ) -> Val -> Val -> Val -> Val -> Val -> m Val
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
_)      -> Val -> VNe -> VElim -> m Val
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 :: 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  -> VClos -> Val -> m Val
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   -> VClos -> Val -> m Val
forall (m :: * -> *). MonadEval m => VClos -> Val -> m Val
applyClos VClos
cl Val
u
  VElimBy VElim
e -> Val -> VElim -> m Val
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' <- VClos -> Val -> m Val
forall (m :: * -> *). MonadEval m => VClos -> Val -> m Val
applyClos VClos
b Val
u
    Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> m Val) -> Val -> m Val
forall a b. (a -> b) -> a -> b
$ Val -> VNe -> Val
VUp Val
t' (VNe -> Val) -> VNe -> Val
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 Val -> VElim
forall a. Arg a -> Elim' a
Apply (Arg Val -> VElim) -> Arg Val -> VElim
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
ai (Val -> Arg Val) -> Val -> Arg Val
forall a b. (a -> b) -> a -> b
$ Val -> Val -> Val
VDown (Dom Val -> Val
forall a. Dom a -> a
unDom Dom Val
a) Val
u ]
  Val
_ -> 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]
++ Val -> String
forall a. Show a => a -> String
show Val
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"  to  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
u
    __IMPOSSIBLE__

-- | Apply a closure to a value.

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

-- | Unfold a fixed-point.

unfoldFix :: MonadEval m => VType -> VType -> Val -> VSize -> Val -> m Val
unfoldFix :: Val -> Val -> Val -> Val -> Val -> m Val
unfoldFix Val
t Val
tf Val
f Val
a Val
v = Val -> VElims -> m Val
forall (m :: * -> *). MonadEval m => Val -> VElims -> m Val
applyEs Val
f (VElims -> m Val) -> VElims -> m Val
forall a b. (a -> b) -> a -> b
$ (Arg Val -> VElim) -> [Arg Val] -> VElims
forall a b. (a -> b) -> [a] -> [b]
map Arg Val -> VElim
forall a. Arg a -> Elim' a
Apply
  [ ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Irrelevant Val
a
  , Val -> Arg Val
forall a. a -> Arg a
defaultArg (Val -> Arg Val) -> Val -> Arg Val
forall a b. (a -> b) -> a -> b
$ VElim -> Val
VElimBy (VElim -> Val) -> VElim -> Val
forall a b. (a -> b) -> a -> b
$ Val -> Val -> Val -> VElim
forall a. a -> a -> a -> Elim' a
Fix Val
t Val
tf Val
f
  , Val -> Arg Val
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 :: 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 <- Val -> Arg Val -> m Val
forall (m :: * -> *). MonadEval m => Val -> Arg Val -> m Val
apply Val
t (Arg Val -> m Val) -> Arg Val -> m Val
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant (Val -> Arg Val) -> Val -> Arg Val
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 <- Val -> Arg Val -> m Val
forall (m :: * -> *). MonadEval m => Val -> Arg Val -> m Val
apply Val
t (Arg Val -> m Val) -> Arg Val -> m Val
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant Val
u
    -- Compute the type of the suc branch
    Val
ts <- Val -> m Val
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 = Val -> Val -> Val -> Val -> VElim
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
    Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> m Val) -> Val -> m Val
forall a b. (a -> b) -> a -> b
$ Val -> VNe -> Val
VUp Val
tr (VNe -> Val) -> VNe -> Val
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 Val
t Val
tf Val
f -> do
    -- Compute the type of the result of the elimination application
    Val
tr <- Val -> VElims -> m Val
forall (m :: * -> *). MonadEval m => Val -> VElims -> m Val
applyEs Val
t (VElims -> m Val) -> VElims -> m Val
forall a b. (a -> b) -> a -> b
$ (Arg Val -> VElim) -> [Arg Val] -> VElims
forall a b. (a -> b) -> [a] -> [b]
map Arg Val -> VElim
forall a. Arg a -> Elim' a
Apply [ ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
ShapeIrr Val
a, ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant (Val -> Arg Val) -> Val -> Arg Val
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 = Val -> Val -> Val -> VElim
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
    Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> m Val) -> Val -> m Val
forall a b. (a -> b) -> a -> b
$ Val -> VNe -> Val
VUp Val
tr (VNe -> Val) -> VNe -> Val
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 :: 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 :: 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 :: Val -> ReaderT Int m Term
readback = \case
    VDown Val
VSize     Val
d -> Val -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackSize Val
d
    VDown (VType Val
_) Val
d -> Val -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackType Val
d
    VDown (VNat Val
_ ) Val
d -> Val -> ReaderT Int m Term
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 (Dom Val -> Val
forall a. Dom a -> a
unDom Dom Val
a) (Int -> Val) -> ReaderT Int m Int -> ReaderT Int m Val
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
      Val
c <- m Val -> ReaderT Int m Val
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Val -> ReaderT Int m Val) -> m Val -> ReaderT Int m Val
forall a b. (a -> b) -> a -> b
$ VClos -> Val -> m Val
forall (m :: * -> *). MonadEval m => VClos -> Val -> m Val
applyClos VClos
b Val
v0
      ArgInfo -> Abs Term -> Term
Lam (Dom Val -> ArgInfo
forall a. Dom a -> ArgInfo
_domInfo Dom Val
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 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)
-> (Val -> ReaderT Int m Term) -> Val -> ReaderT Int m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Val -> ReaderT Int m Term
forall a b (m :: * -> *).
(Readback a b, MonadEval m) =>
a -> ReaderT Int m b
readback (Val -> ReaderT Int m Term)
-> (Val -> Val) -> Val -> ReaderT Int m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Val -> Val -> Val
VDown Val
c (Val -> ReaderT Int m Term)
-> ReaderT Int m Val -> ReaderT Int m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          m Val -> ReaderT Int m Val
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Val -> ReaderT Int m Val) -> m Val -> ReaderT Int m Val
forall a b. (a -> b) -> a -> b
$ Val -> Arg Val -> m Val
forall (m :: * -> *). MonadEval m => Val -> Arg Val -> m Val
apply Val
d (Arg Val -> m Val) -> Arg Val -> m Val
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Val -> Arg Val
forall a. ArgInfo -> a -> Arg a
Arg (Dom Val -> ArgInfo
forall a. Dom a -> ArgInfo
_domInfo Dom Val
a) Val
v0

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

readbackType :: MonadEval m => Val -> ReaderT Int m Term
readbackType :: Val -> ReaderT Int m Term
readbackType = \case
  Val
VSize   -> Term -> ReaderT Int m Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
Size
  VType Val
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
<$> Val -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackSize Val
a
  VNat Val
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
<$> Val -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackSize Val
a
  VPi Dom Val
a VClos
b -> do
    Dom Term
u  <- (Val -> ReaderT Int m Term) -> Dom Val -> ReaderT Int m (Dom Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Val -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackType Dom Val
a
    Val
v0 <- Val -> Int -> Val
vVar (Dom Val -> Val
forall a. Dom a -> a
unDom Dom Val
a) (Int -> Val) -> ReaderT Int m Int -> ReaderT Int m Val
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 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)
-> (Val -> ReaderT Int m Term) -> Val -> ReaderT Int m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Val -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackType (Val -> ReaderT Int m Term)
-> ReaderT Int m Val -> ReaderT Int m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        m Val -> ReaderT Int m Val
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Val -> ReaderT Int m Val) -> m Val -> ReaderT Int m Val
forall a b. (a -> b) -> a -> b
$ VClos -> Val -> m Val
forall (m :: * -> *). MonadEval m => VClos -> Val -> m Val
applyClos VClos
b Val
v0
  VUp Val
_ VNe
n -> VNe -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => VNe -> ReaderT Int m Term
readbackNe VNe
n
  Val
_ -> __IMPOSSIBLE__

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

readbackNe  :: MonadEval m => VNe -> ReaderT Int m Term
readbackNe :: 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
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
readback VElims
es
  Term -> ReaderT Int m Term
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 (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 :: Val -> ReaderT Int m Term
readbackSize = \case
  Val
VInfty   -> Term -> ReaderT Int m Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
Infty
  VZero Val
_  -> Term -> ReaderT Int m Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
sZero
  VSuc Val
_ Val
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
<$> Val -> ReaderT Int m Term
forall (m :: * -> *). MonadEval m => Val -> ReaderT Int m Term
readbackSize Val
a
  VUp Val
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
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 SizeView -> SizeView -> Bool
forall a. Eq a => a -> a -> Bool
== SizeView
b -> Ordering -> Maybe Ordering
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
EQ
    (SizeView
SVInfty, SizeView
_) -> Ordering -> Maybe Ordering
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
GT
    (SizeView
_, SizeView
SVInfty) -> Ordering -> Maybe Ordering
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
LT
    (SVConst Int
n, SVConst Int
m) -> Ordering -> Maybe Ordering
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 (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 :: Val -> Val -> Bool
leqSize Val
a Val
b = Val -> Val -> Val
maxSize Val
a Val
b Val -> Val -> Bool
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 Maybe SizeView -> (SizeView -> Maybe Val) -> Maybe Val
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    SizeView
SVInfty -> Val -> Maybe Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Maybe Val) -> Val -> Maybe Val
forall a b. (a -> b) -> a -> b
$ Val
VInfty
    SVConst Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> Val -> Maybe Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Maybe Val) -> Val -> Maybe Val
forall a b. (a -> b) -> a -> b
$ SizeView -> Val
unSizeView (SizeView -> Val) -> SizeView -> Val
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 -> Val -> Maybe Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Maybe Val) -> Val -> Maybe Val
forall a b. (a -> b) -> a -> b
$ SizeView -> Val
unSizeView (SizeView -> Val) -> SizeView -> Val
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
_ -> Val -> Maybe Val
forall a. a -> Maybe a
Just Val
v