Wingman recursion performance bug

[Tarmean]

I'm new to haskell-language-server and wanted to stare at some code before trying to write some myself to get used to the patterns. While staring, I noticed that the current (operational) behavior of peek as defined here is a bit suspect.
Notably, it seems like it would often use the continuation non-linearly.

peek :: (ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
peek k = tactic $ \j -> Subgoal ((), j) $ \e -> proofState (k e) j

My current understanding is that monadic binds for Tactic and Rule are basically substituting of subgoals and extracts respectively with new ProofStates . So if peek is used like

peek $ \e -> if p e then pure () else empty

this uses substitution over subgoals and reduces roughly like

peek (\e -> if p e then pure () else empty) >>= f
Subgoal ((), j) (\e -> if p e then Subgoal ((), j) Axiom  else empty) >>= f
substExtract (\e -> (if p e then Subgoal ((), j) Axiom else empty) >>= f) (f ((), j))
substExtract (\e -> if p e then f ((),j) else empty) (f ((), j))

The important bit is that f ((), j) occurs twice so everything after peek will be executed twice. Nested peek continuations would be exponential, but only recursion currently uses it.

The direct solution is to use Axiom as cut:

peek :: Applicative m => (ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
peek k = tactic $ \j -> Subgoal ((), j) $ \e -> proofState (k e) j *> Axiom e

Though this means changes to monadic state in peek are forgotten, which is probably fine. Alternatively something like this might be more intuitive? I'm not sure.

peek :: Functor m => (ext -> Maybe ext) -> TacticT jdg ext err s m ()
peek k = tactic $ \j -> Subgoal ((), j) $ \e -> case k e of
  Just e' -> Axiom e'
  Nothing -> Empty

To validate manually this hack works for me:

{-# INLINE checkOnce #-}
checkOnce :: Applicative m  => ((a -> m a) -> m b) -> m b
checkOnce k = unsafePerformIO $ do
   r <- newIORef False
   let
     {-# NOINLINE go #-}
     go a = unsafePerformIO $ do
               o <- readIORef r
               if o
               then error "entered checkOnce twice"
               else pure a <$ writeIORef r True
   pure (k go)

recursion :: TacticsM ()
-- TODO(sandy): This tactic doesn't fire for the @AutoThetaFix@ golden test,
-- presumably due to running afoul of 'requireConcreteHole'. Look into this!
recursion = requireConcreteHole $ tracing "recursion" $ do
  defs <- getCurrentDefinitions
  attemptOn (const defs) $ \(name, ty) -> markRecursion $ do
    checkOnce $ \checkin -> do
        -- Peek allows us to look at the extract produced by this block.
        peek $ \ext -> do
          jdg <- goal
          let pat_vals = jPatHypothesis jdg
          -- Make sure that the recursive call contains at least one already-bound
          -- pattern value. This ensures it is structurally smaller, and thus
          -- suggests termination.
          unless (any (flip M.member pat_vals) $ syn_used_vals ext) empty

        let hy' = recursiveHypothesis defs
        ctx <- ask
        checkin ctx
        localTactic (apply Saturated $ HyInfo name RecursivePrv ty) (introduce ctx hy')
          <@> fmap (localTactic assumption . filterPosition name) [0..]

I haven't figured out how the tests infrastructure works, yet, so I am not sure how to turn this into a sensible test case.

Also, Wingman is really cool!

[jneira]

Wow, thanks for this issue based in a previous code analysis and a posible solution!
I hope @isovector will be happy to review the issue and help to make progress in your investigation.

[isovector]

@Tarmean this an extremely impressive analysis --- kudos to you!

In general, refinery version 3 (the tactics library) does poorly in "speculative" situations like peek. The underlying issue is that there's no good way to reuse the work we performed in conducting the analysis. This is fixed in refinery v4, which comes with a new substitution monad, and where peek is just a library function. I haven't gotten a chance to upgrade yet, but maybe that will be my project for today.

I haven't figured out how the tests infrastructure works

All of the Wingman tests are under the hls-tactics-plugin:tests cabal component, and are primarily golden tests --- which is to say, we test the output of running tactics, rather than anything more clever. Testing stuff like this is going to be hard; maybe a benchmark would be more appropriate?