Merge pull request #3571 from mtzguido/perf

Small perf improvements, also fixing order dependency of qualifiers
FStarLang · Oct 16, 2024 · 74f189b · 74f189b
2 parents 164b9e2 + 1fd7fea
commit 74f189b
Show file tree

Hide file tree

Showing 29 changed files with 695 additions and 126 deletions.
diff --git a/ocaml/fstar-lib/FStarC_Compiler_Util.ml b/ocaml/fstar-lib/FStarC_Compiler_Util.ml
@@ -468,6 +468,7 @@ let pimap_find_default (map: 'value pimap) (key: Z.t) (dflt: 'value) =
 let pimap_try_find (map: 'value pimap) (key: Z.t) =
   ZMap.Exceptionless.find key map
 let pimap_fold (m:'value pimap) f a = ZMap.fold f m a
+let pimap_remove (m:'value pimap) k = ZMap.remove k m
 
 (* restore pre-2.11 BatString.nsplit behavior,
    see https://github.com/ocaml-batteries-team/batteries-included/issues/845 *)

diff --git a/ocaml/fstar-lib/FStarC_Hash.ml b/ocaml/fstar-lib/FStarC_Hash.ml
@@ -5,6 +5,8 @@ type hash_code = int
 
 let cmp_hash (x:hash_code) (y:hash_code) : Z.t = Z.of_int (x-y)
 
+let to_int (i:int) = Z.of_int i
+
 let of_int (i:Z.t) = Z.to_int i
 let of_string (s:string) = BatHashtbl.hash s
 

diff --git a/ocaml/fstar-lib/generated/FStarC_Class_Ord.ml b/ocaml/fstar-lib/generated/FStarC_Class_Ord.ml
diff --git a/ocaml/fstar-lib/generated/FStarC_Ident.ml b/ocaml/fstar-lib/generated/FStarC_Ident.ml
diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_Syntax.ml
diff --git a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml