<commit_before>\section{Using the |Elab| language}
\label{sec:make_elab}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE GADTs, TypeOperators, TupleSections #-}

> module Elaboration.MakeElab where

> import Control.Monad.Error

> import NameSupply.NameSupply
> import NameSupply.NameSupplier

> import Evidences.Tm
> import Evidences.Rules

> import Features.Features ()

> import ProofState.ProofKit

> import DisplayLang.DisplayTm

> import Elaboration.ElabMonad

> import Kit.BwdFwd
> import Kit.MissingLibrary

%endif

\subsection{Tools for writing elaborators}

When part of the display syntax needs to be elaborated as a subproblem, we call
|subElab| rather than |makeElab| to ensure the elaboration does not take place
at the top level. This means that if the subproblem needs to modify the proof
state (for example, to introduce a $\lambda$-boy) it will create a new girl
to work in.

> subElab :: Loc -> (TY :>: InDTmRN) -> Elab (INTM :=>: VAL)
> subElab loc (ty :>: tm) = EElab loc (ty :>: ElabProb tm) Bale

> internalElab :: Loc -> (TY :>: EProb) -> Elab (INTM :=>: VAL)
> internalElab loc (ty :>: ElabDone tt)                = return tt
> internalElab loc (ty :>: ElabProb tm)                = makeElab loc (ty :>: tm)
> internalElab loc (ty :>: ElabInferProb tm)           = makeElabInfer loc tm
> internalElab loc (ty :>: WaitCan (_ :=>: C _) prob)  = internalElab loc (ty :>: prob)
> internalElab loc (ty :>: prob)                       = EElab loc (ty :>: prob) Bale


The |elabCan| instruction asks for an elaboration problem to be solved when the
supplied value is canonical, and returns the result of solving the problem
(which may well be a suspended definition if the value is not currently canonical).

> elabCan :: INTM :=>: VAL -> (TY :>: EProb) -> Elab (INTM :=>: VAL)
> elabCan tt (ty :>: prob) = internalElab (Loc 0) (ty :>: WaitCan tt prob)


The |elabEnsure| instruction demands that a value should be equal to a canonical
value with the given shape. It returns a term and value with the required shape,
together with a proof that these equal the input.

> elabEnsure :: INTM :=>: VAL -> (Can VAL :>: Can ()) -> Elab (INTM :=>: Can VAL, INTM :=>: VAL)
> elabEnsure (tm :=>: C v) (ty :>: t) = case halfZip v t of
>     Nothing  -> throwError' $ err "elabEnsure: halfZip failed!"
>     Just _   -> do
>         ty' :=>: _ <- EQuote (C ty) Bale
>         return (tm :=>: v, N (P refl :$ A ty' :$ A tm)
>                                  :=>: pval refl $$ A (C ty) $$ A (C v))
> elabEnsure (_ :=>: L _) _ = throwError' $ err "elabEnsure: failed to match lambda!"
> elabEnsure (_ :=>: nv) (ty :>: t) = do
>     vu <- unWrapElab $ canTy chev (ty :>: t)
>     let v = fmap valueOf vu
>     pp <- EHope (PRF (EQBLUE (C ty :>: nv) (C ty :>: C v))) Bale
>     return (C (fmap termOf vu) :=>: v, pp)
>  where
>    chev :: (TY :>: ()) -> WrapElab (INTM :=>: VAL)
>    chev (ty :>: ()) = WrapElab (EHope ty Bale)


\subsection{Elaborating |InDTm|s}

We can use the |Elab| language to describe how to elaborate a display term to
produce an evidence term.

> makeElab :: Loc -> (TY :>: InDTmRN) -> Elab (INTM :=>: VAL)

> import <- MakeElabRules

These rules should be moved to features.

> makeElab loc (SET :>: DIMU Nothing iI d i) = do
>       l :=>: lv <- EFake False Bale
>       iI :=>: iIv <- subElab loc (SET :>: iI)
>       d :=>: dv <- subElab loc (ARR iIv (IDESC iIv) :>: d)
>       i :=>: iv <- subElab loc (iIv :>: i)

<       lastIsIndex <- withNSupply (equal (SET :>: (iv,N (P (last xs)))))
<       guard lastIsIndex
<       -- should check i doesn't appear in d (fairly safe it's not in iI :))

>       return $ IMU (Just (N l)) iI d i :=>: IMU (Just lv) iIv dv iv

> makeElab loc (PI UNIT t :>: DCON f) = do
>     tm :=>: tmv <- subElab loc (t $$ A VOID :>: f)
>     return $ LK tm :=>: LK tmv

> makeElab loc (PI (MU l d) t :>: DCON f) = do
>     _ :=>: tmv <- subElab loc $ case l of
>         Nothing  -> elimOpMethodType $$ A d $$ A t :>: f
>         Just l   -> elimOpLabMethodType $$ A l $$ A d $$ A t :>: f
>     x <- ELambda (fortran t) Bale
>     EQuote (elimOp @@ [d, NP x, t, tmv]) Bale

> makeElab loc (PI (SIGMA d r) t :>: DCON f) = do
>     let mt =  PI d . L . HF (fortran r) $ \ a ->
>               PI (r $$ A a) . L . HF (fortran t) $ \ b ->
>               t $$ A (PAIR a b)
>     mt' :=>: _ <- EQuote mt Bale
>     tm :=>: tmv <- subElab loc (mt :>: f)
>     x <- ELambda (fortran t) Bale
>     return $ N ((tm :? mt') :$ A (N (P x :$ Fst)) :$ A (N (P x :$ Snd)))
>                     :=>: tmv $$ A (NP x $$ Fst) $$ A (NP x $$ Snd)

> makeElab loc (PI (ENUMT e) t :>: m) | isTuply m = do
>     _ :=>: tmv <- subElab loc (branchesOp @@ [e, t] :>: m)
>     x <- ELambda (fortran t) Bale
>     EQuote (switchOp @@ [e, NP x, t, tmv]) Bale
>   where
>     isTuply :: InDTmRN -> Bool
>     isTuply DVOID        = True
>     isTuply (DPAIR _ _)  = True
>     isTuply _            = False

> makeElab loc (MONAD d x :>: DCON t) = makeElab loc (MONAD d x :>: DCOMPOSITE t)
> makeElab loc (QUOTIENT a r p :>: DPAIR x DVOID) =
>   makeElab loc (QUOTIENT a r p :>: DCLASS x)

> makeElab loc (NU d :>: DCOIT DU sty f s) = do
>   d' :=>: _ <- EQuote d Bale
>   makeElab loc (NU d :>: DCOIT (DTIN d') sty f s)



We use underscores |DU| in elaboration to mean "figure this out yourself".

> makeElab loc (ty :>: DU) = EHope ty Bale
> makeElab loc (ty :>: DQ s) = EWait s ty neutralise


Elaborating a canonical term with canonical type is a job for |canTy|.

> makeElab loc (C ty :>: DC tm) = do
>     v <- canTy (subElab loc) (ty :>: tm)
>     return $ (C $ fmap termOf v) :=>: (C $ fmap valueOf v)


There are a few possibilities for elaborating $\lambda$-abstractions. If both the
range and term are constants, then we simply |makeElab| underneath. This avoids
creating some trivial children. 

> makeElab loc (PI s (L (K t)) :>: DL (DK dtm)) = do
>     tm :=>: tmv <- subElab loc (t :>: dtm)
>     return $ LK tm :=>: LK tmv

Otherwise, we can simply create a |lambdaBoy| in the current
development, and carry on elaborating.

> makeElab loc (ty :>: DL sc) = do
>     ref <- ELambda (dfortran (DL sc)) Bale
>     ty' <- EGoal Bale
>     makeElab loc (ty' :>: dScopeTm sc)


We push types in to neutral terms by calling |makeElabInfer| on the term, then
coercing the result to the required type. (Note that |ECoerce| will check if the
types are equal, and if so it will not insert a redundant coercion.)

> makeElab loc (w :>: DN n) = do
>     tt <- makeElabInfer loc n
>     let (yt :=>: yn :<: ty :=>: tyv) = extractNeutral tt
>     w' :=>: _ <- EQuote w Bale
>     ECoerce (ty :=>: tyv) (w' :=>: w) (yt :=>: yn) Bale


If we already have an evidence term, we just have to type-check it.<commit_msg>Thou shalt not quote a term produced by elaboration.<commit_after>\section{Using the |Elab| language}
\label{sec:make_elab}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE GADTs, TypeOperators, TupleSections #-}

> module Elaboration.MakeElab where

> import Control.Monad.Error

> import NameSupply.NameSupply
> import NameSupply.NameSupplier

> import Evidences.Tm
> import Evidences.Rules

> import Features.Features ()

> import ProofState.ProofKit

> import DisplayLang.DisplayTm

> import Elaboration.ElabMonad

> import Kit.BwdFwd
> import Kit.MissingLibrary

%endif

\subsection{Tools for writing elaborators}

When part of the display syntax needs to be elaborated as a subproblem, we call
|subElab| rather than |makeElab| to ensure the elaboration does not take place
at the top level. This means that if the subproblem needs to modify the proof
state (for example, to introduce a $\lambda$-boy) it will create a new girl
to work in.

> subElab :: Loc -> (TY :>: InDTmRN) -> Elab (INTM :=>: VAL)
> subElab loc (ty :>: tm) = EElab loc (ty :>: ElabProb tm) Bale

> internalElab :: Loc -> (TY :>: EProb) -> Elab (INTM :=>: VAL)
> internalElab loc (ty :>: ElabDone tt)                = return tt
> internalElab loc (ty :>: ElabProb tm)                = makeElab loc (ty :>: tm)
> internalElab loc (ty :>: ElabInferProb tm)           = makeElabInfer loc tm
> internalElab loc (ty :>: WaitCan (_ :=>: C _) prob)  = internalElab loc (ty :>: prob)
> internalElab loc (ty :>: prob)                       = EElab loc (ty :>: prob) Bale


The |elabCan| instruction asks for an elaboration problem to be solved when the
supplied value is canonical, and returns the result of solving the problem
(which may well be a suspended definition if the value is not currently canonical).

> elabCan :: INTM :=>: VAL -> (TY :>: EProb) -> Elab (INTM :=>: VAL)
> elabCan tt (ty :>: prob) = internalElab (Loc 0) (ty :>: WaitCan tt prob)


The |elabEnsure| instruction demands that a value should be equal to a canonical
value with the given shape. It returns a term and value with the required shape,
together with a proof that these equal the input.

> elabEnsure :: INTM :=>: VAL -> (Can VAL :>: Can ()) -> Elab (INTM :=>: Can VAL, INTM :=>: VAL)
> elabEnsure (tm :=>: C v) (ty :>: t) = case halfZip v t of
>     Nothing  -> throwError' $ err "elabEnsure: halfZip failed!"
>     Just _   -> do
>         ty' :=>: _ <- EQuote (C ty) Bale
>         return (tm :=>: v, N (P refl :$ A ty' :$ A tm)
>                                  :=>: pval refl $$ A (C ty) $$ A (C v))
> elabEnsure (_ :=>: L _) _ = throwError' $ err "elabEnsure: failed to match lambda!"
> elabEnsure (_ :=>: nv) (ty :>: t) = do
>     vu <- unWrapElab $ canTy chev (ty :>: t)
>     let v = fmap valueOf vu
>     pp <- EHope (PRF (EQBLUE (C ty :>: nv) (C ty :>: C v))) Bale
>     return (C (fmap termOf vu) :=>: v, pp)
>  where
>    chev :: (TY :>: ()) -> WrapElab (INTM :=>: VAL)
>    chev (ty :>: ()) = WrapElab (EHope ty Bale)


\subsection{Elaborating |InDTm|s}

We can use the |Elab| language to describe how to elaborate a display term to
produce an evidence term.

> makeElab :: Loc -> (TY :>: InDTmRN) -> Elab (INTM :=>: VAL)

> import <- MakeElabRules

These rules should be moved to features.

> makeElab loc (SET :>: DIMU Nothing iI d i) = do
>       l :=>: lv <- EFake False Bale
>       iI :=>: iIv <- subElab loc (SET :>: iI)
>       d :=>: dv <- subElab loc (ARR iIv (IDESC iIv) :>: d)
>       i :=>: iv <- subElab loc (iIv :>: i)

<       lastIsIndex <- withNSupply (equal (SET :>: (iv,N (P (last xs)))))
<       guard lastIsIndex
<       -- should check i doesn't appear in d (fairly safe it's not in iI :))

>       return $ IMU (Just (N l)) iI d i :=>: IMU (Just lv) iIv dv iv

> makeElab loc (PI UNIT t :>: DCON f) = do
>     tm :=>: tmv <- subElab loc (t $$ A VOID :>: f)
>     return $ LK tm :=>: LK tmv

> makeElab loc (PI (MU l d) t :>: DCON f) = do
>     d' :=>: _ <- EQuote d Bale
>     t' :=>: _ <- EQuote t Bale
>     tm :=>: tmv <- subElab loc $ case l of
>         Nothing  -> elimOpMethodType $$ A d $$ A t :>: f
>         Just l   -> elimOpLabMethodType $$ A l $$ A d $$ A t :>: f
>     x <- ELambda (fortran t) Bale
>     return $ N (elimOp :@ [d', NP x, t', tm]) :=>: elimOp @@ [d, NP x, t, tmv]

> makeElab loc (PI (SIGMA d r) t :>: DCON f) = do
>     let mt =  PI d . L . HF (fortran r) $ \ a ->
>               PI (r $$ A a) . L . HF (fortran t) $ \ b ->
>               t $$ A (PAIR a b)
>     mt' :=>: _ <- EQuote mt Bale
>     tm :=>: tmv <- subElab loc (mt :>: f)
>     x <- ELambda (fortran t) Bale
>     return $ N ((tm :? mt') :$ A (N (P x :$ Fst)) :$ A (N (P x :$ Snd)))
>                     :=>: tmv $$ A (NP x $$ Fst) $$ A (NP x $$ Snd)

> makeElab loc (PI (ENUMT e) t :>: m) | isTuply m = do
>     t' :=>: _ <- EQuote t Bale
>     e' :=>: _ <- EQuote e Bale
>     tm :=>: tmv <- subElab loc (branchesOp @@ [e, t] :>: m)
>     x <- ELambda (fortran t) Bale
>     return $ N (switchOp :@ [e', NP x, t', tm]) :=>: switchOp @@ [e, NP x, t, tmv]
>   where
>     isTuply :: InDTmRN -> Bool
>     isTuply DVOID        = True
>     isTuply (DPAIR _ _)  = True
>     isTuply _            = False

> makeElab loc (MONAD d x :>: DCON t) = makeElab loc (MONAD d x :>: DCOMPOSITE t)
> makeElab loc (QUOTIENT a r p :>: DPAIR x DVOID) =
>   makeElab loc (QUOTIENT a r p :>: DCLASS x)

> makeElab loc (NU d :>: DCOIT DU sty f s) = do
>   d' :=>: _ <- EQuote d Bale
>   makeElab loc (NU d :>: DCOIT (DTIN d') sty f s)



We use underscores |DU| in elaboration to mean "figure this out yourself".

> makeElab loc (ty :>: DU) = EHope ty Bale
> makeElab loc (ty :>: DQ s) = EWait s ty neutralise


Elaborating a canonical term with canonical type is a job for |canTy|.

> makeElab loc (C ty :>: DC tm) = do
>     v <- canTy (subElab loc) (ty :>: tm)
>     return $ (C $ fmap termOf v) :=>: (C $ fmap valueOf v)


There are a few possibilities for elaborating $\lambda$-abstractions. If both the
range and term are constants, then we simply |makeElab| underneath. This avoids
creating some trivial children. 

> makeElab loc (PI s (L (K t)) :>: DL (DK dtm)) = do
>     tm :=>: tmv <- subElab loc (t :>: dtm)
>     return $ LK tm :=>: LK tmv

Otherwise, we can simply create a |lambdaBoy| in the current
development, and carry on elaborating.

> makeElab loc (ty :>: DL sc) = do
>     ref <- ELambda (dfortran (DL sc)) Bale
>     ty' <- EGoal Bale
>     makeElab loc (ty' :>: dScopeTm sc)


We push types in to neutral terms by calling |makeElabInfer| on the term, then
coercing the result to the required type. (Note that |ECoerce| will check if the
types are equal, and if so it will not insert a redundant coercion.)

> makeElab loc (w :>: DN n) = do
>     w' :=>: _ <- EQuote w Bale
>     tt <- makeElabInfer loc n
>     let (yt :=>: yn :<: ty :=>: tyv) = extractNeutral tt
>     ECoerce (ty :=>: tyv) (w' :=>: w) (yt :=>: yn) Bale


If we already have an evidence term, we just have to type-check it.
{'fraction_non_alphanumeric': 0.15172664485641585, 'fraction_numerical': 0.00014540167211922936, 'mean_word_length': 2.6565656565656566, 'pattern_counts': {'":': 0, '<': 63, '<?xml version=': 0, '>': 429, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7363935', 'n_tokens_mistral': 5223, 'n_tokens_neox': 5048, 'n_words': 1933}