You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
For now the backward functions can fail (they use the Result type). The problem comes from enumerations containing mutable borrows. For instance:
fnid<'a,T>(x:&'a mutOption<T>) -> Option<&'a mutT>{match x with
| None => None,
| Some(x) => Some(x),}
A pure model is given by (note that the backward function consumes an option):
defid {T} (x : Option T) : Result (Option T x (Option T -> Result (Option T))) :=
match x with
| none => ok (None, fun _ => ok None)
| some x =>
let back x :=
-- We need to extract the given back value from the optionmatch x with
| none =>
-- This case shouldn't happen if the backward function is called correctly,-- but yet we have to take it into account and are stuck.-- We have to fail somehow.
fail
| some x =>
-- Here we simply propagate
ok (some x)
ok (x, back)
The main issue comes from the fact that we sometimes have to match over an enumeration to extract a given back value from it. If the enumeration doesn't have the proper variant (which shouldn't happen if the backward function is used properly, but that we can't forbid just through typing) then we have an issue because we need to propagate something. However, we could use the fact that we still have the "old" values available to account for this case:
defid {T} (x : Option T) : Result (Option T x (Option T -> Option T)) :=
match x with
| none => ok (None, fun _ => None)
| some x =>
let back x' :=
-- We need to extract the given back value from the optionmatch x' with
| none => x -- Simply propagate the old value!
| some x' => some x' -- Normal case
(ok x, back)
The text was updated successfully, but these errors were encountered:
For now the backward functions can fail (they use the
Result
type). The problem comes from enumerations containing mutable borrows. For instance:A pure model is given by (note that the backward function consumes an option):
The main issue comes from the fact that we sometimes have to match over an enumeration to extract a given back value from it. If the enumeration doesn't have the proper variant (which shouldn't happen if the backward function is used properly, but that we can't forbid just through typing) then we have an issue because we need to propagate something. However, we could use the fact that we still have the "old" values available to account for this case:
The text was updated successfully, but these errors were encountered: