doc(engine/phases/question-marks): add some documentation

cryspen · Jan 18, 2024 · 65c8f5b · 65c8f5b
1 parent ed38a3e
commit 65c8f5b
Show file tree

Hide file tree

Showing 6 changed files with 135 additions and 81 deletions.
diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
@@ -346,12 +346,10 @@ functor
       (* ControlFlow *)
       | Break of { e : expr; label : string option; witness : F.break * F.loop }
       | Return of { e : expr; witness : F.early_exit }
-      | QuestionMark of {
-          e : expr;
-          return_typ : ty;
-              (** [converted_typ] is the converted type: when you do [e?], a convertion might be inserted by Rust on the fly (e.g. [Something::from_residual(e)]) *)
-          witness : F.question_mark;
-        }
+      | QuestionMark of { e : expr; return_typ : ty; witness : F.question_mark }
+          (** The expression `e?`. In opposition to Rust, no implicit
+      coercion is applied on the (potential) error payload of
+      `e`. Coercion should be made explicit within `e`. *)
       | Continue of {
           e : (F.state_passing_loop * expr) option;
           label : string option;

diff --git a/engine/lib/phases/phase_reconstruct_question_marks.ml b/engine/lib/phases/phase_reconstruct_question_marks.ml
@@ -30,12 +30,10 @@ module%inlined_contents Make (FA : Features.T) = struct
 
       open A
 
+      (** The types supported for [e] in a [e?] expression *)
       type qm_kind = QMResult of { success : ty; error : ty } | QMOption of ty
 
-      let return_typ_of_qm_kind = function
-        | QMResult { error; _ } -> error
-        | QMOption _ -> UA.unit_typ
-
+      (** Interpret a type [t] as a [qm_kind] *)
       let qm_kind_of_typ span (t : ty) : qm_kind =
         let is_result = Global_ident.eq_name Core__result__Result in
         let is_option = Global_ident.eq_name Core__option__Option in
@@ -49,19 +47,9 @@ module%inlined_contents Make (FA : Features.T) = struct
                 got: "
               ^ [%show: ty] t)
 
-      type t = {
-        start : expr;
-        end_ : expr;
-        var : local_ident;
-        var_typ : ty;
-        body : expr;
-        state : loop_state option;
-        label : string option;
-        witness : FA.loop;
-      }
-      [@@deriving show]
-
-      (** expect residual impl result 27 *)
+      (** Expects [impl] to be an impl. expr. for the trait
+      `std::ops::FromResidual` for the type [Result<_, _>], and
+      extract its parent [From] impl expr *)
       let expect_residual_impl_result (impl : impl_expr) : impl_expr option =
         match impl with
         | ImplApp
@@ -70,25 +58,30 @@ module%inlined_contents Make (FA : Features.T) = struct
             Some from_impl
         | _ -> None
 
+      (** Expects [t] to be [Result<S, E>], and returns [(S, E)] *)
       let expect_result_type (t : ty) : (ty * ty) option =
         match t with
         | TApp { ident; args = [ GType s; GType e ] }
           when Global_ident.eq_name Core__result__Result ident ->
             Some (s, e)
         | _ -> None
 
+      (** Construct [Result<S,E>] *)
       let make_result_type (success : ty) (error : ty) : ty =
         let ident = Global_ident.of_name Type Core__result__Result in
         TApp { ident; args = [ GType success; GType error ] }
 
-      (** Retype a `Err::<_, E>(x)` literal, as `Err::<success, E>(x)` *)
+      (** Retype a [Err::<_, E>(x)] literal, as [Err::<success, E>(x)] *)
       let retype_err_literal (e : expr) (success : ty) (error : ty) =
         match e.e with
         | Construct { constructor; _ }
           when Global_ident.eq_name Core__result__Result__Err constructor ->
             { e with typ = make_result_type success error }
         | _ -> e
 
+      (** [map_err e error_dest impl] creates the expression
+      [e.map_err(from)] with the proper types and impl
+      informations. *)
       let map_err (e : expr) (error_dest : ty) impl : expr option =
         let* success, error_src = expect_result_type e.typ in
         let* impl = expect_residual_impl_result impl in
@@ -103,6 +96,9 @@ module%inlined_contents Make (FA : Features.T) = struct
         in
         Some call
 
+      (** [extract e] returns [Some (x, ty)] if [e] was a `y?`
+      desugared by rustc. `y` is `x` plus possibly a coercion. [ty] is
+      the return type of the function. *)
       let extract (e : expr) : (expr * ty) option =
         let extract_return (e : expr) =
           match e.e with

diff --git a/engine/lib/phases/phase_reconstruct_question_marks.mli b/engine/lib/phases/phase_reconstruct_question_marks.mli
@@ -1,9 +1,33 @@
+(** In THIR, there are no construct for question marks. Instead, Rustc
+desugars `e?` into the following:
+
+{@rust[
+match core::ops::try_trait::branch(y) {
+    core::ops::control_flow::Break(residual) => {
+        never_to_any(
+            {return core::ops::try_trait::from_residual(residual)},
+        )
+    }
+    core::ops::control_flow::Continue(val) => val,
+})
+]}
+
+This phase does the opposite rewrite.
+
+While `e?` in Rust might implies an implicit coercion, in our AST, a
+question mark is expected to already be of the right type. This phase
+inlines a coercion (of the shape `x.map_err(from)`, in the case of a
+`Result`).
+*)
+
 open! Prelude
 
+(** This phase can be applied to any feature set. *)
 module Make (F : Features.T) : sig
   include module type of struct
     module FA = F
 
+    (** This phase outputs an AST with question marks. *)
     module FB = struct
       include F
       include Features.On.Question_mark

diff --git a/engine/lib/utils.ml b/engine/lib/utils.ml
@@ -23,6 +23,8 @@ let tup2 a b = (a, b)
 let ( let* ) x f = Option.bind ~f x
 let some_if_true = function true -> Some () | _ -> None
 
+(** [let*? () = guard in body] acts as a guard: if [guard] holds, then
+[body] is executed, otherwise [None] is returned. *)
 let ( let*? ) (type a) (x : bool) (f : unit -> a option) =
   let* () = some_if_true x in
   f ()

diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
@@ -18,10 +18,45 @@ info:
       stderr: true
       stdout: true
 ---
-exit = 0
+exit = 101
 stderr = '''
 Compiling side-effects v0.1.0 (WORKSPACE_ROOT/side-effects)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+error[E0428]: the name `direct_result_1` is defined multiple times
+  --> side-effects/src/lib.rs:73:1
+   |
+67 | fn direct_result_1(y: Result<(), u32>) -> Result<i8, u32> {
+   | --------------------------------------------------------- previous definition of the value `direct_result_1` here
+...
+73 | fn direct_result_1(y: Result<i8, u16>) -> Result<i8, u32> {
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `direct_result_1` redefined here
+   |
+   = note: `direct_result_1` must be defined only once in the value namespace of this module
+
+error[E0061]: this enum variant takes 1 argument but 0 arguments were supplied
+   --> side-effects/src/lib.rs:69:5
+    |
+69  |     Ok()
+    |     ^^-- an argument of type `i8` is missing
+    |
+note: tuple variant defined here
+   --> /nix/store/bax026mb31q65yyh0c2jrwx5xynkhhs4-rust-default-1.72.0-nightly-2023-06-02/lib/rustlib/src/rust/library/core/src/result.rs:506:5
+    |
+506 |     Ok(#[stable(feature = "rust1", since = "1.0.0")] T),
+    |     ^^
+help: provide the argument
+    |
+69  |     Ok(/* i8 */)
+    |       ~~~~~~~~~~
+
+error: While trying to reach a body's THIR defintion, got a typechecking error.
+  --> side-effects/src/lib.rs:67:1
+   |
+67 | fn direct_result_1(y: Result<(), u32>) -> Result<i8, u32> {
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Some errors have detailed explanations: E0061, E0428.
+For more information about an error, try `rustc --explain E0061`.
+error: could not compile `side-effects` (lib) due to 3 previous errors'''
 
 [stdout]
 diagnostics = []
@@ -36,22 +71,18 @@ open FStar.Mul
 let add3 (x y z: u32) : u32 =
   Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add x y <: u32) z
 
-let direct_result_1_ (y: Core.Result.t_Result i8 u32) : Core.Result.t_Result i8 u32 =
+let direct_result_1_ (_: Prims.unit) : Rust_primitives.Hax.t_Never =
+  Rust_primitives.Hax.failure "(AST import) Fatal error: something we considered as impossible occurred! Please report this by submitting an issue on GitHub!\nDetails: [import_thir:literal] got an error literal: this means the Rust compiler or Hax's frontend probably reported errors above.\n"
+    "{ Types.attributes = [];\n  contents =\n  Types.Literal {\n    lit =\n    { Types.node = Types.Err;\n      span =\n      { Types.filename =\n        (Types.Real (Types.LocalPath \"side-effects/src/lib.rs\"));\n        hi = { Types.col = \"0\"; line = \"1\" };\n        lo = { Types.col = \"0\"; line = \"1\" } }\n      };\n    neg = false};\n  hir_id = None;\n  span =\n  { Types.filename = (Types.Real (Types.LocalPath \"side-effects/src/lib.rs\"));\n    hi = { Types.col = \"57\"; line = \"67\" };\n    lo = { Types.col = \"0\"; line = \"67\" } };\n  ty = Types.Never }"
+
+let direct_result_1_1 (y: Core.Result.t_Result i8 u16) : Core.Result.t_Result i8 u32 =
   Rust_primitives.Hax.Control_flow_monad.Mresult.run (let| hoist1:i8 =
-        Core.Result.impl__map_err y (Core.Convert.f_from <: u32 -> u32)
+        Core.Result.impl__map_err y (Core.Convert.f_from <: u16 -> u32)
       in
       Core.Result.Result_Ok (Core.Result.Result_Ok hoist1 <: Core.Result.t_Result i8 u32)
       <:
       Core.Result.t_Result (Core.Result.t_Result i8 u32) u32)
 
-let direct_result_2_ (y: Core.Result.t_Result Prims.unit u32) : Core.Result.t_Result i8 u32 =
-  Rust_primitives.Hax.Control_flow_monad.Mresult.run (let| _:Prims.unit =
-        Core.Result.impl__map_err y (Core.Convert.f_from <: u32 -> u32)
-      in
-      Core.Result.Result_Ok (Core.Result.Result_Ok 1y <: Core.Result.t_Result i8 u32)
-      <:
-      Core.Result.t_Result (Core.Result.t_Result i8 u32) u32)
-
 let early_returns (x: u32) : u32 =
   Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! _:Prims.unit =
         if x >. 3ul
@@ -96,20 +127,6 @@ let early_returns (x: u32) : u32 =
       <:
       Core.Ops.Control_flow.t_ControlFlow u32 u32)
 
-let into_err (x: u8) : Core.Result.t_Result u8 u64 =
-  Rust_primitives.Hax.Control_flow_monad.Mresult.run (let| _:Prims.unit =
-        if x >. 200uy
-        then
-          Core.Result.impl__map_err (Core.Result.Result_Err x <: Core.Result.t_Result Prims.unit u8)
-            (Core.Convert.f_from <: u8 -> u64)
-        else Core.Result.Result_Ok () <: Core.Result.t_Result Prims.unit u64
-      in
-      Core.Result.Result_Ok
-      (Core.Result.Result_Ok (Core.Num.impl__u8__wrapping_add x 54uy) <: Core.Result.t_Result u8 u64
-      )
-      <:
-      Core.Result.t_Result (Core.Result.t_Result u8 u64) u64)
-
 let local_mutation (x: u32) : u32 =
   let y:u32 = 0ul in
   let x:u32 = Core.Num.impl__u32__wrapping_add x 1ul in
@@ -232,27 +249,35 @@ type t_Bar = {
   f_b:(t_Array (bool & bool) (sz 6) & bool)
 }
 
-let monad_lifting (_: Prims.unit) : Core.Result.t_Result t_A t_B =
-  Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! hoist33:t_A =
-        Core.Ops.Control_flow.ControlFlow_Continue
-        (Core.Result.impl__map_err (Core.Result.Result_Err (B <: t_B)
-              <:
-              Core.Result.t_Result t_A t_B)
-            (Core.Convert.f_from <: t_B -> t_B))
+let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B =
+  Rust_primitives.Hax.Control_flow_monad.Mexception.run (if x >. 123uy <: bool
+      then
+        let! hoist33:t_A =
+          Core.Ops.Control_flow.ControlFlow_Continue
+          (Core.Result.impl__map_err (Core.Result.Result_Err (B <: t_B)
+                <:
+                Core.Result.t_Result t_A t_B)
+              (Core.Convert.f_from <: t_B -> t_B))
+          <:
+          Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_A t_B)
+            (Core.Result.t_Result t_A t_B)
+        in
+        let hoist34:Core.Result.t_Result t_A t_B =
+          Core.Result.Result_Ok hoist33 <: Core.Result.t_Result t_A t_B
+        in
+        let! hoist35:Rust_primitives.Hax.t_Never =
+          Core.Ops.Control_flow.ControlFlow.v_Break hoist34
+        in
+        Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist35)
         <:
         Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_A t_B)
           (Core.Result.t_Result t_A t_B)
-      in
-      let hoist34:Core.Result.t_Result t_A t_B =
-        Core.Result.Result_Ok hoist33 <: Core.Result.t_Result t_A t_B
-      in
-      let! hoist35:Rust_primitives.Hax.t_Never =
-        Core.Ops.Control_flow.ControlFlow.v_Break hoist34
-      in
-      Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist35)
-      <:
-      Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_A t_B)
-        (Core.Result.t_Result t_A t_B))
+      else
+        Core.Ops.Control_flow.ControlFlow_Continue
+        (Core.Result.Result_Ok (A <: t_A) <: Core.Result.t_Result t_A t_B)
+        <:
+        Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_A t_B)
+          (Core.Result.t_Result t_A t_B))
 
 type t_Foo = {
   f_x:bool;

diff --git a/tests/side-effects/src/lib.rs b/tests/side-effects/src/lib.rs
@@ -1,8 +1,11 @@
 #![allow(dead_code)]
+
+/// Helper function
 fn add3(x: u32, y: u32, z: u32) -> u32 {
     x.wrapping_add(y).wrapping_add(z)
 }
 
+/// Exercise local mutation with control flow and loops
 fn local_mutation(mut x: u32) -> u32 {
     let mut y = 0;
     if {
@@ -39,6 +42,7 @@ fn local_mutation(mut x: u32) -> u32 {
     }
 }
 
+/// Exercise early returns with control flow and loops
 fn early_returns(mut x: u32) -> u32 {
     return (123u32.wrapping_add(
         if {
@@ -59,14 +63,18 @@ fn early_returns(mut x: u32) -> u32 {
     .wrapping_add(x);
 }
 
-fn direct_result_1(y: Result<i8, u32>) -> Result<i8, u32> {
-    Ok(y?)
-}
-fn direct_result_2(y: Result<(), u32>) -> Result<i8, u32> {
+/// Question mark without error coercion
+fn direct_result_1(y: Result<(), u32>) -> Result<i8, u32> {
     y?;
-    Ok(1)
+    Ok()
+}
+
+/// Question mark with an error coercion
+fn direct_result_1(y: Result<i8, u16>) -> Result<i8, u32> {
+    Ok(y?)
 }
 
+/// Test question mark on `Option`s with some control flow
 fn options(x: Option<u8>, y: Option<u8>, z: Option<u64>) -> Option<u8> {
     let v = match (if x? > 10 {
         Some(x?.wrapping_add(3))
@@ -80,6 +88,7 @@ fn options(x: Option<u8>, y: Option<u8>, z: Option<u64>) -> Option<u8> {
     Some(v.wrapping_add(x?).wrapping_add(y?))
 }
 
+/// Test question mark on `Result`s with local mutation
 fn question_mark(mut x: u32) -> Result<u32, u32> {
     if x > 40u32 {
         let mut y = 0;
@@ -98,15 +107,13 @@ fn question_mark(mut x: u32) -> Result<u32, u32> {
 struct A;
 struct B;
 
-fn monad_lifting() -> Result<A, B> {
-    return Ok(Err(B)?);
-}
-
-fn into_err(x: u8) -> Result<u8, u64> {
-    if x > 200 {
-        Err(x)?
+/// Combine `?` and early return
+fn monad_lifting(x: u8) -> Result<A, B> {
+    if x > 123 {
+        return Ok(Err(B)?);
+    } else {
+        Ok(A)
     }
-    Ok(x.wrapping_add(54))
 }
 
 struct Bar {
@@ -119,6 +126,8 @@ struct Foo {
     z: [Bar; 6],
     bar: Bar,
 }
+
+/// Test assignation on non-trivial places
 fn assign_non_trivial_lhs(mut foo: Foo) -> Foo {
     foo.x = true;
     foo.bar.a = true;