Description
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!