Getting rid of specret

[brabalan]

Since our functions never have different return types and we no longer have Coq_out_div, we can flatten specret into resultof. Concretely, resultof becomes

type 't resultof =
| Coq_result_some of (state * 't) [@f value]
| Coq_result_not_yet_implemented
| Coq_result_impossible
| Coq_result_bottom of state [@f state]

We no longer need specres, and result is simply a res resultof.

[brabalan]

This does not work: some functions may return something of non res type (for instance a string after a conversion), but may also throw (in that case they contain a res type with an abort restype). This can be seen in if_spec that uses if_abort.

let if_abort o k =
  match o with
  | Coq_out_div -> k ()
  | Coq_out_ter (s0, r) ->
    if restype_compare r.res_type Coq_restype_normal
    then (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
           s0
           ("[if_abort] received a normal result!")
    else k ()

let if_spec w k =
  if_result_some w (fun sp ->
    match sp with
    | Coq_specret_val (s0, a) -> k s0 a
    | Coq_specret_out o -> if_abort o (fun x -> res_out o))

[brabalan]

Alternative suggestion: replace the specret constructors as follows

type 't specret =
| Normal of state * 't [@f state, res]
| Abnormal of out [@f out]