CN: Can sandbox be replaced with pure?

[dc-mak]

cerberus/backend/cn/lib/typing.ml

Lines 73 to 97 in 1425590

	let pure (m : 'a t) : 'a t =
	fun s ->
	Solver.push (Option.get s.solver);
	let outcome = match m s with Ok (a, _) -> Ok (a, s) | Error e -> Error e in
	Solver.pop (Option.get s.solver) 1;
	outcome
	let sandbox (m : 'a t) : 'a Resultat.t t =
	fun s ->
	let n = Solver.num_scopes (Option.get s.solver) in
	Solver.push (Option.get s.solver);
	let outcome =
	match m s with
	| Ok (a, _s') ->
	assert (Solver.num_scopes (Option.get s.solver) = n + 1);
	Solver.pop (Option.get s.solver) 1;
	Ok a
	| Error e ->
	let n' = Solver.num_scopes (Option.get s.solver) in
	assert (n' > n);
	Solver.pop (Option.get s.solver) (n' - n);
	Error e
	in
	Ok (outcome, s)

I feel like this could be

let sandbox (m : 'a t) : 'a Resultat.t t =
  fun s ->
  Ok (Result.map fst (pure m s), s)

But I am not sure.

[samcowger]

I am also not sure - I didn't write either of those functions, and I don't have a great understanding of solver scopes, so I don't think I'm the best person to address this. Perhaps @cp526 or @yav could weigh in?

For what it's worth, looking at them now, these two functions do seem to me to make different assumptions about how many new solver scopes an erroring action might introduce. pure seems to think that number is always 1, while sandbox seems to think that it could be 1 or more. I don't think both of these assumptions can hold.

[dc-mak]

I think that makes sense actually - I think a reasonable guess, and it might come down to intent: that pure is only for actions which are expected to succeed (not allowed to run anything afterwards) but sandbox is for actions which may succeed or fail.

In which case, I think it is worth strengthening the definition of pure to still leave the the typing monad/solver usable after a failed action.