<commit_before>\section{The |ProofState| Kit}
\label{sec:proof_state_kit}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE FlexibleInstances, TypeOperators, TypeSynonymInstances,
>              GADTs, RankNTypes #-}

> module ProofState.ProofKit where

> import Control.Applicative
> import Control.Monad.Error
> import Control.Monad.State
> import Data.Foldable
> import Data.List

> import Kit.BwdFwd
> import Kit.MissingLibrary

> import NameSupply.NameSupply
> import NameSupply.NameSupplier

> import ProofState.Developments
> import ProofState.News
> import ProofState.Lifting
> import ProofState.ProofContext
> import ProofState.ProofState
> import ProofState.Wire

> import DisplayLang.DisplayTm
> import DisplayLang.Naming

> import Evidences.Tm
> import Evidences.Rules

%endif

\question{There are some serious re-ordering of functions to be done
here, in order to improve the narrative.}


\subsection{Asking for Evidence}

A |ProofState| is almost a |NameSupplier|, but it cannot fork the
name supply.

> instance NameSupplier ProofState where
>     freshRef (s :<: ty) f = do
>         nsupply <- getDevNSupply
>         freshRef (s :<: ty) (\ref nsupply' -> do
>             putDevNSupply nsupply'
>             f ref
>           ) nsupply
>
>     forkNSupply = error "ProofState does not provide forkNSupply"
>     
>     askNSupply = getDevNSupply

We also provide an operator to lift functions from a name supply
to proof state commands.

> withNSupply :: (NameSupply -> x) -> ProofState x
> withNSupply f = getDevNSupply >>= return . f

\begin{danger}[Read-only name supply]

Note that this function has no way to return an updated name supply to
the proof context, so it must not leave any references around when it
has finished.

\end{danger}


The |bquoteHere| command $\beta$-quotes a term using the current name supply.

> bquoteHere :: Tm {d, VV} REF -> ProofState (Tm {d, TT} REF)
> bquoteHere tm = withNSupply $ bquote B0 tm


Similarly, |checkHere| type-checks a term using the local name supply...

> checkHere :: (TY :>: INTM) -> ProofState (INTM :=>: VAL)
> checkHere (ty :>: tm) = do
>     mc <- withNSupply $ typeCheck $ check (ty :>: tm)
>     lift mc

... and |inferHere| infers the type of a term using the local name supply.

> inferHere :: EXTM -> ProofState (VAL :<: TY)
> inferHere tm = do
>     mc <- withNSupply $ typeCheck $ infer tm
>     lift mc




The |validateHere| performs some checks on the current location, which
may be useful for paranoia purposes.

> validateHere :: ProofState ()
> validateHere = do
>     m <- getMother
>     case m of
>         GirlMother (_ := DEFN tm :<: ty) _ _ -> do
>             ty' <- bquoteHere ty
>             mc <- withNSupply (typeCheck $ check (SET :>: ty'))
>             mc `catchEither` intercalate "\n" ["validateHere: girl type failed to type-check: SET does not admit", show ty']
>             tm' <- bquoteHere tm
>             mc <- withNSupply (typeCheck $ check (ty :>: tm'))
>             mc `catchEither` intercalate "\n" ["validateHere: definition failed to type-check:", show ty, "does not admit", show tm']
>             return ()
>         GirlMother (_ := HOLE :<: ty) _ _ -> do
>             ty' <- bquoteHere ty
>             mc <- withNSupply (typeCheck $ check (SET :>: ty'))
>             mc `catchEither` intercalate "\n" ["validateHere: hole type failed to type-check: SET does not admit", show ty']
>             return ()
>         _ -> return ()



\subsection{Navigation Commands}


Now we provide commands to navigate the proof state:
\begin{itemize}
\item |goIn| changes the current location to the bottom-most girl in the current development;
\item |goOut| goes up a layer, so the focus changes to the development containing
the current working location;
\item |goUp| moves the focus to the next eldest girl;
\item |goDown| moves the focus to the next youngest girl.
\end{itemize}

These commands fail (yielding |Nothing|) if they are impossible because the proof context
is not in the required form.

> goIn :: ProofState ()
> goIn = goInAcc (NF F0) `replaceError` "goIn: you can't go that way."
>   where
>     goInAcc :: NewsyEntries -> ProofState ()
>     goInAcc (NF cadets) = do
>         (ls, (es :< e, tip, nsupply)) <- get
>         if entryHasDev e
>            then  put (ls :< Layer es (entryToMother e) (NF cadets) tip nsupply, entryDev e)
>            else  put (ls, (es, tip, nsupply))
>                  >> goInAcc (NF (Right (reverseEntry e) :> cadets)) 
<commit_msg>ProofKit: add a 'withGoal' helper. I thought I would share.<commit_after>\section{The |ProofState| Kit}
\label{sec:proof_state_kit}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE FlexibleInstances, TypeOperators, TypeSynonymInstances,
>              GADTs, RankNTypes #-}

> module ProofState.ProofKit where

> import Control.Applicative
> import Control.Monad.Error
> import Control.Monad.State
> import Data.Foldable
> import Data.List

> import Kit.BwdFwd
> import Kit.MissingLibrary

> import NameSupply.NameSupply
> import NameSupply.NameSupplier

> import ProofState.Developments
> import ProofState.News
> import ProofState.Lifting
> import ProofState.ProofContext
> import ProofState.ProofState
> import ProofState.Wire

> import DisplayLang.DisplayTm
> import DisplayLang.Naming

> import Evidences.Tm
> import Evidences.Rules

%endif

\question{There are some serious re-ordering of functions to be done
here, in order to improve the narrative.}


\subsection{Asking for Evidence}

A |ProofState| is almost a |NameSupplier|, but it cannot fork the
name supply.

> instance NameSupplier ProofState where
>     freshRef (s :<: ty) f = do
>         nsupply <- getDevNSupply
>         freshRef (s :<: ty) (\ref nsupply' -> do
>             putDevNSupply nsupply'
>             f ref
>           ) nsupply
>
>     forkNSupply = error "ProofState does not provide forkNSupply"
>     
>     askNSupply = getDevNSupply

We also provide an operator to lift functions from a name supply
to proof state commands.

> withNSupply :: (NameSupply -> x) -> ProofState x
> withNSupply f = getDevNSupply >>= return . f

\begin{danger}[Read-only name supply]

Note that this function has no way to return an updated name supply to
the proof context, so it must not leave any references around when it
has finished.

\end{danger}


The |bquoteHere| command $\beta$-quotes a term using the current name supply.

> bquoteHere :: Tm {d, VV} REF -> ProofState (Tm {d, TT} REF)
> bquoteHere tm = withNSupply $ bquote B0 tm


Similarly, |checkHere| type-checks a term using the local name supply...

> checkHere :: (TY :>: INTM) -> ProofState (INTM :=>: VAL)
> checkHere (ty :>: tm) = do
>     mc <- withNSupply $ typeCheck $ check (ty :>: tm)
>     lift mc

... and |inferHere| infers the type of a term using the local name supply.

> inferHere :: EXTM -> ProofState (VAL :<: TY)
> inferHere tm = do
>     mc <- withNSupply $ typeCheck $ infer tm
>     lift mc




The |validateHere| performs some checks on the current location, which
may be useful for paranoia purposes.

> validateHere :: ProofState ()
> validateHere = do
>     m <- getMother
>     case m of
>         GirlMother (_ := DEFN tm :<: ty) _ _ -> do
>             ty' <- bquoteHere ty
>             mc <- withNSupply (typeCheck $ check (SET :>: ty'))
>             mc `catchEither` intercalate "\n" ["validateHere: girl type failed to type-check: SET does not admit", show ty']
>             tm' <- bquoteHere tm
>             mc <- withNSupply (typeCheck $ check (ty :>: tm'))
>             mc `catchEither` intercalate "\n" ["validateHere: definition failed to type-check:", show ty, "does not admit", show tm']
>             return ()
>         GirlMother (_ := HOLE :<: ty) _ _ -> do
>             ty' <- bquoteHere ty
>             mc <- withNSupply (typeCheck $ check (SET :>: ty'))
>             mc `catchEither` intercalate "\n" ["validateHere: hole type failed to type-check: SET does not admit", show ty']
>             return ()
>         _ -> return ()


> withGoal :: (VAL -> ProofState ()) -> ProofState ()
> withGoal f = do
>   (_ :=>: goal) <- getGoal "withGoal"
>   f goal


\subsection{Navigation Commands}


Now we provide commands to navigate the proof state:
\begin{itemize}
\item |goIn| changes the current location to the bottom-most girl in the current development;
\item |goOut| goes up a layer, so the focus changes to the development containing
the current working location;
\item |goUp| moves the focus to the next eldest girl;
\item |goDown| moves the focus to the next youngest girl.
\end{itemize}

These commands fail (yielding |Nothing|) if they are impossible because the proof context
is not in the required form.

> goIn :: ProofState ()
> goIn = goInAcc (NF F0) `replaceError` "goIn: you can't go that way."
>   where
>     goInAcc :: NewsyEntries -> ProofState ()
>     goInAcc (NF cadets) = do
>         (ls, (es :< e, tip, nsupply)) <- get
>         if entryHasDev e
>            then  put (ls :< Layer es (entryToMother e) (NF cadets) tip nsupply, entryDev e)
>            else  put (ls, (es, tip, nsupply))
>                  >> goInAcc (NF (Right (reverseEntry e) :> cadets)) 

{'fraction_non_alphanumeric': 0.10954140404259943, 'fraction_numerical': 0.0004346881112801565, 'mean_word_length': 2.978815391266753, 'pattern_counts': {'":': 0, '<': 40, '<?xml version=': 0, '>': 202, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5973457', 'n_tokens_mistral': 2992, 'n_tokens_neox': 2867, 'n_words': 1053}