From 9ddd174959970f87658191034b70d0cfa02ff451 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 15:49:54 +0200
Subject: Filter some type arguments for the builtin types/functions

---
 compiler/ExtractBase.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'compiler/ExtractBase.ml')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index f26beeb6..e004aba8 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -640,6 +640,19 @@ type extraction_ctx = {
   functions_with_decreases_clause : PureUtils.FunLoopIdSet.t;
   trans_trait_decls : Pure.trait_decl Pure.TraitDeclId.Map.t;
   trans_trait_impls : Pure.trait_impl Pure.TraitImplId.Map.t;
+  types_filter_type_args_map : bool list TypeDeclId.Map.t;
+      (** The map to filter the type arguments for the builtin type
+          definitions.
+
+          We need this for type `Vec`, for instance, which takes a useless
+          (in the context of the type translation) type argument for the
+          allocator which is used, and which we want to remove.
+
+          TODO: it would be cleaner to filter those types in a micro-pass,
+          rather than at code generation time.
+        *)
+  funs_filter_type_args_map : bool list FunDeclId.Map.t;
+      (** Same as {!types_filter_type_args_map}, but for functions *)
 }
 
 (** Debugging function, used when communicating name collisions to the user,
-- 
cgit v1.2.3