Prefer Map.of_list to a manual fold

AeneasVerif · Dec 3, 2024 · 8b78a41 · 8b78a41
1 parent 5a8abdf
commit 8b78a41
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 22 deletions.
diff --git a/src/interp/InterpreterUtils.ml b/src/interp/InterpreterUtils.ml
@@ -495,17 +495,9 @@ let instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
   let tr_self = Substitute.trait_instance_id_erase_regions tr_self in
   (* Generate fresh abstraction ids and create a substitution from region
    * group ids to abstraction ids *)
-  let rg_abs_ids_bindings =
-    List.map
-      (fun rg ->
-        let abs_id = fresh_abstraction_id () in
-        (rg.id, abs_id))
-      regions_hierarchy
-  in
   let asubst_map : AbstractionId.id RegionGroupId.Map.t =
-    List.fold_left
-      (fun mp (rg_id, abs_id) -> RegionGroupId.Map.add rg_id abs_id mp)
-      RegionGroupId.Map.empty rg_abs_ids_bindings
+    RegionGroupId.Map.of_list
+      (List.map (fun rg -> (rg.id, fresh_abstraction_id ())) regions_hierarchy)
   in
   let asubst (rg_id : RegionGroupId.id) : AbstractionId.id =
     RegionGroupId.Map.find rg_id asubst_map

diff --git a/src/pure/PureUtils.ml b/src/pure/PureUtils.ml
@@ -168,12 +168,8 @@ let ty_substitute (subst : subst) (ty : ty) : ty =
 
 let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
     =
-  let ls = List.combine vars tys in
-  let mp =
-    List.fold_left
-      (fun mp (k, v) -> TypeVarId.Map.add (k : type_var).index v mp)
-      TypeVarId.Map.empty ls
-  in
+  let var_ids = List.map (fun k -> (k : type_var).index) vars in
+  let mp = TypeVarId.Map.of_list (List.combine var_ids tys) in
   fun id -> TypeVarId.Map.find id mp
 
 let make_const_generic_subst (vars : const_generic_var list)
@@ -184,12 +180,7 @@ let make_trait_subst (clauses : trait_clause list) (refs : trait_ref list) :
     TraitClauseId.id -> trait_instance_id =
   let clauses = List.map (fun x -> x.clause_id) clauses in
   let refs = List.map (fun (x : trait_ref) -> x.trait_id) refs in
-  let ls = List.combine clauses refs in
-  let mp =
-    List.fold_left
-      (fun mp (k, v) -> TraitClauseId.Map.add k v mp)
-      TraitClauseId.Map.empty ls
-  in
+  let mp = TraitClauseId.Map.of_list (List.combine clauses refs) in
   fun id -> TraitClauseId.Map.find id mp
 
 (** Retrieve the list of fields for the given variant of a {!type:Aeneas.Pure.type_decl}.