From b854ac27a4315d2357aad717e1e2f36065d7d8cb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 15:32:54 -0700 Subject: [PATCH] snap --- .../generated/FStarC_Compiler_HashMap.ml | 104 ++++++++++++++++++ .../generated/FStarC_ToSyntax_ToSyntax.ml | 48 ++++---- 2 files changed, 127 insertions(+), 25 deletions(-) create mode 100644 ocaml/fstar-lib/generated/FStarC_Compiler_HashMap.ml diff --git a/ocaml/fstar-lib/generated/FStarC_Compiler_HashMap.ml b/ocaml/fstar-lib/generated/FStarC_Compiler_HashMap.ml new file mode 100644 index 00000000000..8a3b122c9eb --- /dev/null +++ b/ocaml/fstar-lib/generated/FStarC_Compiler_HashMap.ml @@ -0,0 +1,104 @@ +open Prims +type ('k, 'v) hashmap = ('k * 'v) FStarC_Compiler_Util.pimap +type ('k, 'v) t = ('k, 'v) hashmap +let empty : 'k 'v . unit -> ('k, 'v) hashmap = + fun uu___ -> FStarC_Compiler_Util.pimap_empty () +let add : + 'k 'v . + 'k FStarC_Class_Deq.deq -> + 'k FStarC_Class_Hashable.hashable -> + 'k -> 'v -> ('k, 'v) hashmap -> ('k, 'v) hashmap + = + fun uu___ -> + fun uu___1 -> + fun key -> + fun value -> + fun m -> + let uu___2 = + let uu___3 = FStarC_Class_Hashable.hash uu___1 key in + FStarC_Hash.to_int uu___3 in + FStarC_Compiler_Util.pimap_add m uu___2 (key, value) +let remove : + 'k 'v . + 'k FStarC_Class_Deq.deq -> + 'k FStarC_Class_Hashable.hashable -> + 'k -> ('k, 'v) hashmap -> ('k, 'v) hashmap + = + fun uu___ -> + fun uu___1 -> + fun key -> + fun m -> + let uu___2 = + let uu___3 = FStarC_Class_Hashable.hash uu___1 key in + FStarC_Hash.to_int uu___3 in + FStarC_Compiler_Util.pimap_remove m uu___2 +let lookup : + 'k 'v . + 'k FStarC_Class_Deq.deq -> + 'k FStarC_Class_Hashable.hashable -> + 'k -> ('k, 'v) hashmap -> 'v FStar_Pervasives_Native.option + = + fun uu___ -> + fun uu___1 -> + fun key -> + fun m -> + let uu___2 = + let uu___3 = + let uu___4 = FStarC_Class_Hashable.hash uu___1 key in + FStarC_Hash.to_int uu___4 in + FStarC_Compiler_Util.pimap_try_find m uu___3 in + match uu___2 with + | FStar_Pervasives_Native.Some (key', v1) when + FStarC_Class_Deq.op_Equals_Question uu___ key key' -> + FStar_Pervasives_Native.Some v1 + | uu___3 -> FStar_Pervasives_Native.None +let get : + 'k 'v . + 'k FStarC_Class_Deq.deq -> + 'k FStarC_Class_Hashable.hashable -> 'k -> ('k, 'v) hashmap -> 'v + = + fun uu___ -> + fun uu___1 -> + fun key -> + fun m -> + let uu___2 = lookup uu___ uu___1 key m in + FStar_Pervasives_Native.__proj__Some__item__v uu___2 +let mem : + 'k 'v . + 'k FStarC_Class_Deq.deq -> + 'k FStarC_Class_Hashable.hashable -> + 'k -> ('k, 'v) hashmap -> Prims.bool + = + fun uu___ -> + fun uu___1 -> + fun key -> + fun m -> + let uu___2 = lookup uu___ uu___1 key m in + FStar_Pervasives_Native.uu___is_Some uu___2 +let cached_fun : + 'a 'b . + 'a FStarC_Class_Hashable.hashable -> + 'a FStarC_Class_Deq.deq -> ('a -> 'b) -> (('a -> 'b) * (unit -> unit)) + = + fun uu___ -> + fun uu___1 -> + fun f -> + let cache = + let uu___2 = empty () in FStarC_Compiler_Util.mk_ref uu___2 in + let f_cached x = + let uu___2 = + let uu___3 = FStarC_Compiler_Effect.op_Bang cache in + lookup uu___1 uu___ x uu___3 in + match uu___2 with + | FStar_Pervasives_Native.Some y -> y + | FStar_Pervasives_Native.None -> + let y = f x in + ((let uu___4 = + let uu___5 = FStarC_Compiler_Effect.op_Bang cache in + add uu___1 uu___ x y uu___5 in + FStarC_Compiler_Effect.op_Colon_Equals cache uu___4); + y) in + (f_cached, + (fun uu___2 -> + let uu___3 = empty () in + FStarC_Compiler_Effect.op_Colon_Equals cache uu___3)) \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml index 0488b062bb7..712b6a29d93 100644 --- a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml @@ -9182,11 +9182,10 @@ and (desugar_decl_maybe_fail_attr : FStar_Pervasives_Native.snd uu___ in let uu___ = let attrs = - let uu___1 = - FStarC_Compiler_List.map (desugar_term env) - d.FStarC_Parser_AST.attrs in - FStarC_Syntax_Util.deduplicate_terms uu___1 in - let uu___1 = get_fail_attr false attrs in + FStarC_Compiler_List.map (desugar_term env) + d.FStarC_Parser_AST.attrs in + let attrs1 = FStarC_Syntax_Util.deduplicate_terms attrs in + let uu___1 = get_fail_attr false attrs1 in match uu___1 with | FStar_Pervasives_Native.Some (expected_errs, lax) -> let d1 = @@ -9202,7 +9201,7 @@ and (desugar_decl_maybe_fail_attr : FStarC_Errors.catch_errors (fun uu___3 -> FStarC_Options.with_saved_options - (fun uu___4 -> desugar_decl_core env attrs d1)) in + (fun uu___4 -> desugar_decl_core env attrs1 d1)) in (match uu___2 with | (errs, r) -> (match (errs, r) with @@ -9210,7 +9209,7 @@ and (desugar_decl_maybe_fail_attr : let ses1 = FStarC_Compiler_List.map (fun se -> - let uu___3 = no_fail_attrs attrs in + let uu___3 = no_fail_attrs attrs1 in { FStarC_Syntax_Syntax.sigel = (se.FStarC_Syntax_Syntax.sigel); @@ -9242,7 +9241,7 @@ and (desugar_decl_maybe_fail_attr : FStarC_Syntax_Syntax.sigquals = []; FStarC_Syntax_Syntax.sigmeta = FStarC_Syntax_Syntax.default_sigmeta; - FStarC_Syntax_Syntax.sigattrs = attrs; + FStarC_Syntax_Syntax.sigattrs = attrs1; FStarC_Syntax_Syntax.sigopens_and_abbrevs = uu___3; FStarC_Syntax_Syntax.sigopts = FStar_Pervasives_Native.None @@ -9335,7 +9334,7 @@ and (desugar_decl_maybe_fail_attr : FStarC_Errors_Msg.is_error_message_list_doc) (Obj.magic uu___8)); (env0, [])))))) - | FStar_Pervasives_Native.None -> desugar_decl_core env attrs d in + | FStar_Pervasives_Native.None -> desugar_decl_core env attrs1 d in match uu___ with | (env1, sigelts) -> (env1, sigelts) and (desugar_decl : env_t -> FStarC_Parser_AST.decl -> (env_t * FStarC_Syntax_Syntax.sigelts)) @@ -9821,13 +9820,16 @@ and (desugar_decl_core : (fv.FStarC_Syntax_Syntax.fv_name).FStarC_Syntax_Syntax.v in (match uu___6 with | (qs', ats') -> - ((FStarC_Compiler_List.op_At qs' - qs), - (FStarC_Compiler_List.op_At ats' - ats)))) fvs ([], []) in + ((FStarC_Compiler_List.rev_append + qs' qs), + (FStarC_Compiler_List.rev_append + ats' ats)))) fvs ([], []) in (match uu___4 with | (val_quals, val_attrs) -> - let top_attrs = d_attrs in + let top_attrs = + FStarC_Syntax_Util.deduplicate_terms + (FStarC_Compiler_List.rev_append val_attrs + d_attrs) in let lbs1 = let uu___5 = lbs in match uu___5 with @@ -9837,10 +9839,9 @@ and (desugar_decl_core : (fun lb -> let uu___6 = FStarC_Syntax_Util.deduplicate_terms - (FStarC_Compiler_List.op_At + (FStarC_Compiler_List.rev_append lb.FStarC_Syntax_Syntax.lbattrs - (FStarC_Compiler_List.op_At - val_attrs top_attrs)) in + top_attrs) in { FStarC_Syntax_Syntax.lbname = (lb.FStarC_Syntax_Syntax.lbname); @@ -9883,10 +9884,6 @@ and (desugar_decl_core : fvs in let s = let uu___5 = - FStarC_Syntax_Util.deduplicate_terms - (FStarC_Compiler_List.op_At val_attrs - top_attrs) in - let uu___6 = FStarC_Syntax_DsEnv.opens_and_abbrevs env in { FStarC_Syntax_Syntax.sigel = @@ -9900,9 +9897,9 @@ and (desugar_decl_core : FStarC_Syntax_Syntax.sigquals = quals2; FStarC_Syntax_Syntax.sigmeta = FStarC_Syntax_Syntax.default_sigmeta; - FStarC_Syntax_Syntax.sigattrs = uu___5; + FStarC_Syntax_Syntax.sigattrs = top_attrs; FStarC_Syntax_Syntax.sigopens_and_abbrevs = - uu___6; + uu___5; FStarC_Syntax_Syntax.sigopts = FStar_Pervasives_Native.None } in @@ -10572,9 +10569,10 @@ let (desugar_decls : let uu___2 = desugar_decl env1 d in (match uu___2 with | (env2, se) -> - (env2, (FStarC_Compiler_List.op_At sigelts se)))) + (env2, (FStarC_Compiler_List.rev_append se sigelts)))) (env, []) decls in - match uu___ with | (env1, sigelts) -> (env1, sigelts) + match uu___ with + | (env1, sigelts) -> (env1, (FStarC_Compiler_List.rev sigelts)) let (desugar_modul_common : FStarC_Syntax_Syntax.modul FStar_Pervasives_Native.option -> FStarC_Syntax_DsEnv.env ->