io.iterate/forever and the state_t monad

Stream: metaprogramming / tactics

[Stanislas Polu]

Hi, I am new to meta-programming and currently blocked on making io.iterate/io.forever work with the sate_t monad. I have the following setup:

meta structure LeanREPLState : Type :=
(state: dict string tactic_state)

@[reducible]
meta def LeanREPL := state_t LeanREPLState io

And the following function:

meta def loop : LeanREPL unit := do {
  req ← (state_t.lift $ io.get_line >>= parse_request),
  res ← handle_request req,
  state_t.lift $ io.put_str_ln' $ format! "{(json.unparse ∘ LeanREPLResponse.to_json) res}",
  loop
}

Which is called from meta def main : io unit with:

 state_t.run loop σ₀ $>  ()

If run for long enough it hits a recursion limit, so I'd like to use io.iterate instead but I'm a bit lost on how to properly wire together io.iterate and state_t LeanREPLState io? (Thanks!!)

[Jason Rute]

@Stanislas Polu I made this MWE for you (ok, it isn't completely minimal). It does looping with both io.iterate and just a normal tail recursive loop using the state_t monad. However, unlike your example both approaches seem to handle loops of size one million without issue. The most substantial difference seems to be that my state_t monad is not built on top of the io monad. Instead it is just built ontop of option (or you could use except or except_t instead to get better exception handling). To handle io, either one does the io in the outer loop or does it deep inside the loop by using the tactic state which you have saved in your monad. (I give commented-out examples of printing IO with both approaches, but reading IO should work the same.)

[Jason Rute]

import system.io

meta structure my_state :=
(old_tactic_states : list tactic_state)
(current_tactic_state : tactic_state)

@[reducible]
meta def my_monad := state_t my_state option

/- Run skip tactic on current tactic state,
adding a new state to the stack,
print something to stdin
-/
meta def apply_skip_tactic : my_monad unit := do
  s <- get,
  let ts0 := s.current_tactic_state,

  let r := tactic.skip ts0,
  match r  with
  | result.success _ ts1 := do {
    -- update the stack with the new tactic state
    put { my_state .
      old_tactic_states := ts0 :: s.old_tactic_states,
      current_tactic_state := ts1
    }
  }
  | result.exception msg _ _ := do {
    -- fail using the failure mode of the underlying monad
    state_t.lift none
  }
  end,
  return ()


meta def print_ln (msg : string) : my_monad unit := do
  -- use stored tactic state to reach io monad to print
  -- must use the result in a supstantial way or it is
  -- removed from the code since lean thinks it is a noop
  s <- get,
  let ts0 := s.current_tactic_state,
  match tactic.unsafe_run_io (io.print_ln msg) ts0 with
  | result.success _ t0 := pure ()
  | result.exception _ _ _ := pure ()
  end

meta def loop1_aux : nat -> my_monad unit
| 0 := return ()
| (n+1) := do {
  --print_ln ("Loop 1 Iteration " ++ (repr n)),
  apply_skip_tactic,
  loop1_aux n
}

meta def loop1 (start_state : my_state) (interations : nat) : io unit := do
  match state_t.run (loop1_aux interations) start_state with
  | some (_, s) := io.print_ln ("Made it through loop 1 with " ++ (repr (s.old_tactic_states.length)) ++ " states")
  | none := io.print_ln "Loop 1 failed"
  end


meta def loop2_aux : (ℕ × my_state) -> io (option (ℕ × my_state))
| (0, _) := return none --exit loop
| (n+1, s0) := do {
  --io.print_ln ("Loop 2 Iteration " ++ (repr n)),
  match state_t.run apply_skip_tactic s0 with
  | none := do {
    io.print_ln "Loop failed",
    return none -- some problem with loop, exit
  }
  | some (_, s1) := return (some (n, s1))  -- keep looping
  end
}

meta def loop2 (start_state : my_state) (interations : nat) : io unit := do
  (_, s) <- io.iterate (interations, start_state) loop2_aux,
  io.print_ln ("Made it through loop 2 with " ++ (repr (s.old_tactic_states.length)) ++ " states")

meta def main : io unit := do {
  -- get a tactic state to work with
  ts <- io.run_tactic tactic.read,
  let start_state := {my_state . old_tactic_states := [], current_tactic_state := ts},

  loop1 start_state 1000000,
  loop2 start_state 1000000,
  return ()
}

[Jason Rute]

To see what happens, I modified my code above to use a state_t wrapped around io instead of option. The io.iterate version works fine and runs for a million iterations. The tail-recursive loop crashes with "Segmentation fault: 11". (It is still not the recursion error one sees with your code.)

[Jason Rute]

import system.io


meta structure my_state :=
(old_tactic_states : list tactic_state)
(current_tactic_state : tactic_state)

@[reducible]
meta def my_monad := state_t my_state io

/- Run skip tactic on current tactic state,
adding a new state to the stack,
print something to stdin
-/
meta def apply_skip_tactic : my_monad unit := do
  s <- get,
  let ts0 := s.current_tactic_state,

  let r := tactic.skip ts0,
  match r  with
  | result.success _ ts1 := do {
    -- update the stack with the new tactic state
    put { my_state .
      old_tactic_states := ts0 :: s.old_tactic_states,
      current_tactic_state := ts1
    }
  }
  | result.exception msg _ _ := do {
    -- fail using the failure mode of the underlying monad
    state_t.lift failure
  }
  end,
  return ()


meta def print_ln (msg : string) : my_monad unit := do
  -- use stored tactic state to reach io monad to print
  -- must use the result in a supstantial way or it is
  -- removed from the code since lean thinks it is a noop
  s <- get,
  let ts0 := s.current_tactic_state,
  match tactic.unsafe_run_io (io.print_ln msg) ts0 with
  | result.success _ t0 := pure ()
  | result.exception _ _ _ := pure ()
  end

meta def loop1_aux : nat -> my_monad unit
| 0 := return ()
| (n+1) := do {
  --print_ln ("Loop 1 Iteration " ++ (repr n)),
  apply_skip_tactic,
  loop1_aux n
}

meta def loop1 (start_state : my_state) (interations : nat) : io unit := do
  (u, s) <- state_t.run (loop1_aux interations) start_state,
  io.print_ln ("Made it through loop 1 with " ++ (repr (s.old_tactic_states.length)) ++ " states")

meta def loop2_aux : (ℕ × my_state) -> io (option (ℕ × my_state))
| (0, _) := return none --exit loop
| (n+1, s0) := do {
  --io.print_ln ("Loop 2 Iteration " ++ (repr n)),
  (u, s1) <- state_t.run apply_skip_tactic s0,
  return (some (n, s1))  -- keep looping
}

meta def loop2 (start_state : my_state) (interations : nat) : io unit := do
  (_, s) <- io.iterate (interations, start_state) loop2_aux,
  io.print_ln ("Made it through loop 2 with " ++ (repr (s.old_tactic_states.length)) ++ " states")

meta def main : io unit := do {
  -- get a tactic state to work with
  ts <- io.run_tactic tactic.read,
  let start_state := {my_state . old_tactic_states := [], current_tactic_state := ts},

  loop1 start_state 1000000,  -- segfaults
  loop2 start_state 1000000,
  return ()
}

[Stanislas Polu]

(deleted)

[Stanislas Polu]

Thanks! Super helpful :+1: