diff options
author | Son Ho | 2022-11-11 16:34:09 +0100 |
---|---|---|
committer | Son Ho | 2022-11-11 16:34:09 +0100 |
commit | 9408cb898409da5588510233577a20468fac634f (patch) | |
tree | c18f0836bfbafc43b1df08fd5d050905ed57bf84 /compiler | |
parent | f58d3bcea55c06921ad332e6c820b96a5d9d2c37 (diff) |
Fix some issues with the comments
Diffstat (limited to '')
-rw-r--r-- | compiler/Assumed.ml | 2 | ||||
-rw-r--r-- | compiler/Config.ml | 14 | ||||
-rw-r--r-- | compiler/Cps.ml | 2 | ||||
-rw-r--r-- | compiler/InterpreterExpressions.mli | 6 | ||||
-rw-r--r-- | compiler/Pure.ml | 8 | ||||
-rw-r--r-- | compiler/PureMicroPasses.ml | 2 | ||||
-rw-r--r-- | compiler/PureUtils.ml | 2 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 5 |
8 files changed, 19 insertions, 22 deletions
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 7fba3c5c..e751d0ba 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -8,7 +8,7 @@ TODO: implementing the concrete evaluation functions for the assumed functions is really annoying (see - {!InterpreterStatements.eval_non_local_function_call_concrete}), + [InterpreterStatements.eval_non_local_function_call_concrete]), I think it should be possible, in most situations, to write bodies which model the behaviour of those unsafe functions. For instance, [Box::deref_mut] should simply be: diff --git a/compiler/Config.ml b/compiler/Config.ml index f446872c..1f91645b 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -1,6 +1,6 @@ (** Define the global configuration options *) -(** {0 Interpreter} *) +(** {1 Interpreter} *) (** Check that invariants are maintained whenever we execute a statement *) let check_invariants = ref true @@ -44,7 +44,7 @@ let allow_bottom_below_borrow = true *) let return_unit_end_abs_with_no_loans = true -(** {0 Translation} *) +(** {1 Translation} *) (** Controls whether we need to use a state to model the external world (I/O, for instance). @@ -59,7 +59,7 @@ let use_state = ref true (* TODO *) (st1, y) <-- f_fwd x st0; // st0 is the state upon calling f_fwd ... (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back - }] + ]} Otherwise, we generate code of the following shape: {[ @@ -110,7 +110,7 @@ let extract_decreases_clauses = ref true *) let extract_template_decreases_clauses = ref false -(** {0 Micro passes} *) +(** {1 Micro passes} *) (** Some provers like F* don't support the decomposition of return values in monadic let-bindings: @@ -141,8 +141,8 @@ let decompose_monadic_let_bindings = ref false This is useful when extracting to F*: the support for monadic definitions is not super powerful. - Note that when {!field:unfold_monadic_let_bindings} is true, setting - {!field:decompose_monadic_let_bindings} to true and only makes the code + Note that when {!unfold_monadic_let_bindings} is true, setting + {!decompose_monadic_let_bindings} to true and only makes the code more verbose. *) let unfold_monadic_let_bindings = ref false @@ -173,7 +173,7 @@ let unfold_monadic_let_bindings = ref false we later filter the useless *forward* calls in the micro-passes, where it is more natural to do. - See the comments for {!expression_contains_child_call_in_all_paths} + See the comments for {!PureMicroPasses.expression_contains_child_call_in_all_paths} for additional explanations. *) let filter_useless_monadic_calls = ref true diff --git a/compiler/Cps.ml b/compiler/Cps.ml index c2c0363b..de35198f 100644 --- a/compiler/Cps.ml +++ b/compiler/Cps.ml @@ -67,7 +67,7 @@ let comp_update (f : cm_fun) (g : C.eval_ctx -> C.eval_ctx) : cm_fun = (** This is just a test, to check that {!comp} is general enough to handle a case where a function must compute a value and give it to the continuation. - It happens for functions like {!InterpreterExpressions.eval_operand}. + It happens for functions like {!val:InterpreterExpressions.eval_operand}. Keeping this here also makes it a good reference, when one wants to figure out the signatures he should use for such a composition. diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli index a268ed1f..fa717041 100644 --- a/compiler/InterpreterExpressions.mli +++ b/compiler/InterpreterExpressions.mli @@ -17,7 +17,7 @@ open InterpreterPaths borrows*. This function doesn't reorganize the context to make sure we can read - the place. If needs be, you should call {!update_ctx_along_read_place} first. + the place. If needs be, you should call {!InterpreterPaths.update_ctx_along_read_place} first. *) val read_place : access_kind -> E.place -> (V.typed_value -> m_fun) -> m_fun @@ -64,8 +64,8 @@ val eval_operands : Transmits the computed rvalue to the received continuation. - Note that this function fails on {!E.Discriminant}: discriminant reads should - have been eliminated from the AST. + Note that this function fails on {!constructor:E.Discriminant}: discriminant + reads should have been eliminated from the AST. *) val eval_rvalue_not_global : C.config -> E.rvalue -> ((V.typed_value, eval_error) result -> m_fun) -> m_fun diff --git a/compiler/Pure.ml b/compiler/Pure.ml index fc18dbd3..fda2b3a6 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -48,7 +48,7 @@ let option_none_id = T.option_none_id type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty [@@deriving show, ord] -(** Ancestor for iter visitor for {!Pure.ty} *) +(** Ancestor for iter visitor for [ty] *) class ['self] iter_ty_base = object (_self : 'self) inherit [_] VisitorsRuntime.iter @@ -57,7 +57,7 @@ class ['self] iter_ty_base = method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> () end -(** Ancestor for map visitor for {!Pure.ty} *) +(** Ancestor for map visitor for [ty] *) class ['self] map_ty_base = object (_self : 'self) inherit [_] VisitorsRuntime.map @@ -498,9 +498,9 @@ and meta = type fun_effect_info = { stateful_group : bool; (** [true] if the function group is stateful. By *function group*, we mean - the set { forward function } U { backward functions }. + the set [{ forward function } U { backward functions }]. - We need this because the option {!Translate.eval_config.backward_no_state_update}: + We need this because of the option {!Config.backward_no_state_update}: if it is [true], then in case of a backward function {!stateful} is [false], but we might need to know whether the corresponding forward function is stateful or not. diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 1bf3b903..132dc02e 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1083,7 +1083,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = (** Decompose the monadic let-bindings. - See the explanations in {!config.decompose_monadic_let_bindings} + See the explanations in {!Config.decompose_monadic_let_bindings} *) let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl = diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 1ab3439c..0f16b5b4 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -73,7 +73,7 @@ let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty in fun id -> TypeVarId.Map.find id mp -(** Retrieve the list of fields for the given variant of a {!type_decl}. +(** Retrieve the list of fields for the given variant of a {!type:Pure.type_decl}. Raises [Invalid_argument] if the arguments are incorrect. *) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index fafcb348..a327c785 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -485,10 +485,7 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) : let abs_ids = list_ancestor_abstractions_ids ctx abs in List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids -(** Small utility. - - [backward_no_state_update]: see {!config} - *) +(** Small utility. *) let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id) (gid : T.RegionGroupId.id option) : fun_effect_info = match fun_id with |