{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Normalisation by evaluation, used as an all-or-nothing fast path for
-- conversion checking.
--
-- 'nbeConvertible' evaluates both sides into a value domain with closures
-- (sharing by construction: a definition's value is evaluated once per
-- occurrence, not once per copy, and Haskell's laziness makes the evaluation
-- call-by-need) and compares the values structurally, with one-step η for
-- lambdas and pairs mirroring 'Rzk.TypeCheck.Eval.etaMatch'. Evaluation is
-- \emph{glued}: a spine over a definition keeps the spine as well as its
-- unfolding, and the unfolding is lazy. Two spines over the same definition
-- are then compared argument by argument, without unfolding it. Only where
-- the spines disagree is an unfolding forced.
--
-- It answers only 'Convertible' or 'DontKnow', never a definite inequality,
-- so a caller falls back to the ordinary unification on 'DontKnow'. The two
-- cases are not opposites, which is why the answer is not a 'Bool'. The fast
-- path can therefore accept more
-- than the unification below it, but never less. Note that it does accept
-- more. The ordinary path decomposes an application pairwise, which invents
-- subgoals that a βδ-equal but structurally different pair need not meet
-- (see 'Rzk.TypeCheck.Unify.unifyViaDecompose').
--
-- Soundness is a subset argument: 'Convertible' is answered only for terms that are
-- βδ-convertible up to α and the one-step η above, with every construct whose
-- /reduction/ consults the context — @recOR@ guard selection, holes, the
-- modal constructs — evaluating to an opaque 'VAbort' that poisons the
-- comparison into 'DontKnow'. Extension types and @recBOT@ are compared
-- structurally (see the note at their 'eval' case): a structurally identical
-- pair of restricted types is also accepted by the ordinary unification,
-- through reflexive coverage and the cross-face coherences already proved at
-- formation. Every 'Convertible' is therefore also a success of the old
-- unification.
--
-- The evaluator is a pure function of the 'Context': 'valueOfVar' is a plain
-- reader-only lookup, and fresh variables for comparing closures are de
-- Bruijn levels ('HFresh'), so the foil scope machinery is never extended and
-- no quote function is needed.
--
-- == Attribution
--
-- None of the underlying techniques are ours. Semantic conversion checking —
-- evaluate both sides into a value domain with closures and compare the
-- values, applying functions to fresh generic values — is the algorithm of
-- Coquand, /An algorithm for type-checking dependent types/ (Science of
-- Computer Programming 26, 1996), the implementation-level core of
-- normalisation by evaluation (Berger and Schwichtenberg, LICS 1991).
--
-- Comparing two stuck terms by their spines, head first and arguments
-- pairwise, rather than by normalising them, is the algorithmic equality of
-- Abel and Coquand, /Untyped Algorithmic Equality for Martin-Löf's Logical
-- Framework with Surjective Pairs/ (Fundamenta Informaticae 77(4):345–395,
-- 2007; TLCA 2005), see <https://www2.tcs.ifi.lmu.de/~abel/lfsigma.pdf>.
--
-- The representation we use for it is the \emph{glued evaluation} of András
-- Kovács' <https://github.com/AndrasKovacs/smalltt smalltt>. Its README
-- states the tension as "in basic conversion checking, we want to evaluate
-- as efficiently as possible; in quoting, we want to output terms which are
-- as small as possible". It resolves the tension by evaluating a top-level
-- variable to "values which represent lazy ('non-deterministic') choice
-- between unfolding the definition, and not unfolding it". Following
-- smalltt, 'conv' also speculates: "whenever we have the same top-level head
-- symbol on both sides, we try to unify the spines", and unfolds only when
-- that fails. smalltt separates its modes and uses gluing for quoting small
-- terms as well. This module has no quote function, so it needs neither.
-- The general implementation shape, environment machines with closures and
-- de Bruijn levels for fresh variables, follows the same author's
-- <https://github.com/AndrasKovacs/elaboration-zoo elaboration-zoo>.
--
-- For the fragment this module deliberately aborts on (tope-indexed
-- reduction such as @recOR@), the template is cubical: Sterling and Angiuli,
-- /Normalization for Cubical Type Theory/ (LICS 2021), and its
-- implementation lineage in @cooltt@.
--
-- What is specific to rzk is only the packaging: the all-or-nothing gating
-- ('Convertible' or 'DontKnow', never refute), and 'VAbort' poisoning of the
-- context-sensitive fragment so that the fast path stays sound by a subset
-- argument.
module Rzk.TypeCheck.NbE (Conversion (..), nbeConvertible) where

import           Control.Monad.Reader              (asks)
import           Data.Bifoldable                   (bifoldMap)
import           Data.Bifunctor                    (bimap)
import           Data.Monoid                       (All (..))
import           Data.ZipMatchK                    (zipMatch2)

import           Control.Monad.Foil                (NameBinder)
import qualified Control.Monad.Foil                as Foil
import           Control.Monad.Free.Foil           (AST (Node, Var),
                                                    ScopedAST (..))
import           Control.Monad.Free.Foil.Annotated (AnnSig (..))

import           Language.Rzk.Foil.Syntax
import           Rzk.TypeCheck.Context
import           Rzk.TypeCheck.Monad

-- * The value domain

data Val n
  = VLam (Closure n)
    -- ^ A lambda: its body under the environment it was evaluated in.
  | VNeutral (Neu n)
    -- ^ An elimination spine, \emph{glued} to its unfolding when it has one.
  | VCon (TermSig (Closure n) (Val n))
    -- ^ Any other node, its term fields evaluated and its scoped fields
    -- closed over the environment. Covers constructors (pairs, @refl@),
    -- types (Π, Σ, identity, universes) and the cube/tope operators, which
    -- are compared structurally only (reflexivity is entailment).
  | VAbort
    -- ^ A construct outside the context-insensitive fragment, or an
    -- elimination of a value that is neither canonical nor neutral. Poisons
    -- the comparison: 'conv' gives up the moment it meets one.
    --
    -- Carries no reason. Nothing can observe one: the module exports
    -- 'nbeConvertible' alone, whose 'DontKnow' says only that the fast path
    -- declined. The eval cases below say which construct each abort is for.

-- | An elimination spine: what it stands on, and what is eliminated off it.
--
-- The two constructors carry the gluing invariant. Only a spine on a name with
-- a definition unfolds, so only 'NGlued' has an unfolding, and a spine on a
-- comparison level cannot be given one. This was a 'Maybe' beside the spine
-- and a comment saying when it was 'Just'.
data Neu n
  = NRigid (Head n) [Elim n]
    -- ^ A spine that does not unfold: on a local, an assumption, or a fresh
    -- comparison level.
  | NGlued (Foil.Name n) [Elim n] (Val n)
    -- ^ A spine on a name with a definition, beside the value the /whole
    -- spine/ unfolds to. That value is a lazy thunk maintained as the spine
    -- grows, so we compute it at most once and only on demand.
    --
    -- We keep both so that 'conv' can answer @f a =? f a@ from the two
    -- spines, without unfolding @f@. Keeping only the unfolding, as this
    -- evaluator did before, normalises a repeated lemma once per occurrence,
    -- and again per nesting level.

-- | What a spine stands on.
data Head n
  = HVar (Foil.Name n)
    -- ^ An ambient name with no definition.
  | HFresh DeBruijnLevel
    -- ^ A fresh variable minted while comparing two closures.

-- | One elimination off a spine.
--
-- A spine holds its eliminations \emph{outermost first}, so @f a b@ is
-- @'NRigid' ('HVar' f) ['EApp' b, 'EApp' a]@. Growing a spine is then a cons
-- rather than an append, which keeps 'applyVal' constant-time in the length
-- of the spine.
data Elim n
  = EApp (Val n)
  | EFirst
  | ESecond
  | EIdJ (Val n) (Val n) (Val n) (Val n) (Val n)
    -- ^ Path induction over the spine: the type, the base point, the motive,
    -- the base case, and the endpoint. The path is the spine itself.

-- | The supply of fresh variables minted while comparing two closures: a de
-- Bruijn level, counting binders from the outside in.
--
-- Note that such a variable is not a name of the ambient scope @n@, so a
-- @'Val' n@ is really a value in @n@ extended by whichever of these are live.
-- We do not index that: extending the foil scope per comparison is the cost
-- this module exists to avoid, and it would need a quote function to get back
-- out. The newtype buys only that the supply cannot be confused with another
-- 'Int'.
--
-- The discipline it rests on is that every level reachable from a value being
-- compared at @lvl@ was minted below @lvl@. That holds because a closure
-- captures only levels minted before it, and because sibling fields of a
-- 'VCon' are compared independently, so one field's levels never reach
-- another. It is checked by reading, not by the types.
newtype DeBruijnLevel = DeBruijnLevel Int
  deriving (DeBruijnLevel -> DeBruijnLevel -> Bool
(DeBruijnLevel -> DeBruijnLevel -> Bool)
-> (DeBruijnLevel -> DeBruijnLevel -> Bool) -> Eq DeBruijnLevel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DeBruijnLevel -> DeBruijnLevel -> Bool
== :: DeBruijnLevel -> DeBruijnLevel -> Bool
$c/= :: DeBruijnLevel -> DeBruijnLevel -> Bool
/= :: DeBruijnLevel -> DeBruijnLevel -> Bool
Eq)

-- | The next level to mint, once @lvl@ has been used.
nextLevel :: DeBruijnLevel -> DeBruijnLevel
nextLevel :: DeBruijnLevel -> DeBruijnLevel
nextLevel (DeBruijnLevel Int
i) = Int -> DeBruijnLevel
DeBruijnLevel (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

-- | Grow a spine by one elimination, pushing the same elimination into the
-- unfolding when there is one.
--
-- We match on the spine rather than use 'fmap' over a 'Maybe'. A rigid spine
-- then costs one allocation, and not also the closure that would push the
-- elimination into an unfolding it does not have.
elimNeu :: Elim n -> (Val n -> Val n) -> Neu n -> Neu n
elimNeu :: forall (n :: S). Elim n -> (Val n -> Val n) -> Neu n -> Neu n
elimNeu Elim n
e Val n -> Val n
onUnfolding = \case
  NRigid Head n
h [Elim n]
es   -> Head n -> [Elim n] -> Neu n
forall (n :: S). Head n -> [Elim n] -> Neu n
NRigid Head n
h (Elim n
e Elim n -> [Elim n] -> [Elim n]
forall a. a -> [a] -> [a]
: [Elim n]
es)
  NGlued Name n
x [Elim n]
es Val n
u -> Name n -> [Elim n] -> Val n -> Neu n
forall (n :: S). Name n -> [Elim n] -> Val n -> Neu n
NGlued Name n
x (Elim n
e Elim n -> [Elim n] -> [Elim n]
forall a. a -> [a] -> [a]
: [Elim n]
es) (Val n -> Val n
onUnfolding Val n
u)

-- | What a spine stands on, always.
headOf :: Neu n -> Head n
headOf :: forall (n :: S). Neu n -> Head n
headOf (NRigid Head n
h [Elim n]
_)   = Head n
h
headOf (NGlued Name n
x [Elim n]
_ Val n
_) = Name n -> Head n
forall (n :: S). Name n -> Head n
HVar Name n
x

-- | What is eliminated off a spine, outermost first.
elimsOf :: Neu n -> [Elim n]
elimsOf :: forall (n :: S). Neu n -> [Elim n]
elimsOf (NRigid Head n
_ [Elim n]
es)   = [Elim n]
es
elimsOf (NGlued Name n
_ [Elim n]
es Val n
_) = [Elim n]
es

-- | A scoped term closed over its environment. The term lives in the scope
-- @i@ the environment is defined on, and the values it evaluates to live in
-- the ambient scope @n@.
--
-- One binder, not @NameBinders i l@: every scope field of every 'TermSig'
-- constructor is a unary 'ScopedAST' (even a pair-pattern lambda binds one
-- variable operationally), so a multi-binder closure would have nothing to
-- be built from without peeling syntactic lambda chains in 'eval'. Peeling
-- (the eval/apply arity optimisation of Marlow and Peyton Jones' fast
-- curry) does not pay here the way spine-batching paid at the term level:
-- an intermediate 'VLam' costs one closure and one persistent environment
-- insert, not a 'substituteT' traversal, and η-comparison and partial
-- application want one-argument-at-a-time semantics anyway.
data Closure n where
  Closure :: Env i n -> NameBinder i l -> TermT l -> Closure n

-- | An environment for evaluating a term of scope @i@ into values of the
-- ambient scope @n@. It maps the binders passed on the way down to the values
-- they were bound to; the entries are lazy on purpose, since forcing one would
-- evaluate it and evaluation is call-by-need.
--
-- This is 'Foil.Substitution', which is exactly that: a map from the names of
-- @i@ to something in @n@, storing only the names it moves. A name it does not
-- carry stands for itself, and 'Foil.lookupSubst' produces that itself through
-- 'Foil.injectName' (see 'Foil.addRename', which deletes an identity rename
-- rather than storing it). Every 'Foil.addSubst' advances @i@ by the binder it
-- inserts, so the scope index tracks which binders the environment accounts
-- for, and the identity environment for the ambient scope is the empty one.
--
-- This is the same invariant 'peelLambdas' relies on for its substitution.
type Env i n = Foil.Substitution Val i n

-- | A name stands for the empty rigid spine on itself. 'Foil.lookupSubst' uses
-- this for a name the environment does not carry, which is also how the name
-- arrives at the ambient scope @n@.
instance Foil.InjectName Val where
  injectName :: forall (n :: S). Name n -> Val n
injectName Name n
x = Neu n -> Val n
forall (n :: S). Neu n -> Val n
VNeutral (Head n -> [Elim n] -> Neu n
forall (n :: S). Head n -> [Elim n] -> Neu n
NRigid (Name n -> Head n
forall (n :: S). Name n -> Head n
HVar Name n
x) [])

-- * Evaluation

eval :: forall i n. Context n -> Env i n -> TermT i -> Val n
eval :: forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env = \case
  -- An ambient name stays a spine, glued to the value of its definition when
  -- it has one. We evaluate that value only on demand, and in the ambient
  -- scope, whose identity environment is the empty one.
  --
  -- The environment carries no ambient name, so a lookup that lands here is
  -- either a miss, or a hit on a value that is itself a rigid spine on an
  -- ambient name with nothing eliminated off it. Every value the environment
  -- holds is an output of 'eval' or a fresh 'HFresh' variable, so in the
  -- second case the head was already glued and carries no definition, and
  -- gluing it again changes nothing.
  Var Name i
x -> case Env i n -> Name i -> Val n
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
Foil.lookupSubst Env i n
env Name i
x of
    v :: Val n
v@(VNeutral (NRigid (HVar Name n
x') [])) ->
      case VarInfo n -> Maybe (TermT n)
forall (n :: S). VarInfo n -> Maybe (TermT n)
varValue (Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
x' Context n
ctx) of
        Maybe (TermT n)
Nothing   -> Val n
v
        Just TermT n
body -> Neu n -> Val n
forall (n :: S). Neu n -> Val n
VNeutral (Name n -> [Elim n] -> Val n -> Neu n
forall (n :: S). Name n -> [Elim n] -> Val n -> Neu n
NGlued Name n
x' [] (Context n -> Env n n -> TermT n -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst TermT n
body))
    Val n
v -> Val n
v

  AppT TypeInfo (TermT i)
_ty TermT i
f TermT i
x -> Context n -> Val n -> Val n -> Val n
forall (n :: S). Context n -> Val n -> Val n -> Val n
applyVal Context n
ctx (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
f) (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
x)
  LambdaT TypeInfo (TermT i)
_ty Binder
_orig Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) i) (TermT i))
_mparam (ScopedAST NameBinder i l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
body) ->
    Closure n -> Val n
forall (n :: S). Closure n -> Val n
VLam (Env i n
-> NameBinder i l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> Closure n
forall (i :: S) (n :: S) (l :: S).
Env i n -> NameBinder i l -> TermT l -> Closure n
Closure Env i n
env NameBinder i l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
body)
  LetT TypeInfo (TermT i)
_ty Binder
_orig Maybe (TermT i)
_mparam TermT i
val (ScopedAST NameBinder i l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
body) ->
    Context n
-> Env l n -> AST NameBinder (AnnSig TypeInfo TermSig) l -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx (Env i n -> NameBinder i l -> Val n -> Env l n
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
Foil.addSubst Env i n
env NameBinder i l
binder (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
val)) AST NameBinder (AnnSig TypeInfo TermSig) l
body
  FirstT TypeInfo (TermT i)
_ty TermT i
t  -> Proj -> Val n -> Val n
forall (n :: S). Proj -> Val n -> Val n
projVal Proj
ProjFirst  (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
t)
  SecondT TypeInfo (TermT i)
_ty TermT i
t -> Proj -> Val n -> Val n
forall (n :: S). Proj -> Val n -> Val n
projVal Proj
ProjSecond (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
t)
  TypeAscT TypeInfo (TermT i)
_ty TermT i
term TermT i
_ty' -> Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
term
  IdJT TypeInfo (TermT i)
_ty TermT i
tA TermT i
a TermT i
tC TermT i
d TermT i
x TermT i
p ->
    let vd :: Val n
vd = Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
d
        e :: Elim n
e = Val n -> Val n -> Val n -> Val n -> Val n -> Elim n
forall (n :: S).
Val n -> Val n -> Val n -> Val n -> Val n -> Elim n
EIdJ (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
tA) (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
a) (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
tC)
                 Val n
vd (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
x)
        -- As in 'projVal'. The induction stays stuck on the spine, and is
        -- glued to the induction over the unfolded path.
        elim :: Val n -> Val n
elim = \case
          VCon ReflF{} -> Val n
vd
          VNeutral Neu n
neu -> Neu n -> Val n
forall (n :: S). Neu n -> Val n
VNeutral (Elim n -> (Val n -> Val n) -> Neu n -> Neu n
forall (n :: S). Elim n -> (Val n -> Val n) -> Neu n -> Neu n
elimNeu Elim n
e Val n -> Val n
elim Neu n
neu)
          -- an abort propagating through, or a stuck induction
          Val n
_            -> Val n
forall (n :: S). Val n
VAbort
    in Val n -> Val n
elim (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env TermT i
p)

  -- The context-sensitive fragment. A @recOR@ reduces by deciding its guards
  -- against the tope context, and a hole defers by design, so both abort. The
  -- modal constructs reduce under 'enterModality', which eval does not track.
  --
  -- An extension type ('TypeRestrictedT') and @recBOT@ do /not/ abort: they
  -- fall through to the generic constructor case below and are compared
  -- structurally. For two restricted types with structurally identical
  -- underlying types and face lists this is sound: the ordinary unification
  -- proves the same pair by reflexive coverage (each face entails the
  -- disjunction containing itself) and by re-checking the cross-face
  -- coherences that were already proved when the type was formed (entailment
  -- is monotone in the tope context). Two @recBOT@s unify unconditionally.
  HoleT{} -> Val n
forall (n :: S). Val n
VAbort
  RecOrT{} -> Val n
forall (n :: S). Val n
VAbort
  TypeModalT{} -> Val n
forall (n :: S). Val n
VAbort
  ModAppT{} -> Val n
forall (n :: S). Val n
VAbort
  ModExtractT{} -> Val n
forall (n :: S). Val n
VAbort
  LetModT{} -> Val n
forall (n :: S). Val n
VAbort

  -- everything else is a plain constructor: evaluate the fields
  Node (AnnSig TypeInfo (TermT i)
_info TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) i) (TermT i)
sig) ->
    TermSig (Closure n) (Val n) -> Val n
forall (n :: S). TermSig (Closure n) (Val n) -> Val n
VCon ((ScopedAST NameBinder (AnnSig TypeInfo TermSig) i -> Closure n)
-> (TermT i -> Val n)
-> TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) i) (TermT i)
-> TermSig (Closure n) (Val n)
forall a b c d. (a -> b) -> (c -> d) -> TermSig a c -> TermSig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (\(ScopedAST NameBinder i l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
body) -> Env i n
-> NameBinder i l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> Closure n
forall (i :: S) (n :: S) (l :: S).
Env i n -> NameBinder i l -> TermT l -> Closure n
Closure Env i n
env NameBinder i l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
body) (Context n -> Env i n -> TermT i -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env i n
env) TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) i) (TermT i)
sig)

-- | β, and the same application pushed into the glued unfolding. Applying a
-- spine grows the spine rather than forcing its head. We carry the unfolded
-- side along lazily, so we normalise nothing unless a comparison asks for it,
-- and the shared thunk keeps us from normalising it twice.
applyVal :: Context n -> Val n -> Val n -> Val n
applyVal :: forall (n :: S). Context n -> Val n -> Val n -> Val n
applyVal Context n
ctx Val n
f Val n
v = case Val n
f of
  VLam Closure n
closure -> Context n -> Closure n -> Val n -> Val n
forall (n :: S). Context n -> Closure n -> Val n -> Val n
applyClosure Context n
ctx Closure n
closure Val n
v
  VNeutral Neu n
neu -> Neu n -> Val n
forall (n :: S). Neu n -> Val n
VNeutral (Elim n -> (Val n -> Val n) -> Neu n -> Neu n
forall (n :: S). Elim n -> (Val n -> Val n) -> Neu n -> Neu n
elimNeu (Val n -> Elim n
forall (n :: S). Val n -> Elim n
EApp Val n
v) (\Val n
u -> Context n -> Val n -> Val n -> Val n
forall (n :: S). Context n -> Val n -> Val n -> Val n
applyVal Context n
ctx Val n
u Val n
v) Neu n
neu)
  -- an abort propagating through, or a stuck application
  Val n
_ -> Val n
forall (n :: S). Val n
VAbort

applyClosure :: Context n -> Closure n -> Val n -> Val n
applyClosure :: forall (n :: S). Context n -> Closure n -> Val n -> Val n
applyClosure Context n
ctx (Closure Env i n
env NameBinder i l
binder TermT l
body) Val n
v =
  Context n -> Env l n -> TermT l -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx (Env i n -> NameBinder i l -> Val n -> Env l n
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
Foil.addSubst Env i n
env NameBinder i l
binder Val n
v) TermT l
body

-- | Which component of a pair a projection takes. One value decides both the
-- spine 'projVal' builds and the component it picks, so the two cannot
-- disagree.
data Proj = ProjFirst | ProjSecond

-- | Project from a pair value, or stay neutral. For a glued spine the
-- projection stays stuck on the spine, and is glued to the projection out of
-- the unfolding. Thus 'conv' can still compare @π₁ (f a)@ rigidly.
projVal :: Proj -> Val n -> Val n
projVal :: forall (n :: S). Proj -> Val n -> Val n
projVal Proj
proj = Val n -> Val n
go
  where
    go :: Val n -> Val n
go = \case
      VCon (PairF Val n
l Val n
r) -> case Proj
proj of
        Proj
ProjFirst  -> Val n
l
        Proj
ProjSecond -> Val n
r
      VNeutral Neu n
neu -> Neu n -> Val n
forall (n :: S). Neu n -> Val n
VNeutral (Elim n -> (Val n -> Val n) -> Neu n -> Neu n
forall (n :: S). Elim n -> (Val n -> Val n) -> Neu n -> Neu n
elimNeu Elim n
e Val n -> Val n
go Neu n
neu)
      -- an abort propagating through, or a stuck projection
      Val n
_            -> Val n
forall (n :: S). Val n
VAbort
    e :: Elim n
e = case Proj
proj of
      Proj
ProjFirst  -> Elim n
forall (n :: S). Elim n
EFirst
      Proj
ProjSecond -> Elim n
forall (n :: S). Elim n
ESecond

-- * Conversion

-- | 'False' means "do not know", never a definite inequality. The exported
-- 'nbeConvertible' names the two cases; inside, 'Bool' is the conjunction
-- monoid this folds with.
--
-- We compare two spines standing on the same definition argument by argument,
-- with neither side unfolded. Congruence makes that answer definite. Forcing
-- both sides to a weak head normal form first, which is what this module did
-- before, normalises a repeated lemma once per occurrence, and again per
-- nesting level.
conv :: Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv :: forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl Val n
l Val n
r
  -- Look for a nearby state in which the two sides stand on the same
  -- definition, and answer from their spines if there is one.
  | Val n -> Val n -> Bool
align Val n
l Val n
r = Bool
True
  -- Without an alignment we force both sides to a weak head normal form and
  -- compare them structurally, as before.
  | Bool
otherwise = case (Val n -> Val n
forall {n :: S}. Val n -> Val n
forceVal Val n
l, Val n -> Val n
forall {n :: S}. Val n -> Val n
forceVal Val n
r) of
      (Val n
VAbort, Val n
_) -> Bool
False
      (Val n
_, Val n
VAbort) -> Bool
False

      (VLam Closure n
c1, VLam Closure n
c2) ->
        Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx (DeBruijnLevel -> DeBruijnLevel
nextLevel DeBruijnLevel
lvl) (Context n -> Closure n -> Val n -> Val n
forall (n :: S). Context n -> Closure n -> Val n -> Val n
applyClosure Context n
ctx Closure n
c1 (DeBruijnLevel -> Val n
forall {n :: S}. DeBruijnLevel -> Val n
freshV DeBruijnLevel
lvl)) (Context n -> Closure n -> Val n -> Val n
forall (n :: S). Context n -> Closure n -> Val n -> Val n
applyClosure Context n
ctx Closure n
c2 (DeBruijnLevel -> Val n
forall {n :: S}. DeBruijnLevel -> Val n
freshV DeBruijnLevel
lvl))
      -- one-step η for lambdas, as in 'etaMatch'
      (VLam Closure n
c1, Val n
v2) ->
        Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx (DeBruijnLevel -> DeBruijnLevel
nextLevel DeBruijnLevel
lvl) (Context n -> Closure n -> Val n -> Val n
forall (n :: S). Context n -> Closure n -> Val n -> Val n
applyClosure Context n
ctx Closure n
c1 (DeBruijnLevel -> Val n
forall {n :: S}. DeBruijnLevel -> Val n
freshV DeBruijnLevel
lvl)) (Context n -> Val n -> Val n -> Val n
forall (n :: S). Context n -> Val n -> Val n -> Val n
applyVal Context n
ctx Val n
v2 (DeBruijnLevel -> Val n
forall {n :: S}. DeBruijnLevel -> Val n
freshV DeBruijnLevel
lvl))
      (Val n
v1, VLam Closure n
c2) ->
        Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx (DeBruijnLevel -> DeBruijnLevel
nextLevel DeBruijnLevel
lvl) (Context n -> Val n -> Val n -> Val n
forall (n :: S). Context n -> Val n -> Val n -> Val n
applyVal Context n
ctx Val n
v1 (DeBruijnLevel -> Val n
forall {n :: S}. DeBruijnLevel -> Val n
freshV DeBruijnLevel
lvl)) (Context n -> Closure n -> Val n -> Val n
forall (n :: S). Context n -> Closure n -> Val n -> Val n
applyClosure Context n
ctx Closure n
c2 (DeBruijnLevel -> Val n
forall {n :: S}. DeBruijnLevel -> Val n
freshV DeBruijnLevel
lvl))

      -- one-step η for pairs. Both sides are forced here, so the spine is
      -- rigid and 'projVal' grows it without unfolding anything.
      (VCon (PairF Val n
a Val n
b), n :: Val n
n@(VNeutral Neu n
_)) ->
        Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl Val n
a (Proj -> Val n -> Val n
forall (n :: S). Proj -> Val n -> Val n
projVal Proj
ProjFirst Val n
n) Bool -> Bool -> Bool
&& Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl Val n
b (Proj -> Val n -> Val n
forall (n :: S). Proj -> Val n -> Val n
projVal Proj
ProjSecond Val n
n)
      (n :: Val n
n@(VNeutral Neu n
_), VCon (PairF Val n
a Val n
b)) ->
        Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl (Proj -> Val n -> Val n
forall (n :: S). Proj -> Val n -> Val n
projVal Proj
ProjFirst Val n
n) Val n
a Bool -> Bool -> Bool
&& Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl (Proj -> Val n -> Val n
forall (n :: S). Proj -> Val n -> Val n
projVal Proj
ProjSecond Val n
n) Val n
b

      (VCon TermSig (Closure n) (Val n)
s1, VCon TermSig (Closure n) (Val n)
s2) -> case TermSig (Closure n) (Val n)
-> TermSig (Closure n) (Val n)
-> Maybe (TermSig (Closure n, Closure n) (Val n, Val n))
forall (f :: * -> * -> *) a b a' b'.
(Bitraversable f, ZipMatchK f) =>
f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
zipMatch2 TermSig (Closure n) (Val n)
s1 TermSig (Closure n) (Val n)
s2 of
        Maybe (TermSig (Closure n, Closure n) (Val n, Val n))
Nothing -> Bool
False
        Just TermSig (Closure n, Closure n) (Val n, Val n)
s  -> All -> Bool
getAll (((Closure n, Closure n) -> All)
-> ((Val n, Val n) -> All)
-> TermSig (Closure n, Closure n) (Val n, Val n)
-> All
forall m a b. Monoid m => (a -> m) -> (b -> m) -> TermSig a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap
          (Bool -> All
All (Bool -> All)
-> ((Closure n, Closure n) -> Bool)
-> (Closure n, Closure n)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Closure n -> Closure n -> Bool) -> (Closure n, Closure n) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Context n -> DeBruijnLevel -> Closure n -> Closure n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Closure n -> Closure n -> Bool
convClosure Context n
ctx DeBruijnLevel
lvl))
          (Bool -> All
All (Bool -> All) -> ((Val n, Val n) -> Bool) -> (Val n, Val n) -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Val n -> Val n -> Bool) -> (Val n, Val n) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl))
          TermSig (Closure n, Closure n) (Val n, Val n)
s)

      (VNeutral Neu n
n1, VNeutral Neu n
n2) -> Context n -> DeBruijnLevel -> Neu n -> Neu n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Neu n -> Neu n -> Bool
convNeu Context n
ctx DeBruijnLevel
lvl Neu n
n1 Neu n
n2
      (Val n, Val n)
_ -> Bool
False
  where
    freshV :: DeBruijnLevel -> Val n
freshV DeBruijnLevel
k = Neu n -> Val n
forall (n :: S). Neu n -> Val n
VNeutral (Head n -> [Elim n] -> Neu n
forall (n :: S). Head n -> [Elim n] -> Neu n
NRigid (DeBruijnLevel -> Head n
forall (n :: S). DeBruijnLevel -> Head n
HFresh DeBruijnLevel
k) [])

    -- Two spines on the same definition are convertible when their
    -- eliminations are. This is congruence, and it needs no unfolding.
    --
    -- Only a glued spine is worth trying. A rigid one reaches the structural
    -- case below anyway, and attempting it here would only repeat a failure.
    -- We need no separate head test: 'convNeu' compares the two heads first.
    aligned :: Val n -> Val n -> Bool
aligned (VNeutral n1 :: Neu n
n1@NGlued{}) (VNeutral Neu n
n2) = Context n -> DeBruijnLevel -> Neu n -> Neu n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Neu n -> Neu n -> Bool
convNeu Context n
ctx DeBruijnLevel
lvl Neu n
n1 Neu n
n2
    aligned Val n
_ Val n
_ = Bool
False

    unfolded :: Val n -> Maybe (Val n)
unfolded (VNeutral (NGlued Name n
_ [Elim n]
_ Val n
u)) = Val n -> Maybe (Val n)
forall a. a -> Maybe a
Just Val n
u
    unfolded Val n
_                         = Maybe (Val n)
forall a. Maybe a
Nothing

    -- The two sides need not stand on the same definition to begin with.
    -- One is often the other under a thin wrapper, such as
    -- @transport … refl t@ for @t@, an alias, or an accessor, and such a
    -- wrapper is a δ-step or two away. We therefore search the unfoldings of
    -- both sides, nearest first, and take the first shared head.
    --
    -- The search is breadth-first over both chains at once. Walking one chain
    -- to its end before starting the other normalises that side completely
    -- whenever the wrapper is on the other side. For example,
    -- @d20 A f x@ against @wrap A (d20 A f x)@ aligns after one step on the
    -- right, but costs 21 million evaluation steps if we walk the left chain
    -- first.
    align :: Val n -> Val n -> Bool
align Val n
a Val n
b = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
      [ Val n -> Val n -> Bool
aligned Val n
a' Val n
b'
      | Int
k <- [Int
0 .. Int
maxAlignOffset]
      , (Int
i, Val n
a') <- [Int] -> [Val n] -> [(Int, Val n)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (Val n -> [Val n]
forall {n :: S}. Val n -> [Val n]
chainOf Val n
a)
      , (Int
j, Val n
b') <- [Int] -> [Val n] -> [(Int, Val n)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (Val n -> [Val n]
forall {n :: S}. Val n -> [Val n]
chainOf Val n
b)
      , Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
i Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k ]

    -- Lazy, and cut off at the window. An element is forced only when the
    -- search reaches it.
    chainOf :: Val n -> [Val n]
chainOf Val n
v = Int -> [Val n] -> [Val n]
forall a. Int -> [a] -> [a]
take (Int
maxAlignOffset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Val n
v Val n -> [Val n] -> [Val n]
forall a. a -> [a] -> [a]
: [Val n] -> (Val n -> [Val n]) -> Maybe (Val n) -> [Val n]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Val n -> [Val n]
chainOf (Val n -> Maybe (Val n)
forall {n :: S}. Val n -> Maybe (Val n)
unfolded Val n
v))

    -- Unfold at the head until the value is canonical or truly stuck.
    forceVal :: Val n -> Val n
forceVal Val n
v = Val n -> (Val n -> Val n) -> Maybe (Val n) -> Val n
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Val n
v Val n -> Val n
forceVal (Val n -> Maybe (Val n)
forall {n :: S}. Val n -> Maybe (Val n)
unfolded Val n
v)

-- | How far to look for a shared head before giving up and comparing weak
-- head normal forms instead. A wrapper sits one or two unfoldings from what
-- it wraps, and beyond that a shared head is unlikely. Every step inside the
-- window forces an unfolding that the fallback would force anyway, so the
-- window costs nothing extra. We keep it small.
maxAlignOffset :: Int
maxAlignOffset :: Int
maxAlignOffset = Int
4

convClosure :: Context n -> DeBruijnLevel -> Closure n -> Closure n -> Bool
convClosure :: forall (n :: S).
Context n -> DeBruijnLevel -> Closure n -> Closure n -> Bool
convClosure Context n
ctx DeBruijnLevel
lvl Closure n
c1 Closure n
c2 =
  Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx (DeBruijnLevel -> DeBruijnLevel
nextLevel DeBruijnLevel
lvl) (Context n -> Closure n -> Val n -> Val n
forall (n :: S). Context n -> Closure n -> Val n -> Val n
applyClosure Context n
ctx Closure n
c1 Val n
fresh) (Context n -> Closure n -> Val n -> Val n
forall (n :: S). Context n -> Closure n -> Val n -> Val n
applyClosure Context n
ctx Closure n
c2 Val n
fresh)
  where
    fresh :: Val n
fresh = Neu n -> Val n
forall (n :: S). Neu n -> Val n
VNeutral (Head n -> [Elim n] -> Neu n
forall (n :: S). Head n -> [Elim n] -> Neu n
NRigid (DeBruijnLevel -> Head n
forall (n :: S). DeBruijnLevel -> Head n
HFresh DeBruijnLevel
lvl) [])

-- | Two spines are convertible when they stand on the same head and their
-- eliminations agree pairwise. Neither side is unfolded.
convNeu :: Context n -> DeBruijnLevel -> Neu n -> Neu n -> Bool
convNeu :: forall (n :: S).
Context n -> DeBruijnLevel -> Neu n -> Neu n -> Bool
convNeu Context n
ctx DeBruijnLevel
lvl Neu n
n1 Neu n
n2 =
  Head n -> Head n -> Bool
forall {l :: S} {l :: S}. Head l -> Head l -> Bool
convHead (Neu n -> Head n
forall (n :: S). Neu n -> Head n
headOf Neu n
n1) (Neu n -> Head n
forall (n :: S). Neu n -> Head n
headOf Neu n
n2) Bool -> Bool -> Bool
&& [Elim n] -> [Elim n] -> Bool
convElims (Neu n -> [Elim n]
forall (n :: S). Neu n -> [Elim n]
elimsOf Neu n
n1) (Neu n -> [Elim n]
forall (n :: S). Neu n -> [Elim n]
elimsOf Neu n
n2)
  where
    convHead :: Head l -> Head l -> Bool
convHead (HVar Name l
x) (HVar Name l
y)     = Name l -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name l
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Name l -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name l
y
    convHead (HFresh DeBruijnLevel
i) (HFresh DeBruijnLevel
j) = DeBruijnLevel
i DeBruijnLevel -> DeBruijnLevel -> Bool
forall a. Eq a => a -> a -> Bool
== DeBruijnLevel
j
    convHead Head l
_ Head l
_                   = Bool
False

    -- The recursive call comes first so that a difference in spine length,
    -- and the innermost eliminations, are settled before we compare the
    -- arguments of the outermost one.
    convElims :: [Elim n] -> [Elim n] -> Bool
convElims [] []           = Bool
True
    convElims (Elim n
e:[Elim n]
es) (Elim n
e':[Elim n]
es') = [Elim n] -> [Elim n] -> Bool
convElims [Elim n]
es [Elim n]
es' Bool -> Bool -> Bool
&& Elim n -> Elim n -> Bool
convElim Elim n
e Elim n
e'
    convElims [Elim n]
_ [Elim n]
_             = Bool
False

    convElim :: Elim n -> Elim n -> Bool
convElim (EApp Val n
v) (EApp Val n
v') = Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl Val n
v Val n
v'
    convElim Elim n
EFirst Elim n
EFirst      = Bool
True
    convElim Elim n
ESecond Elim n
ESecond    = Bool
True
    convElim (EIdJ Val n
tA Val n
a Val n
tC Val n
d Val n
x) (EIdJ Val n
tA' Val n
a' Val n
tC' Val n
d' Val n
x') =
      Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl Val n
tA Val n
tA' Bool -> Bool -> Bool
&& Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl Val n
a Val n
a' Bool -> Bool -> Bool
&& Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl Val n
tC Val n
tC'
        Bool -> Bool -> Bool
&& Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl Val n
d Val n
d' Bool -> Bool -> Bool
&& Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx DeBruijnLevel
lvl Val n
x Val n
x'
    convElim Elim n
_ Elim n
_                = Bool
False

-- * Entry point

-- | The answer of the fast path.
--
-- Note that the two cases are not opposites, so this is deliberately not a
-- 'Bool': 'DontKnow' is never a refutation, and a caller may not read it as
-- one.
data Conversion
  = Convertible
    -- ^ Definitely convertible, by the module's soundness argument.
  | DontKnow
    -- ^ No answer. The two terms may well be convertible, and the caller
    -- falls back to the ordinary unification to find out.
  deriving (Conversion -> Conversion -> Bool
(Conversion -> Conversion -> Bool)
-> (Conversion -> Conversion -> Bool) -> Eq Conversion
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Conversion -> Conversion -> Bool
== :: Conversion -> Conversion -> Bool
$c/= :: Conversion -> Conversion -> Bool
/= :: Conversion -> Conversion -> Bool
Eq, Int -> Conversion -> ShowS
[Conversion] -> ShowS
Conversion -> String
(Int -> Conversion -> ShowS)
-> (Conversion -> String)
-> ([Conversion] -> ShowS)
-> Show Conversion
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Conversion -> ShowS
showsPrec :: Int -> Conversion -> ShowS
$cshow :: Conversion -> String
show :: Conversion -> String
$cshowList :: [Conversion] -> ShowS
showList :: [Conversion] -> ShowS
Show)

-- | Are the two terms definitely convertible?
nbeConvertible :: TermT n -> TermT n -> TypeCheck n Conversion
nbeConvertible :: forall (n :: S). TermT n -> TermT n -> TypeCheck n Conversion
nbeConvertible TermT n
t1 TermT n
t2 = (Context n -> Conversion)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Conversion
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Context n -> Conversion)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      Conversion)
-> (Context n -> Conversion)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Conversion
forall a b. (a -> b) -> a -> b
$ \Context n
ctx ->
  if Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
forall (n :: S).
Context n -> DeBruijnLevel -> Val n -> Val n -> Bool
conv Context n
ctx (Int -> DeBruijnLevel
DeBruijnLevel Int
0) (Context n -> Env n n -> TermT n -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst TermT n
t1) (Context n -> Env n n -> TermT n -> Val n
forall (i :: S) (n :: S). Context n -> Env i n -> TermT i -> Val n
eval Context n
ctx Env n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst TermT n
t2)
    then Conversion
Convertible
    else Conversion
DontKnow