diff options
| -rw-r--r-- | compiler/ExtractToFStar.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 10 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 6 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 14 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 2 |
6 files changed, 19 insertions, 17 deletions
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml index a77e3df3..b44b8f25 100644 --- a/compiler/ExtractToFStar.ml +++ b/compiler/ExtractToFStar.ml @@ -857,7 +857,7 @@ let extract_global (ctx : extraction_ctx) (fmt : F.formatter) (id : A.GlobalDeclId.id) : unit = F.pp_print_string fmt (ctx_get_global id ctx) -(** [inside]: see [extract_ty]. +(** [inside]: see {!extract_ty}. As a pattern can introduce new variables, we return an extraction context updated with new bindings. diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 30c3b221..16f68d9e 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -224,7 +224,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) Ok (ctx, !replaced_bc) with FoundPriority outers -> Error outers -(** Auxiliary function to end borrows. See [give_back]. +(** Auxiliary function to end borrows. See {!give_back}. When we end a mutable borrow, we need to "give back" the value it contained to its original owner by reinserting it at the proper position. @@ -475,7 +475,7 @@ let give_back_symbolic_value (_config : C.config) in update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx -(** Auxiliary function to end borrows. See [give_back]. +(** Auxiliary function to end borrows. See {!give_back}. This function is similar to {!give_back_value} but gives back an {!V.avalue} (coming from an abstraction). @@ -577,7 +577,7 @@ let give_back_avalue_to_same_abstraction (_config : C.config) (* Return *) ctx -(** Auxiliary function to end borrows. See [give_back]. +(** Auxiliary function to end borrows. See {!give_back}. When we end a shared borrow, we need to remove the borrow id from the list of borrows to the shared value. @@ -704,7 +704,7 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id) assert !r; { ctx with env } -(** Auxiliary function: see [end_borrow] *) +(** Auxiliary function: see {!end_borrow} *) let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) (ctx : C.eval_ctx) : C.eval_ctx = (* Debug *) @@ -1430,7 +1430,7 @@ let end_outer_borrow config : V.BorrowId.id -> cm_fun = let end_outer_borrows config : V.BorrowId.Set.t -> cm_fun = end_borrows config [] None -(** Helper function: see [activate_inactivated_mut_borrow]. +(** Helper function: see {!activate_inactivated_mut_borrow}. This function updates the shared loan to a mutable loan (we then update the borrow with another helper). Of course, the shared loan must contain diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index 8caa828e..9a944428 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -431,7 +431,7 @@ let expand_symbolic_value_borrow (config : C.config) Apply a branching symbolic expansion to a context and execute all the branches. Note that the expansion is optional for every branch (this is - used for integer expansion: see [expand_symbolic_int]). + used for integer expansion: see {!expand_symbolic_int}). [see_cf_l]: list of pairs (optional symbolic expansion, continuation) *) diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 28e81dc6..1cd27b31 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -620,9 +620,11 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) [end_borrows]: - if true: end all the loans and borrows we find, starting with the outer - ones. This is used when evaluating the [drop] statement (see [drop_value]) - - if false: only end the outer loans. This is used by [assign_to_place] + ones. This is used when evaluating the {!LlbcAst.Drop} statement (see {!InterpreterStatements.drop_value}) + - if false: only end the outer loans. This is used by {!InterpreterStatements.assign_to_place} or to drop the loans in the local variables when popping a frame. + TODO: remove this option, it is actually not used anymore (should always be + false). Note that we don't do what is defined in the formalization: we move the value to a temporary dummy value, then explore this value and end the diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 45d2aab2..f935734e 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -413,13 +413,13 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun = in comp cf_pop cf_assign -(** Auxiliary function - see [eval_non_local_function_call] *) +(** Auxiliary function - see {!eval_non_local_function_call} *) let eval_replace_concrete (_config : C.config) (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun = fun _cf _ctx -> raise Unimplemented -(** Auxiliary function - see [eval_non_local_function_call] *) +(** Auxiliary function - see {!eval_non_local_function_call} *) let eval_box_new_concrete (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun = fun cf ctx -> @@ -459,7 +459,7 @@ let eval_box_new_concrete (config : C.config) | _ -> raise (Failure "Inconsistent state") (** Auxiliary function which factorizes code to evaluate [std::Deref::deref] - and [std::DerefMut::deref_mut] - see [eval_non_local_function_call] *) + and [std::DerefMut::deref_mut] - see {!eval_non_local_function_call} *) let eval_box_deref_mut_or_shared_concrete (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) (is_mut : bool) : cm_fun = @@ -504,19 +504,19 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config) comp cf_borrow cf_move cf ctx | _ -> raise (Failure "Inconsistent state") -(** Auxiliary function - see [eval_non_local_function_call] *) +(** Auxiliary function - see {!eval_non_local_function_call} *) let eval_box_deref_concrete (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun = let is_mut = false in eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut -(** Auxiliary function - see [eval_non_local_function_call] *) +(** Auxiliary function - see {!eval_non_local_function_call} *) let eval_box_deref_mut_concrete (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun = let is_mut = true in eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut -(** Auxiliary function - see [eval_non_local_function_call]. +(** Auxiliary function - see {!eval_non_local_function_call}. [Box::free] is not handled the same way as the other assumed functions: - in the regular case, whenever we need to evaluate an assumed function, @@ -556,7 +556,7 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) cc cf ctx | _ -> raise (Failure "Inconsistent state") -(** Auxiliary function - see [eval_non_local_function_call] *) +(** Auxiliary function - see {!eval_non_local_function_call} *) let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun = diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 3edae38a..5da07e55 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -100,7 +100,7 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator = let id = obj#visit_expression () body.body.e () in VarId.generator_from_incr_id id -(** "pretty-name context": see [compute_pretty_names] *) +(** "Pretty-Name context": see {!compute_pretty_names} *) type pn_ctx = { pure_vars : string VarId.Map.t; (** Information about the pure variables used in the synthesized program *) |