summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/ExtractToFStar.ml2
-rw-r--r--compiler/InterpreterBorrows.ml10
-rw-r--r--compiler/InterpreterExpansion.ml2
-rw-r--r--compiler/InterpreterPaths.ml6
-rw-r--r--compiler/InterpreterStatements.ml14
-rw-r--r--compiler/PureMicroPasses.ml2
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 *)