refactor: incorporate an AxEffects field in SymContext, introduce SymM monad for SymContext state

[alexkeizer]

Description:

This turned into a rather big tech-debt removal PR. The primary focus is the removal of the duplication we had between SymContext tracking names of hypotheses, and AxEffects tracking Exprs for those same hypotheses.

• Added an effects : AxEffects field to SymContext, which stores the AxEffects for a single (non-aggregated!) step
• To make live easier, we introduce a SymM monad, so that we don't have to project out to the effect field every single every time (credits/blame go to @bollu for showing me the MonadStateOf trick).
• This allowed us to remove a bunch of fields of SymContext which had duplicates in AxEffects
• Also, it allowed us to move reflection of the PC out of explodeSteps and into prepareForNextStep (which was previously called SymContext.next),
• Finally, we extract ensureAtMostRunSteps and assertStepTheoremsGenerated functions out of the main body of sym_n

Testing:

What tests have been run? Did make all succeed for your changes? Was
conformance testing successful on an Aarch64 machine? yes

License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

[alexkeizer]

Hmm, for some reason having a logWarning in the following causes the yellow line to get stuck for a suspicuously long time right at the last line of the def. If I comment out the logWarning, the file build as fast as usual. @bollu any idea what's going on?

EDIT: I thought it might be something off with typeclass synthesis, but putting a #check logWarning (m := SymM) right before doesn't seem to invoke the Yellow Line of Doom (but specifying m := SymM still has the same stuck behaviour, so that's not it, either).

/-- Infer `state_prefix` and `curr_state_number` from the `state` name
as follows: if `state` is `s{i}` for some number `i` and a single character `s`,
then `s` is the prefix and `i` the number,
otherwise ignore `state`, log a warning, and start counting from `s1` -/
def inferStatePrefixAndNumber : SymM Unit := do
  let state ← AxEffects.getCurrentStateName
  let state := state.toString
  let tail := state.toSubstring.drop 1

  if let some currentStateNumber := tail.toNat? then
    modifyThe SymContext ({ · with
      state_prefix := (state.get? 0).getD 's' |>.toString,
      currentStateNumber })
  else
    logWarning ""
    modifyThe SymContext ({ · with
      state_prefix := "s",
      currentStateNumber := 1 })

[bollu]

@alexkeizer and I minimized this, and will be sending an issue upstream soon. In the meantime, we also have a workaround so it's all good :)

[alexkeizer]

I pushed the workaround, @shigoel this is once more ready for review (and at the top of the priority queue from my side)

[shigoel]

Thanks!