<commit_before>\section{Programming Gadgets}

%if False

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

> module Tactics.Gadgets where

%endif



\subsection{The |Return| gadget}

> import -> CochonTactics where
>   : unaryInCT "=" (\tm -> elabGiveNext (DLRET tm) >> return "Ta.")
>       "= <term> - solves the programming problem by returning <term>."


\subsection{The Define gadget}

> import -> CochonTactics where
>   : (simpleCT
>      "define"
>      (| (| (B0 :<) tokenExTm |) :< (%keyword KwDefn%) tokenInTm |)
>      (\ [ExArg rl, InArg tm] -> do
>          relabel rl
>          elabGiveNext (DLRET tm)
>          return "Hurrah!")
>      "define <prob> := <term> - relabels and solves <prob> with <term>")


\subsection{The |By| gadget}

> import -> CochonTactics where
>   : (simpleCT
>     "<="
>     (|(|(B0 :<) (tokenOption tokenName)|) :< (|id tokenExTm
>                                               |id tokenAscription |)|)
>     (\ [n,e] -> do
>         elimCTactic (argOption (unDP . argToEx) n) (argToEx e)
>         optional problemSimplify
>         optional seekGoal
>         return "Eliminated and simplified."
>     )
>     "<= [<comma>] <eliminator> - eliminates with a motive.")


\subsection{The |solve| gadet}

> import -> CochonTactics where
>     : simpleCT
>         "solve"
>         (| (| (B0 :<) tokenName |) :< tokenInTm |)
>         (\ [ExArg (DP rn ::$ []), InArg tm] -> do
>             (ref, spine, _) <- resolveHere rn
>             _ :<: ty <- inferHere (P ref $:$ toSpine spine)
>             _ :=>: tv <- elaborate' (ty :>: tm)
>             tm' <- bquoteHere tv -- force definitional expansion
>             solveHole ref tm'
>             return "Solved."<commit_msg>Gadgets: make by gadget simplify all methods<commit_after>\section{Programming Gadgets}

%if False

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

> module Tactics.Gadgets where

%endif



\subsection{The Return gadget}

> import -> CochonTactics where
>   : unaryInCT "=" (\tm -> elabGiveNext (DLRET tm) >> return "Ta.")
>       "= <term> - solves the programming problem by returning <term>."


\subsection{The Define gadget}

> import -> CochonTactics where
>   : (simpleCT
>      "define"
>      (| (| (B0 :<) tokenExTm |) :< (%keyword KwDefn%) tokenInTm |)
>      (\ [ExArg rl, InArg tm] -> do
>          relabel rl
>          elabGiveNext (DLRET tm)
>          return "Hurrah!")
>      "define <prob> := <term> - relabels and solves <prob> with <term>")


\subsection{The By gadget}

The By gadget, written |<=|, invokes elimination with a motive, then simplifies
the methods and moves to the first subgoal remaining.

> import -> CochonTactics where
>   : (simpleCT
>     "<="
>     (|(|(B0 :<) (tokenOption tokenName)|) :< (|id tokenExTm
>                                               |id tokenAscription |)|)
>     (\ [n,e] -> do
>         elimCTactic (argOption (unDP . argToEx) n) (argToEx e)
>         optional problemSimplify            -- simplify first method
>         many (goDown >> problemSimplify)    -- simplify other methods
>         many goUp                           -- go back up to motive
>         goDown                              -- go down to first method
>         optional seekGoal                   -- jump to goal
>         return "Eliminated and simplified."
>     )
>     "<= [<comma>] <eliminator> - eliminates with a motive.")


\subsection{The Solve gadet}

> import -> CochonTactics where
>     : simpleCT
>         "solve"
>         (| (| (B0 :<) tokenName |) :< tokenInTm |)
>         (\ [ExArg (DP rn ::$ []), InArg tm] -> do
>             (ref, spine, _) <- resolveHere rn
>             _ :<: ty <- inferHere (P ref $:$ toSpine spine)
>             _ :=>: tv <- elaborate' (ty :>: tm)
>             tm' <- bquoteHere tv -- force definitional expansion
>             solveHole ref tm'
>             return "Solved."
{'fraction_non_alphanumeric': 0.15013808686919408, 'fraction_numerical': 0.001506402209389907, 'mean_word_length': 2.0575594781273985, 'pattern_counts': {'":': 0, '<': 46, '<?xml version=': 0, '>': 124, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6504221', 'n_tokens_mistral': 1390, 'n_tokens_neox': 1340, 'n_words': 350}