diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Config.ml | 2 | ||||
| -rw-r--r-- | compiler/Contexts.ml | 8 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 6 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 12 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.mli | 2 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsCore.ml | 8 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.mli | 6 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.mli | 2 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.mli | 2 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 4 | ||||
| -rw-r--r-- | compiler/Pure.ml | 4 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/Substitute.ml | 2 | ||||
| -rw-r--r-- | compiler/SymbolicAst.ml | 4 | ||||
| -rw-r--r-- | compiler/TypesUtils.ml | 4 |
16 files changed, 35 insertions, 35 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index 1a00656d..364ef748 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -289,7 +289,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 {!val:PureMicroPasses.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/Contexts.ml b/compiler/Contexts.ml index a2ae4f16..c93bb213 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -112,7 +112,7 @@ let reset_global_counters () = fun_call_id_counter := FunCallId.generator_zero; dummy_var_id_counter := DummyVarId.generator_zero -(** Ancestor for {!env} iter visitor *) +(** Ancestor for {!type:env} iter visitor *) class ['self] iter_env_base = object (_self : 'self) inherit [_] iter_abs @@ -120,7 +120,7 @@ class ['self] iter_env_base = method visit_dummy_var_id : 'env -> dummy_var_id -> unit = fun _ _ -> () end -(** Ancestor for {!env} map visitor *) +(** Ancestor for {!type:env} map visitor *) class ['self] map_env_base = object (_self : 'self) inherit [_] map_abs @@ -423,11 +423,11 @@ let erase_regions (ty : ty) : ty = in v#visit_ty () ty -(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.Bottom}) *) +(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *) let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx = ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty)) -(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.Bottom}) *) +(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *) let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx = let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in ctx_push_vars ctx vars diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 1ca68120..85ab1112 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -311,7 +311,7 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string) the same name because Lean uses the typing information to resolve the ambiguities. - This map complements the {!names_map}, which checks for collisions. + This map complements the {!type:names_map}, which checks for collisions. *) type unsafe_names_map = { id_to_name : string IdMap.t } @@ -1639,7 +1639,7 @@ let ctx_compute_trait_type_clause_name (ctx : extraction_ctx) function is an assumed function or a local function - function basename - the number of loops in the parent function. This is used for - the same purpose as in {!field:llbc_name}. + the same purpose as in [llbc_name]. - loop identifier, if this is for a loop *) let ctx_compute_termination_measure_name (ctx : extraction_ctx) @@ -1668,7 +1668,7 @@ let ctx_compute_termination_measure_name (ctx : extraction_ctx) function is an assumed function or a local function - function basename - the number of loops in the parent function. This is used for - the same purpose as in {!field:llbc_name}. + the same purpose as in [llbc_name]. - loop identifier, if this is for a loop *) let ctx_compute_decreases_proof_name (ctx : extraction_ctx) diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index c6212d31..ca9984be 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -213,7 +213,7 @@ let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool = - in Lean, groups of mutually recursive definitions must end with "end" - in HOL4 (in most situations) the whole group must be within a `Define` command - Calls to {!extract_fun_decl} should be inserted between calls to + Calls to {!Extract.extract_fun_decl} should be inserted between calls to {!start_fun_decl_group} and {!end_fun_decl_group}. TODO: maybe those [{start/end}_decl_group] functions are not that much a good diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index b13d545c..44f85d0a 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -924,7 +924,7 @@ let remove_intersecting_aproj_borrows_shared (regions : RegionId.Set.t) [subst]: takes as parameters the abstraction in which we perform the substitution and the list of given back values at the projector of - loans where we perform the substitution (see the fields in {!AProjLoans}). + loans where we perform the substitution (see the fields in {!Values.AProjLoans}). Note that the symbolic value at this place is necessarily equal to [sv], which is why we don't give it as parameters. *) @@ -970,13 +970,13 @@ let update_intersecting_aproj_loans (proj_regions : RegionId.Set.t) (* Return *) ctx -(** Helper function: lookup an {!AProjLoans} by using an abstraction id and a +(** Helper function: lookup an {!constructor:Values.aproj.AProjLoans} by using an abstraction id and a symbolic value. - + We return the information from the looked up projector of loans. See the - fields in {!AProjLoans} (we don't return the symbolic value, because it + fields in {!constructor:Values.aproj.AProjLoans} (we don't return the symbolic value, because it is equal to [sv]). - + Sanity check: we check that there is exactly one projector which corresponds to the couple (abstraction id, symbolic value). *) @@ -1115,7 +1115,7 @@ let update_aproj_borrows (abs_id : AbstractionId.id) (sv : symbolic_value) (** Helper function: might break invariants. - Converts an {!AProjLoans} to an {!AEndedProjLoans}. The projector is identified + Converts an {!Values.aproj.AProjLoans} to an {!Values.aproj.AEndedProjLoans}. The projector is identified by a symbolic value and an abstraction id. *) let update_aproj_loans_to_ended (abs_id : AbstractionId.id) diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index 4be1fd24..b545f979 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -79,6 +79,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 {!type:config} for more information. + values which need to be expanded. See {!type:Contexts.config} for more information. *) val greedy_expand_symbolic_values : config -> cm_fun diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index d14230c6..ca1f8f31 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -41,10 +41,10 @@ type abs_borrows_loans_maps = { borrow_loan_to_abs : AbstractionId.Set.t BorrowId.Map.t; } -(** See {!InterpreterLoopsMatchCtxs.MakeMatcher} and {!InterpreterLoopsCore.Matcher}. +(** See {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} and [Matcher]. This module contains primitive match functions to instantiate the generic - {!InterpreterLoopsMatchCtxs.MakeMatcher} functor. + {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} functor. *) module type PrimMatcher = sig val match_etys : ety -> ety -> ety @@ -231,8 +231,8 @@ module type Matcher = sig eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue end -(** See {!InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and - {!InterpreterLoopsCore.CheckEquivMatcher}. +(** See {!module:InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and + {!module-type:InterpreterLoopsCore.CheckEquivMatcher}. Very annoying: functors only take modules as inputs... *) diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli index bf29af79..5f69b8d3 100644 --- a/compiler/InterpreterLoopsMatchCtxs.mli +++ b/compiler/InterpreterLoopsMatchCtxs.mli @@ -27,13 +27,13 @@ val compute_abs_borrows_loans_maps : We use it for joins, to check if two environments are convertible, etc. See for instance {!MakeJoinMatcher} and {!MakeCheckEquivMatcher}. - The functor is parameterized by a {!PrimMatcher}, which implements the - non-generic part of the match. More precisely, the role of {!PrimMatcher} is two + The functor is parameterized by a {!module-type:InterpreterLoopsCore.PrimMatcher}, which implements the + non-generic part of the match. More precisely, the role of {!module-type:InterpreterLoopsCore.PrimMatcher} is two provide generic functions which recursively match two values (by recursively matching the fields of ADT values for instance). When it does need to match values in a non-trivial manner (if two ADT values don't have the same variant for instance) it calls the corresponding specialized function from - {!PrimMatcher}. + {!module-type:InterpreterLoopsCore.PrimMatcher}. *) module MakeMatcher : functor (_ : PrimMatcher) -> Matcher diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli index 583c6907..9e4ebc20 100644 --- a/compiler/InterpreterProjectors.mli +++ b/compiler/InterpreterProjectors.mli @@ -6,7 +6,7 @@ open Contexts Apply a proj_borrows on a shared borrow. Note that when projecting over shared values, we generate - {!type:abstract_shared_borrows}, not {!type:avalue}s. + {!type:Aeneas.Values.abstract_shared_borrows}, not {!type:Aeneas.Values.avalue}s. Parameters: [regions] diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli index d84e8be6..3832d02f 100644 --- a/compiler/InterpreterStatements.mli +++ b/compiler/InterpreterStatements.mli @@ -10,7 +10,7 @@ open Cps 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 - {!constructor:env_elem.Frame} indicator delimiting the current frame and + {!constructor:Contexts.env_elem.EFrame} 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 diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index ecd8f53f..bba88e9f 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -111,7 +111,7 @@ let mk_typed_value_from_symbolic_value (svalue : symbolic_value) : typed_value = (** Create a loans projector value from a symbolic value. Checks if the projector will actually project some regions. If not, - returns {!AIgnored} ([_]). + returns {!Values.AIgnored} ([_]). TODO: update to handle 'static *) @@ -238,7 +238,7 @@ let symbolic_value_has_ended_regions (ended_regions : RegionId.Set.t) let regions = ty_regions s.sv_ty in not (RegionId.Set.disjoint regions ended_regions) -(** Check if a {!type:value} contains [⊥]. +(** Check if a {!type:Values.value} contains [⊥]. Note that this function is very general: it also checks wether symbolic values contain already ended regions. diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 50849df9..0ae83007 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -273,7 +273,7 @@ class virtual ['self] mapreduce_ty_base = type ty = | TAdt of type_id * generic_args - (** {!Adt} encodes ADTs and tuples and assumed types. + (** {!TAdt} encodes ADTs and tuples and assumed types. TODO: what about the ended regions? (ADTs may be parameterized with several region variables. When giving back an ADT value, we may @@ -1064,7 +1064,7 @@ type trait_impl = { meta : meta; impl_trait : trait_decl_ref; llbc_impl_trait : Types.trait_decl_ref; - (** Same remark as for {llbc_generics}. *) + (** Same remark as for {!field:llbc_generics}. *) generics : generic_params; llbc_generics : Types.generic_params; (** We use the LLBC generics to generate "pretty" names, for instance diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 6b0deb73..a5143f3c 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -195,7 +195,7 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig = We only look for outer monadic let-bindings. This is used when printing the branches of [if ... then ... else ...]. - Rem.: this function will *fail* if there are {!constructor:Aeneas.Pure.expression.Loop} + Rem.: this function will *fail* if there are {!Pure.Loop} nodes (you should call it on an expression where those nodes have been eliminated). *) let rec let_group_requires_parentheses (e : texpression) : bool = diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index 73e7f71d..a05b2c5a 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -76,7 +76,7 @@ let erase_regions_subst : subst = tr_self = Self; } -(** Convert an {!rty} to an {!ety} by erasing the region variables *) +(** Erase the region variables in a type *) let erase_regions (ty : ty) : ty = ty_substitute erase_regions_subst ty let trait_ref_erase_regions (tr : trait_ref) : trait_ref = diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index a9f45926..53f99b7f 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -66,8 +66,8 @@ type 'a region_group_id_map = 'a RegionGroupId.Map.t [@@deriving show] (** Ancestor for {!expression} iter visitor. - We could make it inherit the visitor for {!eval_ctx}, but in all the uses - of this visitor we don't need to explore {!eval_ctx}, so we make it inherit + We could make it inherit the visitor for {!Contexts.eval_ctx}, but in all the uses + of this visitor we don't need to explore {!Contexts.eval_ctx}, so we make it inherit the abstraction visitors instead. *) class ['self] iter_expression_base = diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml index 52e12b9a..76cc710a 100644 --- a/compiler/TypesUtils.ml +++ b/compiler/TypesUtils.ml @@ -5,7 +5,7 @@ include Charon.TypesUtils (** Retuns true if the type contains borrows. Note that we can't simply explore the type and look for regions: sometimes - we erase the lists of regions (by replacing them with [[]] when using {!Types.ety}, + we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty}, and when a type uses 'static this region doesn't appear in the region parameters. *) let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = @@ -15,7 +15,7 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = (** Retuns true if the type contains nested borrows. Note that we can't simply explore the type and look for regions: sometimes - we erase the lists of regions (by replacing them with [[]] when using {!Types.ety}, + we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty}, and when a type uses 'static this region doesn't appear in the region parameters. *) let ty_has_nested_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = |