diff options
| -rw-r--r-- | compiler/Config.ml | 2 | ||||
| -rw-r--r-- | compiler/Contexts.ml | 4 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.mli | 2 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.mli | 2 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.mli | 5 | ||||
| -rw-r--r-- | compiler/Pure.ml | 2 |
8 files changed, 11 insertions, 10 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index 0b8ee574..cc80e452 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -266,7 +266,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 {!Aeneas.PureMicroPasses.expression_contains_child_call_in_all_paths} + See the comments for {!val:PureMicroPasses.expression_contains_child_call_in_all_paths} for additional explanations. *) let filter_useless_monadic_calls = ref true diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index 0a6b27fd..a425d42b 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -396,11 +396,11 @@ let ctx_lookup_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value = in lookup_var ctx.env -(** Push an uninitialized variable (which thus maps to {!Values.Bottom}) *) +(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.Bottom}) *) let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx = ctx_push_var ctx var (mk_bottom var.var_ty) -(** Push a list of uninitialized variables (which thus map to {!Values.Bottom}) *) +(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.Bottom}) *) let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx = let vars = List.map (fun v -> (v, mk_bottom v.var_ty)) vars in ctx_push_vars ctx vars diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index c87aa6f2..a69b7b51 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -126,7 +126,7 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context) the synthesis (mostly by ending abstractions). [is_regular_return]: [true] if we reached a [Return] instruction (i.e., the - result is {!Return} or {!LoopReturn}). + result is {!constructor:Cps.statement_eval_res.Return} or {!constructor:Cps.statement_eval_res.LoopReturn}). [inside_loop]: [true] if we are *inside* a loop (result [EndContinue]). *) diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index a75f88fd..b9165ecb 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -96,6 +96,6 @@ val expand_symbolic_int : m_fun (** If this mode is activated through the [config], greedily expand the symbolic - values which need to be expanded. See {!C.config} for more information. + values which need to be expanded. See {!type:C.config} for more information. *) val greedy_expand_symbolic_values : C.config -> cm_fun diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 2b7241ba..2d900b7d 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -370,7 +370,7 @@ let destructure_new_abs (loop_id : V.LoopId.id) Note that we decompose only in the "fresh" abstractions (this is controled by the [old_aids] parameter). - TODO: how to factorize with {!destructure_abs}? + TODO: how to factorize with {!InterpreterBorrows.destructure_abs}? *) let decompose_shared_avalues (loop_id : V.LoopId.id) (old_aids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx = diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli index 602125c6..1afb9d53 100644 --- a/compiler/InterpreterProjectors.mli +++ b/compiler/InterpreterProjectors.mli @@ -10,7 +10,7 @@ open InterpreterBorrowsCore Apply a proj_borrows on a shared borrow. Note that when projecting over shared values, we generate - {!V.abstract_shared_borrows}, not {!V.avalue}s. + {!type:V.abstract_shared_borrows}, not {!type:V.avalue}s. Parameters: [regions] diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli index 789804b1..f28bf2ea 100644 --- a/compiler/InterpreterStatements.mli +++ b/compiler/InterpreterStatements.mli @@ -16,8 +16,9 @@ open InterpreterExpressions Drop all the local variables (which has the effect of moving their values to dummy variables, after ending the proper borrows of course) but the return variable, move the return value out of the return variable, remove all the - local variables (but preserve the abstractions!), remove the {!C.Frame} indicator - delimiting the current frame and handle the return value to the continuation. + local variables (but preserve the abstractions!), remove the + {!constructor:C.env_elem.Frame} indicator delimiting the current frame and + handle the return value to the continuation. If the boolean is false, we don't move the return value, and call the continuation with [None]. diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 521d60e6..1b0a6b5c 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -674,7 +674,7 @@ type fun_sig = { Non-decomposed ouputs (if the function can fail, but is not stateful): - [result T] - - [[result (T * T)] + - [[result (T * T)]] *) info : fun_sig_info; (** Additional information *) } |