<commit_before>\section{Rules}
\label{sec:rules}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, GADTs, KindSignatures,
>     TypeSynonymInstances, FlexibleInstances, FlexibleContexts, PatternGuards #-}

> module Rules where

> import Control.Applicative
> import Control.Monad
> import Control.Monad.Error

> import Data.Foldable
> import Data.Traversable
> import Data.Maybe

> import BwdFwd
> import Tm
> import Root
> import Rooty
> import Features
> import MissingLibrary

> import {-# SOURCE #-} Tactics

%endif

\subsection{Type-checking Canonicals and Eliminators}

Historically, canonical terms were type-checked by the following
function:

< canTy :: (t -> VAL) -> (Can VAL :>: Can t) -> Maybe (Can (TY :>: t))
< canTy ev (Set,Set)    = Just Set
< canTy ev (Pi s t,Set) = Just (Pi (SET :>: s) ((ARR (ev s) SET) :>: t)
< canTy _  _            = Nothing

If we temporally forget Features, we have here a type-checker that
takes an evaluation function |ev|, a type, and a term to be checked
against this type. When successful, the result of typing is a
canonical term that contains both the initial term and its normalized
form, as we get it for free during type-checking.

However, in order to implement tactics, we have to generalize this
function. The generalization consists in parameterizing |canTy| with a
type-directed function |TY :>: t -> s|, which is equivalent to 
|TY -> t -> s|. Because we are still using the concept of evaluation, both
functions are fused into a single one, of type: |TY :>: t -> (s,VAL)|.
To support the use of tactics, which can fail to produce a
value, we extend this type to |TY :>: t -> m (s,VAL)| where |m| is a
|MonadError|.

Hence, by defining an appropriate function |chev|, we can recover the
previous definition of |canTy|. We can also do much more: intuitively,
we can write any type-directed function in term of |canTy|. That is,
any function traversing the types derivation tree can be expressed
using |canTy|.

> canTy :: MonadError [String] m => (TY :>: t -> m (s :=>: VAL)) -> (Can VAL :>: Can t) -> m (Can (s :=>: VAL))
> canTy chev (Set :>: Set)     = return Set
> canTy chev (Set :>: Pi s t)  = do
>   ssv@(s :=>: sv) <- chev (SET :>: s)
>   ttv@(t :=>: tv) <- chev (ARR sv SET :>: t)
>   return $ Pi ssv ttv
> import <- CanTyRules
> canTy  chev (ty :>: x)  = throwError' $ "canTy: the proposed value "
>                                      ++ show (fmap (\x -> ".") x)
>                                      ++ " is not of type " ++ show ty


Type-checking elimination forms mirrors |canTy|. |elimTy| is provided
with a checker-evaluator, a value |f| of inferred typed |t|, ie. a |f
:<: t| of |VAL :<: Can VAL|, and an eliminator of |Elim t|. If the
operation is type-safe, we are given back the eliminator enclosing the
result of |chev| and the type of the eliminated value.

it computes the type of the argument,
ie. the eliminator, in |Elim (s :=>: VAL)| and the type of the result in
|TY|.

> elimTy :: MonadError [String] m => (TY :>: t -> m (s :=>: VAL)) -> 
>           (VAL :<: Can VAL) -> Elim t ->
>           m (Elim (s :=>: VAL),TY)
> elimTy chev (f :<: Pi s t) (A e) = do
>   eev@(e :=>: ev) <- chev (s :>: e)
>   return $ (A eev, t $$ A ev) 
> import <- ElimTyRules
> elimTy _  (v :<: t) e = throwError' $ "elimTy: failed to eliminate " ++ show v ++ 
>                                    " with " ++ (show $ fmap (\t -> ".") e)


\subsection{Equality and Quotation}

Testing for equality is a direct application of normalization by
evaluation\cite{dybjer:nbe, chapman:phd, dybjer:dependent_types_work}:
to compare two values, we first bring them to their normal form. Then,
it is a simple matter of syntactic equality, defined in Section
\ref{sec:syntactic_equality}, to compare the normal forms.

> equal :: (TY :>: (VAL,VAL)) -> Root -> Bool
> equal (ty :>: (v1,v2)) r = quote (ty :>: v1) r == quote (ty :>: v2) r


|quote| is a type-directed operation that returns a normal form |INTM|
by recursively evaluating the value |VAL| of type |TY|. The normal
form corresponds to a $\beta$-normal $\eta$-long form: there are no
$\beta$-redexes present and all possible $\eta$-expansions have been
performed.

\question{Is that right? It's $\beta$-$\eta$-stuff?}

This is performed by two mutually recursive functions, |inQuote| and
|exQuote|:

< inQuote :: (TY :>: VAL) -> Root -> INTM
< exQuote :: NEU -> Root -> (EXTM :<: TY)

Where |inQuote| quotes values and |exQuote| quotes neutral terms. As
we are initially provided with a value, we quote it with |inQuote|, in
a fresh namespace.

> quote :: (TY :>: VAL) -> Root -> INTM
> quote vty r = inQuote vty (room r "quote")


Quoting a value consists in, if possible, $\eta$-expanding
it. So it goes:

> inQuote :: (TY :>: VAL) -> Root -> INTM
> inQuote tyv              r | Just t    <- etaExpand tyv r = t

Needless to say, we can always $\eta$-expand a closure. Therefore, if
$\eta$-expansion has failed, there are two possible cases: either we
are quoting a neutral term, or a canonical term. In the case of
neutral term, we simply switch to |exQuote|, which is designed to
quote neutral terms:

> inQuote (_ :>: N n)      r = N t
>     where (t :<: _) = exQuote n r

In the case of a canonical term, we use |canTy| to check that |cv| is
of type |cty| and, more importantly, to evaluate |cty|. Then, it is
simply a matter of quoting this |type :>: val| inside the canonical
constructor, and returning the fully quoted term. The reason for the
breeding of |Just| is that we are in the |Maybe| monad, and we really
want to stay in there: |canTy| asks for a |MonadError|. Obviously, we
cannot fail in this code, but we have to be artificially
cautious. Hence, this is |Just| a mess.

> inQuote (C cty :>: C cv) r = fromJust $ do
>     ct <- canTy chev (cty :>: cv)
>     c <- traverse (\(c :=>: _) -> Just $ inQuote c r)  ct
>     return $ C c
>         where chev (t :>: v) = do
>                 return $ (t :>: v) :=>: v
> inQuote (C x :>: t) r = error $ "inQuote: type "
>     ++ show (fmap (\_ -> ()) x) ++ " doesn't admit " ++ show t

As mentioned above, |\eta|-expansion is the first sensible thing to do
when quoting. Sometimes it works, especially for closures and features
for which an |EtaExpand| aspect is defined. Quoting a closure is a bit
tricky: you cannot compute under a binder as you would like to. So, we
first have to generate a fresh variable |v|. Then, we apply |v| to the
function |f|, getting a value of type |t v|. At this point, we can
safely quote this term. The result is a binding of |v| in the quoted
term.

> etaExpand :: (TY :>: VAL) -> Root -> Maybe INTM
> etaExpand (PI s t :>: f) r = Just $
>   L ("" :. fresh ("" :<: s) (\v  -> inQuote (t $$ A v :>: (f $$ A v))) r)
> import <- EtaExpand
> etaExpand _                  _ = Nothing


Now, let us examine the quotation of neutral terms. Remember that a
neutral term is either a parameter, a stuck elimination, or a stuck
operation. Hence, we consider each cases in turn.

> exQuote :: NEU -> Root -> (EXTM :<: TY)

To quote a free variable, ie. a parameter, the idea is the
following. If we are asked to quote a free variable |P|, there are two
possible cases. First case, we have introduced it during an
$\eta$-expansion (see |etaExpand|, above). Hence, we know that it is
bound by a lambda: it needs to be turned into the bound variable |V|,
with the right De Bruijn index. Second case, we have not introduced
it: we can simply return it as such.

> exQuote (P x)       r = quop x r :<: pty x
>     where quop :: REF -> Root -> EXTM
>           quop ref@(ns := _) r = help (bwdList ns) r
>               where
>               help (ns :< (_,i)) (r,j) = if ns == r then V (j-i-1) else P ref

Let's be clear. The code above is, in my opinion, a hack.
Technically, we know that a free variable has been created by |quote|
if and only if the current root and the namespace |ns| of the variable
are the same. Hence, the test |ns == r|. Then, we compute the De
Bruijn index of the bound variable by counting the number of lambdas
traversed up to now -- by looking at |j-1| in our current root |(r,j)|
-- minus the number of lambdas traversed at the time of the parameter
creation, ie. |i|. Do some math, pray, and you get the right De Bruijn
index.


If an elimination is stuck, it is because the function is stuck while
the arguments are ready to go. So, we have to recursively |exQuote|
the neutral application, while |inQuote|-ing the arguments. 

> exQuote (n :$ v)    r = (n' :$ traverse (\(tx :=>: _) -> inQuote tx) e r) :<: ty'
>     where (n' :<: ty)  = exQuote n r
>           Just (e,ty') = elimTy chev (N n :<: unC ty) v
>           chev (t :>: x) =
>             Just $ (t :>: x) :=>: x
>           unC :: VAL -> Can VAL
>           unC (C ty) = ty


Similarly, if an operation is stuck, this means that one of the value
passed as an argument needs to be |inQuote|-ed. So it goes. Note that
the operation itself cannot be stuck: it is a simple fully-applied
constructor which can always compute.

> exQuote (op :@ vs)  r = (op :@ vals) :<: v where
>    (vs',v) = fromJust $ opTy op chev vs 
>    vals = map (\(t :=>: v) -> t) vs'
>    chev (t :>: x) = do
>      return $ inQuote (t :>: x) r :=>: x


As we are in the quotation business, let us define $\beta$-quotation,
ie. |bquote|. Unlike |quote|, |bquote| does not perform
$\eta$-expansion, but just brings the term in $\beta$-normal
form. Therefore, the code is much more simpler than |quote|, although
the idea is the same.

From a technical point of view, it is important to note that we are in
|Rooty| and we don't require a specially crafted |Root| (unlike
|quote| and |quop|, as described above). Because of that, we have to
maintain the variables we have generated and to which De Bruijn index
they correspond. This is the role of the backward list of
references. Note also that we let the user provide an initial
environment of references: this is useful to discharge a bunch of
assumptions inside a term. The typical use-case is |discharge| in
@Tactics.lhs@.

Apart from that, this is a standard $\beta$-quotation: 

> bquote :: Rooty m => Bwd REF -> Tm {d,VV} REF -> m (Tm {d,TT} REF)

If binded by one of our lambda, we bind the free variables to the
(hopefully) correct lambda. We don't do anything otherwise.

> bquote  refs (P x) =
>     case x `elemIndex` refs of
>       Just i -> pure $ V i 
>       Nothing -> pure $ P x

Going under a closure is the usual story: we create a fresh variable,
evaluate the applied term, quote the result, and bring everyone under
a binder.

> bquote refs (L (H vs x t)) = 
>     (|(\t -> L (x :. t))
>       (Rooty.freshRef (x :<: undefined) 
>                       (\x -> bquote (refs :< x) 
>                                     (eval t (vs :< pval x))))|)

For the other constructors, we simply go through and do as much damage
as we can. Simple, easy.

> bquote refs (L (K t)) = (|(L . K) (bquote refs t) |)
> bquote refs (C c) = (|C (traverse (bquote refs) c )|)
> bquote refs (N n) = (|N (bquote refs n)|)
> bquote refs (n :$ v) = (|(:$) (bquote refs n)
>                                 (traverse (bquote refs) v)|)
> bquote refs (op :@ vs) = (|(:@) (pure op)
>                                   (traverse (bquote refs) vs)|)


\subsection{Type checking}
\label{subsec:type-checking}

Here starts the bidirectional type-checking story. In this section, we
address the Checking side. In the next section, we implement the
Inference side. Give Conor a white-board, three pens of different
colors, 30 minutes, and you will know what is happening below in the
Edinburgh style. If you can bear with some black-and-white boring
sequents, keep reading.

The checker works as follow. In a valid typing environment $\Gamma$,
it checks that the term $t$ is indeed of type $T$, ie. $t$ can be
pushed into $T$: |T :>: t|:

$$\Gamma \vdash \mbox{TY} \ni \mbox{Tm \{In,.\} p}$$

Technically, we also need a root and handle failure with the |Maybe|
monad:

> check :: (TY :>: INTM) -> Root -> Maybe ()

Type-checking a canonical term is rather easy, as we just have to
delegate the hard work to |canTy|. The checker-evaluator simply needs
to evaluate the well-typed terms.

> check (C c :>: C c')        r = do
>   canTy chev (c :>: c')
>   return ()
>     where chev (t :>: x) = 
>             Just $ x :=>: evTm x

As for lambda, we know it is simple too. We wish the code was simple
too. But, hey, it isn't. The formal typing rule is the following:

\begin{prooftree}
\AxiomC{$x : S \vdash T x \ni t$}
\UnaryInfC{$\Pi S\ T \ni \lambda x . t$}
\end{prooftree}

As for the implementation, we apply the by-now standard trick of
making a fresh variable $x \in S$ and computing the type |T x|. Then,
we simply have to check that $T\ x \ni t$.

> check (PI s t :>: L sc) r = 
>   Root.freshRef ("" :<: s) 
>            (\ref -> check (t $$ A (pval ref) :>: underScope sc ref)) 
>            r

Formally, we can bring the |Ex| terms into the |In| world with the
rule:

\begin{prooftree}
\AxiomC{$n \in Y$}
\AxiomC{$\star \ni W \equiv Y$}
\BinaryInfC{$W \ni n$}
\end{prooftree}

This translates naturally into the following code:

> check (w :>: N n)           r = do
>   y <- infer n r
>   guard $ equal (SET :>: (w, y)) r
>   return ()

Finally, we can extend the checker with the |Check| aspect. If no rule
has matched, then we have to give up.

> import <- Check
> check _                     _ = Nothing


\subsection{Type inference}
\label{subsec:type-inference}

On the inference side, we also have a valid typing environment
$\Gamma$ that is used to pull types |TY| out of |Ex| terms:

$$\Gamma \vdash \mbox{Tm \{Ex,.\} p} \in \mbox{TY}$$

This translates into the following signature:

> infer :: EXTM -> Root -> Maybe TY

We all know the rule to infer the type of a free variable from the
context:

\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\Gamma, x : A, \Delta \vdash x \in A$}
\end{prooftree}

In Epigram, parameters carry there types, so it even easier:

> infer (P x)              r = Just (pty x)

The rule for eliminators is a generalization of the rule for function
application. Let us give a look at its formal rule:

\begin{prooftree}
\AxiomC{$f \in \Pi\ S\ T$}
\AxiomC{$S \ni x$}
\BinaryInfC{$f x \in {(B x)}^\downarrow$}
\end{prooftree}

The story is the same in the general case: we infer the eliminated
term |t| and we type-check the eliminator, using |elimTy|. Because
|elimTy| computes the result type, we have inferred the result type.

> infer (t :$ s)           r = do
>   C ty <- infer t r
>   (s',ty') <- elimTy chev (evTm t :<: ty) s
>   return ty'
>       where chev (t :>: x) =
>               Just $ check (t :>: x) :=>: evTm x

Following exactly the same principle, we can infer the result of an
operator application:

> infer (op :@ ts)         r = do
>   (vs,t) <- opTy op chev ts
>   return t
>       where chev (t :>: x) = do 
>               ch <- check (t :>: x) r 
>               return $ ch :=>: evTm x

Type ascription is formalized by the following rule:

\begin{prooftree}
\AxiomC{$\star \ni \mbox{ty}$}
\AxiomC{$\mbox{ty}^\downarrow \ni t$}
\BinaryInfC{$(t :\in T) \in \mbox{ty}^\downarrow$}
\end{prooftree}

Which translates directly into the following code:

> infer (t :? ty)          r = do
>   check (SET :>: ty) r
>   let vty = evTm ty
>   check (vty :>: t) r
>   return vty

Obviously, if none of the rule above applies, then there is something
fishy.

> infer _                  _ = Nothing



\subsection{Operators}

In this section, we weave some She aspects. In particular, we bring
inside @Rules.lhs@ the |OpCode|s and |Operators| defined in the
various Features.

> import <- Axioms
> import <- OpCode
>
> operators :: [Op]
> operators = (
>   import <- Operators
>   [])

We also define and import some handy tactics, sugaring some canonical
constructors to make them easier to swallow.

> setTac :: Tac VAL
> setTac = can Set

> conTac :: Tac VAL -> Tac VAL
> conTac t = can $ Con t

> piTac :: Tac VAL -> (REF -> Tac VAL) -> Tac VAL
> piTac s t = can $ Pi s (lambda t)

> arrTac :: Tac VAL -> Tac VAL -> Tac VAL
> arrTac s t = piTac s (\_ -> t)

> (@@@) :: REF -> [Tac VAL] -> Tac VAL
> f @@@ xs = foldl' app (use f) xs $ done
>     where app f x = f . apply (A x)

> import <- SugarTactics

A neat thing to do, because |opTy| gives it for free, is to computeq
the type of the operator. Here is how it goes, relying on the |Fresh|
Rooty. Provided with a Root and an Operator, we compute its type.

> opType ::  Root -> Op -> TY
> opType root op = buildType args ty
>     where names = replicate (opArity op) "x"
>           (args, ty) = runFresh root $ opTy op mkTypes names
>           buildType [] t = t
>           buildType (((s,v) :=>: _) : ts) t = C (Pi s (L (H B0 "" (bquote (B0 :< v) 
>                                                                   (buildType ts t)
>                                                                   root))))
>           mkTypes (ty :>: s) = 
>               Rooty.freshRef (s :<: ty) $ \r ->
>                   return $ (ty,r) :=>: pval r



> inDesc :: VAL
> inDesc = ARG (ENUMT constructors) $
>              eval (L $ "" :. [.x. 
>               N $ switchDOp :@ [constructors, cases, NV x]]) B0
>     where constructors = (CONSE (TAG "done")
>                           (CONSE (TAG "arg")
>                            (CONSE (TAG "ind")
>                             (CONSE (TAG "ind1")
>                              NILE))))
>           cases = PAIR DONE 
>                   (PAIR (ARG SET (L $ "" :. [.s. IND (NV s) DONE]))
>                    (PAIR (ARG SET (L $ "" :. [.h. IND1 DONE]))
>                     (PAIR (IND1 DONE)
>                      VOID)))


\subsection{Observational Equality}

\question{|mkEqConj| does not respect contravariance in the |Pi| rule,
          and, in general, does not introduce quantifiers. At first
          glance, this contradicts the definition in the OTT paper.}

> mkEqConj :: [(TY :>: VAL,TY :>: VAL)] -> VAL
> mkEqConj ((y0 :>: t0,y1 :>: t1) : []) = eqGreen @@ [y0,t0,y1,t1]
> mkEqConj ((y0 :>: t0,y1 :>: t1) : xs) = 
>   AND (eqGreen @@ [y0,t0,y1,t1]) (mkEqConj xs)<commit_msg>Desc-in-desc: fixpoint inDesc and define Desc constructors<commit_after>\section{Rules}
\label{sec:rules}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, GADTs, KindSignatures,
>     TypeSynonymInstances, FlexibleInstances, FlexibleContexts, PatternGuards #-}

> module Rules where

> import Control.Applicative
> import Control.Monad
> import Control.Monad.Error

> import Data.Foldable
> import Data.Traversable
> import Data.Maybe

> import BwdFwd
> import Tm
> import Root
> import Rooty
> import Features
> import MissingLibrary

> import {-# SOURCE #-} Tactics

%endif

\subsection{Type-checking Canonicals and Eliminators}

Historically, canonical terms were type-checked by the following
function:

< canTy :: (t -> VAL) -> (Can VAL :>: Can t) -> Maybe (Can (TY :>: t))
< canTy ev (Set,Set)    = Just Set
< canTy ev (Pi s t,Set) = Just (Pi (SET :>: s) ((ARR (ev s) SET) :>: t)
< canTy _  _            = Nothing

If we temporally forget Features, we have here a type-checker that
takes an evaluation function |ev|, a type, and a term to be checked
against this type. When successful, the result of typing is a
canonical term that contains both the initial term and its normalized
form, as we get it for free during type-checking.

However, in order to implement tactics, we have to generalize this
function. The generalization consists in parameterizing |canTy| with a
type-directed function |TY :>: t -> s|, which is equivalent to 
|TY -> t -> s|. Because we are still using the concept of evaluation, both
functions are fused into a single one, of type: |TY :>: t -> (s,VAL)|.
To support the use of tactics, which can fail to produce a
value, we extend this type to |TY :>: t -> m (s,VAL)| where |m| is a
|MonadError|.

Hence, by defining an appropriate function |chev|, we can recover the
previous definition of |canTy|. We can also do much more: intuitively,
we can write any type-directed function in term of |canTy|. That is,
any function traversing the types derivation tree can be expressed
using |canTy|.

> canTy :: MonadError [String] m => (TY :>: t -> m (s :=>: VAL)) -> (Can VAL :>: Can t) -> m (Can (s :=>: VAL))
> canTy chev (Set :>: Set)     = return Set
> canTy chev (Set :>: Pi s t)  = do
>   ssv@(s :=>: sv) <- chev (SET :>: s)
>   ttv@(t :=>: tv) <- chev (ARR sv SET :>: t)
>   return $ Pi ssv ttv
> import <- CanTyRules
> canTy  chev (ty :>: x)  = throwError' $ "canTy: the proposed value "
>                                      ++ show (fmap (\x -> ".") x)
>                                      ++ " is not of type " ++ show ty


Type-checking elimination forms mirrors |canTy|. |elimTy| is provided
with a checker-evaluator, a value |f| of inferred typed |t|, ie. a |f
:<: t| of |VAL :<: Can VAL|, and an eliminator of |Elim t|. If the
operation is type-safe, we are given back the eliminator enclosing the
result of |chev| and the type of the eliminated value.

it computes the type of the argument,
ie. the eliminator, in |Elim (s :=>: VAL)| and the type of the result in
|TY|.

> elimTy :: MonadError [String] m => (TY :>: t -> m (s :=>: VAL)) -> 
>           (VAL :<: Can VAL) -> Elim t ->
>           m (Elim (s :=>: VAL),TY)
> elimTy chev (f :<: Pi s t) (A e) = do
>   eev@(e :=>: ev) <- chev (s :>: e)
>   return $ (A eev, t $$ A ev) 
> import <- ElimTyRules
> elimTy _  (v :<: t) e = throwError' $ "elimTy: failed to eliminate " ++ show v ++ 
>                                    " with " ++ (show $ fmap (\t -> ".") e)


\subsection{Equality and Quotation}

Testing for equality is a direct application of normalization by
evaluation\cite{dybjer:nbe, chapman:phd, dybjer:dependent_types_work}:
to compare two values, we first bring them to their normal form. Then,
it is a simple matter of syntactic equality, defined in Section
\ref{sec:syntactic_equality}, to compare the normal forms.

> equal :: (TY :>: (VAL,VAL)) -> Root -> Bool
> equal (ty :>: (v1,v2)) r = quote (ty :>: v1) r == quote (ty :>: v2) r


|quote| is a type-directed operation that returns a normal form |INTM|
by recursively evaluating the value |VAL| of type |TY|. The normal
form corresponds to a $\beta$-normal $\eta$-long form: there are no
$\beta$-redexes present and all possible $\eta$-expansions have been
performed.

\question{Is that right? It's $\beta$-$\eta$-stuff?}

This is performed by two mutually recursive functions, |inQuote| and
|exQuote|:

< inQuote :: (TY :>: VAL) -> Root -> INTM
< exQuote :: NEU -> Root -> (EXTM :<: TY)

Where |inQuote| quotes values and |exQuote| quotes neutral terms. As
we are initially provided with a value, we quote it with |inQuote|, in
a fresh namespace.

> quote :: (TY :>: VAL) -> Root -> INTM
> quote vty r = inQuote vty (room r "quote")


Quoting a value consists in, if possible, $\eta$-expanding
it. So it goes:

> inQuote :: (TY :>: VAL) -> Root -> INTM
> inQuote tyv              r | Just t    <- etaExpand tyv r = t

Needless to say, we can always $\eta$-expand a closure. Therefore, if
$\eta$-expansion has failed, there are two possible cases: either we
are quoting a neutral term, or a canonical term. In the case of
neutral term, we simply switch to |exQuote|, which is designed to
quote neutral terms:

> inQuote (_ :>: N n)      r = N t
>     where (t :<: _) = exQuote n r

In the case of a canonical term, we use |canTy| to check that |cv| is
of type |cty| and, more importantly, to evaluate |cty|. Then, it is
simply a matter of quoting this |type :>: val| inside the canonical
constructor, and returning the fully quoted term. The reason for the
breeding of |Just| is that we are in the |Maybe| monad, and we really
want to stay in there: |canTy| asks for a |MonadError|. Obviously, we
cannot fail in this code, but we have to be artificially
cautious. Hence, this is |Just| a mess.

> inQuote (C cty :>: C cv) r = fromJust $ do
>     ct <- canTy chev (cty :>: cv)
>     c <- traverse (\(c :=>: _) -> Just $ inQuote c r)  ct
>     return $ C c
>         where chev (t :>: v) = do
>                 return $ (t :>: v) :=>: v
> inQuote (C x :>: t) r = error $ "inQuote: type "
>     ++ show (fmap (\_ -> ()) x) ++ " doesn't admit " ++ show t

As mentioned above, |\eta|-expansion is the first sensible thing to do
when quoting. Sometimes it works, especially for closures and features
for which an |EtaExpand| aspect is defined. Quoting a closure is a bit
tricky: you cannot compute under a binder as you would like to. So, we
first have to generate a fresh variable |v|. Then, we apply |v| to the
function |f|, getting a value of type |t v|. At this point, we can
safely quote this term. The result is a binding of |v| in the quoted
term.

> etaExpand :: (TY :>: VAL) -> Root -> Maybe INTM
> etaExpand (PI s t :>: f) r = Just $
>   L ("" :. fresh ("" :<: s) (\v  -> inQuote (t $$ A v :>: (f $$ A v))) r)
> import <- EtaExpand
> etaExpand _                  _ = Nothing


Now, let us examine the quotation of neutral terms. Remember that a
neutral term is either a parameter, a stuck elimination, or a stuck
operation. Hence, we consider each cases in turn.

> exQuote :: NEU -> Root -> (EXTM :<: TY)

To quote a free variable, ie. a parameter, the idea is the
following. If we are asked to quote a free variable |P|, there are two
possible cases. First case, we have introduced it during an
$\eta$-expansion (see |etaExpand|, above). Hence, we know that it is
bound by a lambda: it needs to be turned into the bound variable |V|,
with the right De Bruijn index. Second case, we have not introduced
it: we can simply return it as such.

> exQuote (P x)       r = quop x r :<: pty x
>     where quop :: REF -> Root -> EXTM
>           quop ref@(ns := _) r = help (bwdList ns) r
>               where
>               help (ns :< (_,i)) (r,j) = if ns == r then V (j-i-1) else P ref

Let's be clear. The code above is, in my opinion, a hack.
Technically, we know that a free variable has been created by |quote|
if and only if the current root and the namespace |ns| of the variable
are the same. Hence, the test |ns == r|. Then, we compute the De
Bruijn index of the bound variable by counting the number of lambdas
traversed up to now -- by looking at |j-1| in our current root |(r,j)|
-- minus the number of lambdas traversed at the time of the parameter
creation, ie. |i|. Do some math, pray, and you get the right De Bruijn
index.


If an elimination is stuck, it is because the function is stuck while
the arguments are ready to go. So, we have to recursively |exQuote|
the neutral application, while |inQuote|-ing the arguments. 

> exQuote (n :$ v)    r = (n' :$ traverse (\(tx :=>: _) -> inQuote tx) e r) :<: ty'
>     where (n' :<: ty)  = exQuote n r
>           Just (e,ty') = elimTy chev (N n :<: unC ty) v
>           chev (t :>: x) =
>             Just $ (t :>: x) :=>: x
>           unC :: VAL -> Can VAL
>           unC (C ty) = ty


Similarly, if an operation is stuck, this means that one of the value
passed as an argument needs to be |inQuote|-ed. So it goes. Note that
the operation itself cannot be stuck: it is a simple fully-applied
constructor which can always compute.

> exQuote (op :@ vs)  r = (op :@ vals) :<: v where
>    (vs',v) = fromJust $ opTy op chev vs 
>    vals = map (\(t :=>: v) -> t) vs'
>    chev (t :>: x) = do
>      return $ inQuote (t :>: x) r :=>: x


As we are in the quotation business, let us define $\beta$-quotation,
ie. |bquote|. Unlike |quote|, |bquote| does not perform
$\eta$-expansion, but just brings the term in $\beta$-normal
form. Therefore, the code is much more simpler than |quote|, although
the idea is the same.

From a technical point of view, it is important to note that we are in
|Rooty| and we don't require a specially crafted |Root| (unlike
|quote| and |quop|, as described above). Because of that, we have to
maintain the variables we have generated and to which De Bruijn index
they correspond. This is the role of the backward list of
references. Note also that we let the user provide an initial
environment of references: this is useful to discharge a bunch of
assumptions inside a term. The typical use-case is |discharge| in
@Tactics.lhs@.

Apart from that, this is a standard $\beta$-quotation: 

> bquote :: Rooty m => Bwd REF -> Tm {d,VV} REF -> m (Tm {d,TT} REF)

If binded by one of our lambda, we bind the free variables to the
(hopefully) correct lambda. We don't do anything otherwise.

> bquote  refs (P x) =
>     case x `elemIndex` refs of
>       Just i -> pure $ V i 
>       Nothing -> pure $ P x

Going under a closure is the usual story: we create a fresh variable,
evaluate the applied term, quote the result, and bring everyone under
a binder.

> bquote refs (L (H vs x t)) = 
>     (|(\t -> L (x :. t))
>       (Rooty.freshRef (x :<: undefined) 
>                       (\x -> bquote (refs :< x) 
>                                     (eval t (vs :< pval x))))|)

For the other constructors, we simply go through and do as much damage
as we can. Simple, easy.

> bquote refs (L (K t)) = (|(L . K) (bquote refs t) |)
> bquote refs (C c) = (|C (traverse (bquote refs) c )|)
> bquote refs (N n) = (|N (bquote refs n)|)
> bquote refs (n :$ v) = (|(:$) (bquote refs n)
>                                 (traverse (bquote refs) v)|)
> bquote refs (op :@ vs) = (|(:@) (pure op)
>                                   (traverse (bquote refs) vs)|)


\subsection{Type checking}
\label{subsec:type-checking}

Here starts the bidirectional type-checking story. In this section, we
address the Checking side. In the next section, we implement the
Inference side. Give Conor a white-board, three pens of different
colors, 30 minutes, and you will know what is happening below in the
Edinburgh style. If you can bear with some black-and-white boring
sequents, keep reading.

The checker works as follow. In a valid typing environment $\Gamma$,
it checks that the term $t$ is indeed of type $T$, ie. $t$ can be
pushed into $T$: |T :>: t|:

$$\Gamma \vdash \mbox{TY} \ni \mbox{Tm \{In,.\} p}$$

Technically, we also need a root and handle failure with the |Maybe|
monad:

> check :: (TY :>: INTM) -> Root -> Maybe ()

Type-checking a canonical term is rather easy, as we just have to
delegate the hard work to |canTy|. The checker-evaluator simply needs
to evaluate the well-typed terms.

> check (C c :>: C c')        r = do
>   canTy chev (c :>: c')
>   return ()
>     where chev (t :>: x) = 
>             Just $ x :=>: evTm x

As for lambda, we know it is simple too. We wish the code was simple
too. But, hey, it isn't. The formal typing rule is the following:

\begin{prooftree}
\AxiomC{$x : S \vdash T x \ni t$}
\UnaryInfC{$\Pi S\ T \ni \lambda x . t$}
\end{prooftree}

As for the implementation, we apply the by-now standard trick of
making a fresh variable $x \in S$ and computing the type |T x|. Then,
we simply have to check that $T\ x \ni t$.

> check (PI s t :>: L sc) r = 
>   Root.freshRef ("" :<: s) 
>            (\ref -> check (t $$ A (pval ref) :>: underScope sc ref)) 
>            r

Formally, we can bring the |Ex| terms into the |In| world with the
rule:

\begin{prooftree}
\AxiomC{$n \in Y$}
\AxiomC{$\star \ni W \equiv Y$}
\BinaryInfC{$W \ni n$}
\end{prooftree}

This translates naturally into the following code:

> check (w :>: N n)           r = do
>   y <- infer n r
>   guard $ equal (SET :>: (w, y)) r
>   return ()

Finally, we can extend the checker with the |Check| aspect. If no rule
has matched, then we have to give up.

> import <- Check
> check _                     _ = Nothing


\subsection{Type inference}
\label{subsec:type-inference}

On the inference side, we also have a valid typing environment
$\Gamma$ that is used to pull types |TY| out of |Ex| terms:

$$\Gamma \vdash \mbox{Tm \{Ex,.\} p} \in \mbox{TY}$$

This translates into the following signature:

> infer :: EXTM -> Root -> Maybe TY

We all know the rule to infer the type of a free variable from the
context:

\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\Gamma, x : A, \Delta \vdash x \in A$}
\end{prooftree}

In Epigram, parameters carry there types, so it even easier:

> infer (P x)              r = Just (pty x)

The rule for eliminators is a generalization of the rule for function
application. Let us give a look at its formal rule:

\begin{prooftree}
\AxiomC{$f \in \Pi\ S\ T$}
\AxiomC{$S \ni x$}
\BinaryInfC{$f x \in {(B x)}^\downarrow$}
\end{prooftree}

The story is the same in the general case: we infer the eliminated
term |t| and we type-check the eliminator, using |elimTy|. Because
|elimTy| computes the result type, we have inferred the result type.

> infer (t :$ s)           r = do
>   C ty <- infer t r
>   (s',ty') <- elimTy chev (evTm t :<: ty) s
>   return ty'
>       where chev (t :>: x) =
>               Just $ check (t :>: x) :=>: evTm x

Following exactly the same principle, we can infer the result of an
operator application:

> infer (op :@ ts)         r = do
>   (vs,t) <- opTy op chev ts
>   return t
>       where chev (t :>: x) = do 
>               ch <- check (t :>: x) r 
>               return $ ch :=>: evTm x

Type ascription is formalized by the following rule:

\begin{prooftree}
\AxiomC{$\star \ni \mbox{ty}$}
\AxiomC{$\mbox{ty}^\downarrow \ni t$}
\BinaryInfC{$(t :\in T) \in \mbox{ty}^\downarrow$}
\end{prooftree}

Which translates directly into the following code:

> infer (t :? ty)          r = do
>   check (SET :>: ty) r
>   let vty = evTm ty
>   check (vty :>: t) r
>   return vty

Obviously, if none of the rule above applies, then there is something
fishy.

> infer _                  _ = Nothing



\subsection{Operators}

In this section, we weave some She aspects. In particular, we bring
inside @Rules.lhs@ the |OpCode|s and |Operators| defined in the
various Features.

> import <- Axioms
> import <- OpCode
>
> operators :: [Op]
> operators = (
>   import <- Operators
>   [])

We also define and import some handy tactics, sugaring some canonical
constructors to make them easier to swallow.

> setTac :: Tac VAL
> setTac = can Set

> conTac :: Tac VAL -> Tac VAL
> conTac t = can $ Con t

> piTac :: Tac VAL -> (REF -> Tac VAL) -> Tac VAL
> piTac s t = can $ Pi s (lambda t)

> arrTac :: Tac VAL -> Tac VAL -> Tac VAL
> arrTac s t = piTac s (\_ -> t)

> (@@@) :: REF -> [Tac VAL] -> Tac VAL
> f @@@ xs = foldl' app (use f) xs $ done
>     where app f x = f . apply (A x)

> import <- SugarTactics

A neat thing to do, because |opTy| gives it for free, is to computeq
the type of the operator. Here is how it goes, relying on the |Fresh|
Rooty. Provided with a Root and an Operator, we compute its type.

> opType ::  Root -> Op -> TY
> opType root op = buildType args ty
>     where names = replicate (opArity op) "x"
>           (args, ty) = runFresh root $ opTy op mkTypes names
>           buildType [] t = t
>           buildType (((s,v) :=>: _) : ts) t = C (Pi s (L (H B0 "" (bquote (B0 :< v) 
>                                                                   (buildType ts t)
>                                                                   root))))
>           mkTypes (ty :>: s) = 
>               Rooty.freshRef (s :<: ty) $ \r ->
>                   return $ (ty,r) :=>: pval r



> inDesc :: VAL
> inDesc = ARG (ENUMT constructors) $
>              eval (L $ "" :. [.x. 
>               N $ switchDOp :@ [constructors, cases, NV x]]) B0
>     where constructors = (CONSE (TAG "done")
>                           (CONSE (TAG "arg")
>                            (CONSE (TAG "ind")
>                             (CONSE (TAG "ind1")
>                              NILE))))
>           cases = PAIR DONE 
>                   (PAIR (ARG SET (L $ "" :. [.s. IND (NV s) DONE]))
>                    (PAIR (ARG SET (L $ "" :. [.h. IND1 DONE]))
>                     (PAIR (IND1 DONE)
>                      VOID)))

> descInDesc :: VAL
> descInDesc = MU inDesc

> doneInDesc = CON (PAIR ZE VOID)
> argInDesc s d = CON (PAIR (SU ZE) (PAIR s (PAIR d VOID)))
> indInDesc h d = CON (PAIR (SU (SU ZE)) (PAIR h (PAIR d VOID)))
> ind1InDesc d = CON (PAIR (SU (SU (SU ZE))) (PAIR d VOID))


\subsection{Observational Equality}

\question{|mkEqConj| does not respect contravariance in the |Pi| rule,
          and, in general, does not introduce quantifiers. At first
          glance, this contradicts the definition in the OTT paper.}

> mkEqConj :: [(TY :>: VAL,TY :>: VAL)] -> VAL
> mkEqConj ((y0 :>: t0,y1 :>: t1) : []) = eqGreen @@ [y0,t0,y1,t1]
> mkEqConj ((y0 :>: t0,y1 :>: t1) : xs) = 
>   AND (eqGreen @@ [y0,t0,y1,t1]) (mkEqConj xs)
{'fraction_non_alphanumeric': 0.12795549374130738, 'fraction_numerical': 0.0016635305026043796, 'mean_word_length': 2.662970732194586, 'pattern_counts': {'":': 0, '<': 97, '<?xml version=': 0, '>': 649, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 26, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1721196', 'n_tokens_mistral': 12451, 'n_tokens_neox': 11987, 'n_words': 5347}