<commit_before>\section{The Elaborator}

%if False

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

> module Elaboration.Elaborator where

> import Control.Applicative
> import Control.Monad.Error
> import Data.Traversable

> import Evidences.Tm
> import Evidences.Rules

> import Features.Features ()

> import ProofState.Developments
> import ProofState.Lifting
> import ProofState.ProofContext
> import ProofState.ProofState
> import ProofState.ProofKit

> import DisplayLang.DisplayTm
> import DisplayLang.Naming

> import Tactics.PropSimp

> import Elaboration.ElabMonad
> import Elaboration.MakeElab
> import Elaboration.Unification

> import Cochon.Error

> import Kit.BwdFwd
> import Kit.MissingLibrary

%endif

\subsection{Implementing the |Elab| monad}

The |runElab| proof state command actually interprets an |Elab x| in
the proof state. That is, it defines the semantics of the |Elab| syntax.
It returns |True| in the second component if elaboration was successful,
and |False| if the problem was suspended.

> runElab :: Bool -> (TY :>: Elab (INTM :=>: VAL))
>                       -> ProofState (INTM :=>: VAL, Bool)
> runElab _ (_ :>: Bale x) = return (x, True)

> runElab True (ty :>: ELambda x f) = case lambdable ty of
>     Just (_, s, tyf) -> do
>         ref <- lambdaBoy x
>         runElab True (tyf (NP ref) :>: f ref)
>     Nothing -> throwError' $ err "runElab: type" ++ errTyVal (ty :<: SET)
>                                  ++ err "is not lambdable!"

> runElab False (ty :>: ELambda s f) = runElabTop (ty :>: ELambda s f)

> runElab top (ty :>: EGoal f) = runElab top (ty :>: f ty)

> runElab top (ty :>: EHope tyHope f) = runElabHope tyHope
>     >>= runElab top . (ty :>:) . f

> runElab top (ty :>: EWait s tyWait f) = do
>     tyWait' <- bquoteHere tyWait
>     tt <- make' Waiting (s :<: tyWait' :=>: tyWait)
>     runElab top (ty :>: f tt)

> runElab top (ty :>: EElab l p f)  = runElabProb l p
>     >>= runElab top . (ty :>:) . f . fst

> runElab True (ty :>: ECry e) = do
>     e' <- distillErrors e
>     throwError e'

<     let msg = show (prettyStackError e')
<     putHoleKind (Crying msg)
<     t :=>: tv <- getMotherDefinition
<     return (N t :=>: tv, False)

> runElab False (ty :>: ECry e) = runElabTop (ty :>: ECry e)

> runElab True (ty :>: EFake b f)           = do
>     GirlMother (nom := HOLE _ :<: ty) _ _ _ <- getMother
>     let fr = nom := FAKE :<: ty
>     xs <- if b  then  (| boySpine getAuncles |)
>                 else  (| (init . boySpine) getAuncles |)
>     let tm = P fr $:$ xs
>     runElab True . (ty :>:) . f $ tm :=>: evTm tm

> runElab False (ty :>: EFake b f) = runElabTop (ty :>: EFake b f)


> runElab top (ty :>: EResolve rn f) = do
>     (ref, as, ms) <- resolveHere rn
>     let tm = P ref $:$ as
>     (tmv :<: tyv) <- inferHere tm
>     tyv'  <- bquoteHere tyv
>     runElab top (ty :>: f (PAIR tyv' (N tm) :=>: PAIR tyv tmv, ms))
>   

> runElab top (ty :>: EQuote v f) = do
>     tm <- bquoteHere v
>     runElab top (ty :>: f (tm :=>: v))

> runElab top (ty :>: ECoerce (_S :=>: _Sv) (_T :=>: _Tv) (s :=>: sv) f) = do
>     eq <- withNSupply (equal $ SET :>: (_Sv, _Tv))
>     tt <- if eq
>         then return (s :=>: sv)
>         else do
>             q :=>: qv <- runElabHope (PRF (EQBLUE (SET :>: _Sv) (SET :>: _Tv)))
>             return $ N (coe :@ [_S, _T, q, s]) :=>: coe @@ [_Sv, _Tv, qv, sv]
>     runElab top (ty :>: f tt)

> runElab top (ty :>: tm) = throwError' . err $ "runElab: cannot evaluate "
>                                                 ++ show tm


The |runElabTop| command interprets the |Elab| monad at the top level, by
creating a new subgoal corresponding to the solution. This is necessary
when commands that need to modify the proof state (such as |ELambda|)
are encountered below the top level.

> runElabTop :: (TY :>: Elab (INTM :=>: VAL)) -> ProofState (INTM :=>: VAL, Bool)
> runElabTop (ty :>: elab) = do
>     ty' <- bquoteHere ty
>     x <- pickName "h" ""
>     make' Waiting (x :<: ty' :=>: ty)
>     goIn
>     (tm :=>: tmv, okay) <- runElab True (ty :>: elab)
>     if okay
>         then  return . (, True)  =<< neutralise =<< give tm
>         else  return . (, False) =<< neutralise =<< getMotherDefinition


The |runElabHope| command interprets the |EHope| instruction, which hopes for
an element of a given type. If it is asking for a proof, we might be able to
find one, but otherwise we just create a hole.

> runElabHope :: TY -> ProofState (INTM :=>: VAL)
> runElabHope (PRF p)  = flexiProof p <|> simplifyProof p <|> lastHope (PRF p)
> runElabHope ty       = lastHope ty

> lastHope :: TY -> ProofState (INTM :=>: VAL)
> lastHope ty = do
>     ty' <- bquoteHere ty
>     neutralise =<< make' Hoping ("hope" :<: ty' :=>: ty)

> flexiProof :: VAL -> ProofState (INTM :=>: VAL)
> flexiProof p@(EQBLUE (_S :>: s) (_T :>: (NP ref@(_ := HOLE Hoping :<: _)))) = do
>     s' <- bquoteHere s
>     _S' <- bquoteHere _S
>     _T' <- bquoteHere _T
>     let p' = EQBLUE (_S' :>: s') (_T' :>: NP ref)
>     neutralise =<< suspend ("hope" :<: PRF p' :=>: PRF p)
>         (WaitSolve ref (s' :=>: s) (ElabDone (N (P refl :$ A _S' :$ A s')
>                                               :=>: pval refl $$ A _S $$ A s)))

> flexiProof p@(EQBLUE (_T :>: (NP ref@(_ := HOLE Hoping :<: _))) (_S :>: s)) = do
>     s' <- bquoteHere s
>     _S' <- bquoteHere _S
>     _T' <- bquoteHere _T
>     let p' = EQBLUE (_T' :>: NP ref) (_S' :>: s')
>     neutralise =<< suspend ("hope" :<: PRF p' :=>: PRF p)
>         (WaitSolve ref (s' :=>: s) (ElabDone (N (P refl :$ A _S' :$ A s')
>                                               :=>: pval refl $$ A _S $$ A s)))

> flexiProof _ = (|)

> simplifyProof :: VAL -> ProofState (INTM :=>: VAL)
> simplifyProof p = do
>     pSimp <- runPropSimplify p
>     case pSimp of
>         Just (SimplyTrivial prf) -> do
>             prf' <- bquoteHere prf
>             return $ prf' :=>: prf
>         Just (SimplyAbsurd _) -> do
>             throwError' $ err "hopeProof: proposition is absurd!"
>         Just (Simply qs _ h) -> do
>             qrs <- Data.Traversable.mapM (subProof  . pty) qs
>             h' <- dischargeLots qs h
>             let prf = h' $$$ fmap (A . valueOf) qrs
>             prf' <- bquoteHere prf
>             return $ prf' :=>: prf
>         Nothing -> (|)
>   where
>     subProof :: VAL -> ProofState (INTM :=>: VAL)
>     subProof (PRF p) = flexiProof p <|> lastHope (PRF p)


The |runElabProb| command interprets the |EElab| instruction, which holds a syntactic
representation of an elaboration problem. 
\question{How should this relate to the |internalElab| instruction?}

> runElabProb :: Loc -> (TY :>: EProb) -> ProofState (INTM :=>: VAL, Bool)
> runElabProb loc (ty :>: ElabDone tt) = return (tt, True)
> runElabProb loc (ty :>: ElabProb tm) = runElab False (ty :>: makeElab loc (ty :>: tm))
> runElabProb loc (ty :>: ElabInferProb tm) = runElab False (ty :>: makeElabInfer loc tm)
> runElabProb loc (ty :>: WaitCan (_ :=>: C _) prob) = runElabProb loc (ty :>: prob)
> runElabProb loc (ty :>: prob) = do
>     ty' <- bquoteHere ty
>     return . (, False) =<< neutralise =<< suspend (name prob :<: ty' :=>: ty) prob
>   where
>     name :: EProb -> String
>     name (WaitCan _ _)      = "can"
>     name (WaitSolve _ _ _)  = "solve"
>     name _                  = "suspend"


The |suspend| command can be used to delay elaboration, by creating a subgoal
of the given type and attaching a suspended elaboration problem to its tip.<commit_msg>Elaborator: handle errors more intelligently (trace a message and update hole kind to crying)<commit_after>\section{The Elaborator}

%if False

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

> module Elaboration.Elaborator where

> import Control.Applicative
> import Control.Monad.Error
> import Data.Traversable

> import Evidences.Tm
> import Evidences.Rules

> import Features.Features ()

> import ProofState.Developments
> import ProofState.Lifting
> import ProofState.ProofContext
> import ProofState.ProofState
> import ProofState.ProofKit

> import DisplayLang.DisplayTm
> import DisplayLang.Naming

> import Tactics.PropSimp

> import Elaboration.ElabMonad
> import Elaboration.MakeElab
> import Elaboration.Unification

> import Cochon.Error

> import Kit.BwdFwd
> import Kit.MissingLibrary

%endif

\subsection{Implementing the |Elab| monad}

The |runElab| proof state command actually interprets an |Elab x| in
the proof state. That is, it defines the semantics of the |Elab| syntax.
It returns |True| in the second component if elaboration was successful,
and |False| if the problem was suspended.

> runElab :: Bool -> (TY :>: Elab (INTM :=>: VAL))
>                       -> ProofState (INTM :=>: VAL, Bool)
> runElab _ (_ :>: Bale x) = return (x, True)

> runElab True (ty :>: ELambda x f) = case lambdable ty of
>     Just (_, s, tyf) -> do
>         ref <- lambdaBoy x
>         runElab True (tyf (NP ref) :>: f ref)
>     Nothing -> throwError' $ err "runElab: type" ++ errTyVal (ty :<: SET)
>                                  ++ err "is not lambdable!"

> runElab False (ty :>: ELambda s f) = runElabTop (ty :>: ELambda s f)

> runElab top (ty :>: EGoal f) = runElab top (ty :>: f ty)

> runElab top (ty :>: EHope tyHope f) = runElabHope tyHope
>     >>= runElab top . (ty :>:) . f

> runElab top (ty :>: EWait s tyWait f) = do
>     tyWait' <- bquoteHere tyWait
>     tt <- make' Waiting (s :<: tyWait' :=>: tyWait)
>     runElab top (ty :>: f tt)

> runElab top (ty :>: EElab l p f)  = runElabProb l p
>     >>= runElab top . (ty :>:) . f . fst

> runElab True (ty :>: ECry e) = do
>     e' <- distillErrors e
>     let msg = show (prettyStackError e')
>     mn <- getMotherName
>     proofTrace ("Hole " ++ showName mn ++ " started crying:\n" ++ msg)
>     putHoleKind (Crying msg)
>     t :=>: tv <- getMotherDefinition
>     return (N t :=>: tv, False)

> runElab False (ty :>: ECry e) = runElabTop (ty :>: ECry e)

> runElab True (ty :>: EFake b f)           = do
>     GirlMother (nom := HOLE _ :<: ty) _ _ _ <- getMother
>     let fr = nom := FAKE :<: ty
>     xs <- if b  then  (| boySpine getAuncles |)
>                 else  (| (init . boySpine) getAuncles |)
>     let tm = P fr $:$ xs
>     runElab True . (ty :>:) . f $ tm :=>: evTm tm

> runElab False (ty :>: EFake b f) = runElabTop (ty :>: EFake b f)


> runElab top (ty :>: EResolve rn f) = do
>     (ref, as, ms) <- resolveHere rn
>     let tm = P ref $:$ as
>     (tmv :<: tyv) <- inferHere tm
>     tyv'  <- bquoteHere tyv
>     runElab top (ty :>: f (PAIR tyv' (N tm) :=>: PAIR tyv tmv, ms))
>   

> runElab top (ty :>: EQuote v f) = do
>     tm <- bquoteHere v
>     runElab top (ty :>: f (tm :=>: v))

> runElab top (ty :>: ECoerce (_S :=>: _Sv) (_T :=>: _Tv) (s :=>: sv) f) = do
>     eq <- withNSupply (equal $ SET :>: (_Sv, _Tv))
>     tt <- if eq
>         then return (s :=>: sv)
>         else do
>             q :=>: qv <- runElabHope (PRF (EQBLUE (SET :>: _Sv) (SET :>: _Tv)))
>             return $ N (coe :@ [_S, _T, q, s]) :=>: coe @@ [_Sv, _Tv, qv, sv]
>     runElab top (ty :>: f tt)

> runElab top (ty :>: tm) = throwError' . err $ "runElab: cannot evaluate "
>                                                 ++ show tm


The |runElabTop| command interprets the |Elab| monad at the top level, by
creating a new subgoal corresponding to the solution. This is necessary
when commands that need to modify the proof state (such as |ELambda|)
are encountered below the top level.

> runElabTop :: (TY :>: Elab (INTM :=>: VAL)) -> ProofState (INTM :=>: VAL, Bool)
> runElabTop (ty :>: elab) = do
>     ty' <- bquoteHere ty
>     x <- pickName "h" ""
>     make' Waiting (x :<: ty' :=>: ty)
>     goIn
>     (tm :=>: tmv, okay) <- runElab True (ty :>: elab)
>     if okay
>         then  return . (, True)  =<< neutralise =<< give tm
>         else  return . (, False) =<< neutralise =<< getMotherDefinition <* goOut


The |runElabHope| command interprets the |EHope| instruction, which hopes for
an element of a given type. If it is asking for a proof, we might be able to
find one, but otherwise we just create a hole.

> runElabHope :: TY -> ProofState (INTM :=>: VAL)
> runElabHope (PRF p)  = flexiProof p <|> simplifyProof p
> runElabHope ty       = lastHope ty

> lastHope :: TY -> ProofState (INTM :=>: VAL)
> lastHope ty = do
>     ty' <- bquoteHere ty
>     neutralise =<< make' Hoping ("hope" :<: ty' :=>: ty)

> flexiProof :: VAL -> ProofState (INTM :=>: VAL)
> flexiProof p@(EQBLUE (_S :>: s) (_T :>: (NP ref@(_ := HOLE Hoping :<: _)))) = do
>     s' <- bquoteHere s
>     _S' <- bquoteHere _S
>     _T' <- bquoteHere _T
>     let p' = EQBLUE (_S' :>: s') (_T' :>: NP ref)
>     neutralise =<< suspend ("hope" :<: PRF p' :=>: PRF p)
>         (WaitSolve ref (s' :=>: s) (ElabDone (N (P refl :$ A _S' :$ A s')
>                                               :=>: pval refl $$ A _S $$ A s)))

> flexiProof p@(EQBLUE (_T :>: (NP ref@(_ := HOLE Hoping :<: _))) (_S :>: s)) = do
>     s' <- bquoteHere s
>     _S' <- bquoteHere _S
>     _T' <- bquoteHere _T
>     let p' = EQBLUE (_T' :>: NP ref) (_S' :>: s')
>     neutralise =<< suspend ("hope" :<: PRF p' :=>: PRF p)
>         (WaitSolve ref (s' :=>: s) (ElabDone (N (P refl :$ A _S' :$ A s')
>                                               :=>: pval refl $$ A _S $$ A s)))

> flexiProof _ = (|)

> simplifyProof :: VAL -> ProofState (INTM :=>: VAL)
> simplifyProof p = do
>     pSimp <- runPropSimplify p
>     case pSimp of
>         Just (SimplyTrivial prf) -> do
>             prf' <- bquoteHere prf
>             return $ prf' :=>: prf
>         Just (SimplyAbsurd _) -> return . fst =<< runElabTop (PRF p :>:
>             ECry [err "lastHope: proposition is absurd!"])
>         Just (Simply qs _ h) -> do
>             qrs <- Data.Traversable.mapM (subProof  . pty) qs
>             h' <- dischargeLots qs h
>             let prf = h' $$$ fmap (A . valueOf) qrs
>             prf' <- bquoteHere prf
>             return $ prf' :=>: prf
>         Nothing -> lastHope (PRF p)
>   where
>     subProof :: VAL -> ProofState (INTM :=>: VAL)
>     subProof (PRF p) = flexiProof p <|> lastHope (PRF p)


The |runElabProb| command interprets the |EElab| instruction, which holds a syntactic
representation of an elaboration problem. 
\question{How should this relate to the |internalElab| instruction?}

> runElabProb :: Loc -> (TY :>: EProb) -> ProofState (INTM :=>: VAL, Bool)
> runElabProb loc (ty :>: ElabDone tt) = return (tt, True)
> runElabProb loc (ty :>: ElabProb tm) = runElab False (ty :>: makeElab loc (ty :>: tm))
> runElabProb loc (ty :>: ElabInferProb tm) = runElab False (ty :>: makeElabInfer loc tm)
> runElabProb loc (ty :>: WaitCan (_ :=>: C _) prob) = runElabProb loc (ty :>: prob)
> runElabProb loc (ty :>: prob) = do
>     ty' <- bquoteHere ty
>     return . (, False) =<< neutralise =<< suspend (name prob :<: ty' :=>: ty) prob
>   where
>     name :: EProb -> String
>     name (WaitCan _ _)      = "can"
>     name (WaitSolve _ _ _)  = "solve"
>     name _                  = "suspend"


The |suspend| command can be used to delay elaboration, by creating a subgoal
of the given type and attaching a suspended elaboration problem to its tip.
{'fraction_non_alphanumeric': 0.15872395833333333, 'fraction_numerical': 0.0, 'mean_word_length': 2.4800634345265067, 'pattern_counts': {'":': 0, '<': 136, '<?xml version=': 0, '>': 512, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 16, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3805594', 'n_tokens_mistral': 5797, 'n_tokens_neox': 5545, 'n_words': 1822}