<commit_before>\section{Tactics}

%if False

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

> module Tactics where

Export |Tac| abstractly.

> import Control.Monad
> import Control.Applicative
> import Debug.Trace

> import BwdFwd
> import Rooty
> import Root
> import Tm
> import Rules

%endif

\subsection{The machinery}

> newtype Tac x = Tac { runTac :: Root -> TY -> Maybe x }

> instance Functor Tac where
>     fmap f g = Tac { runTac = \r t -> fmap f (runTac g r t) }

> instance Applicative Tac where
>     pure x = Tac { runTac = \_ _ -> Just x }
>     f <*> x = Tac { runTac = \r t ->
>                              do 
>                              f' <- runTac f r t
>                              x' <- runTac x r t
>                              return $ f' x' }

> instance Monad Tac where
>     return = pure
>     x >>= f = Tac { runTac = \r t -> 
>                                do 
>                                x <- runTac x r t
>                                runTac (f x) r t }

> instance Rooty Tac where
>     freshRef x tacF = Tac { runTac = Rooty.freshRef x (runTac . tacF) }
>     forkRoot s child dad = Tac { runTac = \root typ -> 
>                                           do 
>                                           c <- runTac child (room root s) typ
>                                           runTac (dad c) (roos root) typ
>                                }

\subsection{The tactic combinators}

This is the only place where we are allowed to play inside |Tac { ... }|.

\subsubsection{Setting goals}

This is a bit of Reader digest: |ask| and |runReader|.

> goal :: Tac TY
> goal = Tac { runTac = \root typ -> Just typ }

> subgoal :: TY -> Tac x -> Tac x
> subgoal typ tacX = 
>     Tac { runTac = \root typ' -> 
>           do
>           guard $ equal (SET :>: (typ, typ')) root 
>           runTac tacX root typ
>         }

\subsubsection{}

> discharge :: Rooty m => REF -> VAL -> m VAL
> discharge freshRef val = (|(\t -> L (H B0 "discharge" t)) 
>                            (quoteRef' [freshRef] val) |)

\subsection{Syntax-directed tacticals}

Intros

> lambda :: (VAL -> Tac VAL) -> Tac VAL
> lambda body = do
>   C (Pi s t) <- goal
>   Rooty.freshRef ("" :<: s) $
>                  \x -> 
>                      discharge x =<<
>                      subgoal (t $$ A (pval x)) (body (pval x))

This one should use the modified version of canTy:
       
> can :: Can (Tac VAL) -> Tac VAL
> can Set = do
>           SET <- goal
>           return SET
> can (Pi tacS tacT) = do
>   SET <- goal
>   s <- subgoal SET tacS
>   t <- subgoal (C (Pi s SET)) tacT
>   return $ C (Pi s t)

Elim

> type Use = (NEU :<: TY) -> Tac VAL



> {-
> done :: Use
> done =
>   Use { runUse = \(v :<: t) ->
>     Tac { runTac = \root typ ->
>                    if equal (SET :>: (typ, t)) root then
>                       do
>                       check (typ :>: bquote (N v) root) root
>                       return (N v)
>                    else
>                        Nothing
>         }
>       }

> use :: REF -> Use -> Tac VAL
> use ref useR = 
>     Tac { runTac =
>             runTac $ runUse useR (P ref :<: pty ref)
>         }

> apply :: Tac VAL -> Use -> Use
> apply tacX use = 
>     Use { runUse = \(f :<: t) ->
>             Tac { runTac = \root typ ->
>                     case t of
>                       C (Pi s t) ->
>                         do
>                         xv <- runTac tacX root s
>                         runTac (runUse use (f :$ A xv :<: t $$ A xv))
>                                root
>                                typ
>                       _ -> Nothing
>                 }
>         }
> -}<commit_msg>Tactics: implement the use side of the Force.<commit_after>\section{Tactics}

%if False

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

> module Tactics where

Export |Tac| abstractly.

> import Control.Monad
> import Control.Applicative
> import Debug.Trace

> import BwdFwd
> import Rooty
> import Root
> import Tm
> import Rules

%endif

\subsection{The machinery}

> newtype Tac x = Tac { runTac :: Root -> TY -> Maybe x }

> instance Functor Tac where
>     fmap f g = Tac { runTac = \r t -> fmap f (runTac g r t) }

> instance Applicative Tac where
>     pure x = Tac { runTac = \_ _ -> Just x }
>     f <*> x = Tac { runTac = \r t ->
>                              do 
>                              f' <- runTac f r t
>                              x' <- runTac x r t
>                              return $ f' x' }

> instance Monad Tac where
>     return = pure
>     x >>= f = Tac { runTac = \r t -> 
>                                do 
>                                x <- runTac x r t
>                                runTac (f x) r t }

> instance Rooty Tac where
>     freshRef x tacF = Tac { runTac = Rooty.freshRef x (runTac . tacF) }
>     forkRoot s child dad = Tac { runTac = \root typ -> 
>                                           do 
>                                           c <- runTac child (room root s) typ
>                                           runTac (dad c) (roos root) typ
>                                }

\subsection{The tactic combinators}

This is the only place where we are allowed to play inside |Tac { ... }|.

\subsubsection{Setting goals}

This is a bit of Reader digest: |ask| and |runReader|.

> goal :: Tac TY
> goal = Tac { runTac = \root typ -> Just typ }

> subgoal :: TY -> Tac x -> Tac x
> subgoal typ tacX = 
>     Tac { runTac = \root typ' -> 
>           do
>           guard $ equal (SET :>: (typ, typ')) root 
>           runTac tacX root typ
>         }

\subsubsection{}

> discharge :: Rooty m => REF -> VAL -> m VAL
> discharge freshRef val = (|(\t -> L (H B0 "discharge" t)) 
>                            (quoteRef' [freshRef] val) |)

\subsection{Syntax-directed tacticals}

Intros

> lambda :: (VAL -> Tac VAL) -> Tac VAL
> lambda body = do
>   C (Pi s t) <- goal
>   Rooty.freshRef ("" :<: s) $
>                  \x -> 
>                      discharge x =<<
>                      subgoal (t $$ A (pval x)) (body (pval x))

This one should use the modified version of canTy:
       
> can :: Can (Tac VAL) -> Tac VAL
> can Set = do
>           SET <- goal
>           return SET
> can (Pi tacS tacT) = do
>   SET <- goal
>   s <- subgoal SET tacS
>   t <- subgoal (C (Pi s SET)) tacT
>   return $ C (Pi s t)

Elim

> type Use = (NEU :<: TY) -> Tac VAL

> done :: Use
> done (v :<: t) =
>     do
>       vv <- subgoal t $
>             (do
>               return $ N v)
>       return vv

> use :: REF -> Use -> Tac VAL
> use ref useR = 
>     do
>       useR (P ref :<: pty ref)

> apply :: Tac VAL -> Use -> Use
> apply tacX use (f :<: C (Pi s t)) = 
>     do
>     x <- subgoal s tacX
>     use (f :$ A x :<: t $$ A x)

{'fraction_non_alphanumeric': 0.12569158745921408, 'fraction_numerical': 0.0002837281883955171, 'mean_word_length': 1.3009138381201044, 'pattern_counts': {'":': 0, '<': 42, '<?xml version=': 0, '>': 244, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3987172', 'n_tokens_mistral': 2440, 'n_tokens_neox': 2291, 'n_words': 786}