diff options
| -rw-r--r-- | backends/lean/primitives.lean | 1 | ||||
| -rw-r--r-- | compiler/Extract.ml | 39 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 34 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 1 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 575 |
5 files changed, 358 insertions, 292 deletions
diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean index 9e72b708..09ece14e 100644 --- a/backends/lean/primitives.lean +++ b/backends/lean/primitives.lean @@ -100,6 +100,7 @@ def USize.checked_sub (n: USize) (m: USize): result USize := fail integerOverflow -- TODO: settle the style for usize_sub before we write these +def USize.checked_add (n: USize) (m: USize): result USize := sorry def USize.checked_mul (n: USize) (m: USize): result USize := sorry def USize.checked_div (n: USize) (m: USize): result USize := sorry diff --git a/compiler/Extract.ml b/compiler/Extract.ml index af510a84..44bc5e1c 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -175,8 +175,8 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = ] | Lean -> [ - (Result, result_return_id, "result.ret"); - (Result, result_fail_id, "result.fail"); + (Result, result_return_id, "ret"); + (Result, result_fail_id, "fail"); (Error, error_failure_id, "panic"); (* No Fuel::Zero on purpose *) (* No Fuel::Succ on purpose *) @@ -202,7 +202,7 @@ let assumed_llbc_functions : (VecIndexMut, rg0, "vec_index_mut_back"); ] -let assumed_pure_functions : (pure_assumed_fun_id * string) list = +let assumed_pure_functions (): (pure_assumed_fun_id * string) list = match !backend with | FStar -> [ @@ -218,7 +218,7 @@ let assumed_pure_functions : (pure_assumed_fun_id * string) list = | Lean -> [ (Return, "return"); - (Fail, "fail"); + (Fail, "fail_"); (Assert, "massert"); (* TODO: figure out how to deal with this *) (FuelDecrease, "decrease"); @@ -232,7 +232,7 @@ let names_map_init () : names_map_init = assumed_structs; assumed_variants = assumed_variants (); assumed_llbc_functions; - assumed_pure_functions; + assumed_pure_functions = assumed_pure_functions (); } let extract_unop (extract_expr : bool -> texpression -> unit) @@ -1414,7 +1414,11 @@ let extract_adt_g_value *) let cons = match variant_id with - | Some vid -> ctx_get_variant adt_id vid ctx + | Some vid -> + if !backend = Lean then + ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx + else + ctx_get_variant adt_id vid ctx | None -> ctx_get_struct adt_id ctx in if inside && field_values <> [] then F.pp_print_string fmt "("; @@ -1610,7 +1614,11 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) *) let cons = match adt_cons.variant_id with - | Some vid -> ctx_get_variant adt_cons.adt_id vid ctx + | Some vid -> + if !backend = Lean then + ctx_get_type adt_cons.adt_id ctx ^ "." ^ ctx_get_variant adt_cons.adt_id vid ctx + else + ctx_get_variant adt_cons.adt_id vid ctx | None -> ctx_get_struct adt_cons.adt_id ctx in let use_parentheses = inside && args <> [] in @@ -1725,7 +1733,8 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) F.pp_print_space fmt (); extract_texpression ctx fmt false re; F.pp_print_space fmt (); - F.pp_print_string fmt "in"; + if !backend <> Lean then + F.pp_print_string fmt "in"; ctx) in (* Close the box for the let-binding *) @@ -1734,6 +1743,13 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (* Return *) ctx in + (* If Lean, we rely on monadic blocks, so we insert a do and open a new box + immediately *) + if !backend = Lean then begin + F.pp_open_vbox fmt ctx.indent_incr; + F.pp_print_string fmt "do"; + F.pp_print_space fmt (); + end; let ctx = List.fold_left (fun ctx (monadic, lv, re) -> extract_let ctx monadic lv re) @@ -1745,6 +1761,9 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) extract_texpression ctx fmt false next_e; (* Close the box for the next expression *) F.pp_close_box fmt (); + (* do-box (Lean only) *) + if !backend = Lean then + F.pp_close_box fmt (); (* Close parentheses *) if inside then F.pp_print_string fmt ")"; (* Close the box for the whole expression *) @@ -1852,7 +1871,9 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (* End the match *) F.pp_print_space fmt (); - F.pp_print_string fmt "end"); + (* Relying on indentation in Lean *) + if !backend <> Lean then + F.pp_print_string fmt "end"); (* Close parentheses *) if inside then F.pp_print_string fmt ")"; (* Close the box for the whole expression *) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 3ad55d37..152dfc99 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -107,10 +107,10 @@ type type_decl_kind = Enum | Struct For instance, provided some information about a function (its basename, information about the region group, etc.) it should come up with an appropriate name for the forward/backward function. - + It can of course apply many transformations, like changing to camel case/ snake case, adding prefixes/suffixes, etc. - + 2. Format some specific terms, like constants. *) type formatter = { @@ -120,12 +120,12 @@ type formatter = { str_name : string; type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> string; (** Compute the qualified for a type definition/declaration. - + For instance: "type", "and", etc. *) fun_decl_kind_to_qualif : decl_kind -> string; (** Compute the qualified for a function definition/declaration. - + For instance: "let", "let rec", "and", etc. *) field_name : name -> FieldId.id -> string option -> string; @@ -133,7 +133,7 @@ type formatter = { - type name - field id - field name - + Note that fields don't always have names, but we still need to generate some names if we want to extract the structures to records... We might want to extract such structures to tuples, later, but field @@ -147,13 +147,13 @@ type formatter = { *) struct_constructor : name -> string; (** Structure constructors are used when constructing structure values. - + For instance, in F*: {[ type pair = { x : nat; y : nat } let p : pair = Mkpair 0 1 ]} - + Inputs: - type name *) @@ -194,7 +194,7 @@ type formatter = { (** Generates the name of the definition used to prove/reason about termination. The generated code uses this clause where needed, but its body must be defined by the user. - + Inputs: - function id: this is especially useful to identify whether the function is an assumed function or a local function @@ -205,7 +205,7 @@ type formatter = { *) var_basename : StringSet.t -> string option -> ty -> string; (** Generates a variable basename. - + Inputs: - the set of names used in the context so far - the basename we got from the symbolic execution, if we have one @@ -227,7 +227,7 @@ type formatter = { *) extract_primitive_value : F.formatter -> bool -> primitive_value -> unit; (** Format a constant value. - + Inputs: - formatter - [inside]: if [true], the value should be wrapped in parentheses @@ -242,7 +242,7 @@ type formatter = { texpression -> unit; (** Format a unary operation - + Inputs: - a formatter for expressions (called on the argument of the unop) - extraction context (see below) @@ -262,7 +262,7 @@ type formatter = { texpression -> unit; (** Format a binary operation - + Inputs: - a formatter for expressions (called on the arguments of the binop) - extraction context (see below) @@ -289,7 +289,7 @@ type id = | StructId of type_id (** We use this when we manipulate the names of the structure constructors. - + For instance, in F*: {[ type pair = { x: nat; y : nat } @@ -328,7 +328,7 @@ module IdMap = Collections.MakeMap (IdOrderedType) (** The names map stores the mappings from names to identifiers and vice-versa. We use it for lookups (during the translation) and to check for name clashes. - + [id_to_string] is for debugging. *) type names_map = { @@ -385,7 +385,7 @@ let names_map_add_function (id_to_string : id -> string) (fid : fun_id) We do this in an inefficient manner (by testing all indices starting from 0) but it shouldn't be a bottleneck. - + Also note that at some point, we thought about trying to reuse names of variables which are not used anymore, like here: {[ @@ -394,7 +394,7 @@ let names_map_add_function (id_to_string : id -> string) (fid : fun_id) let x0 = ... in // We could use the name "x" if [x] is not used below ... ]} - + However it is a good idea to keep things as they are for F*: as F* is designed for extrinsic proofs, a proof about a function follows this function's structure. The consequence is that we often end up @@ -402,7 +402,7 @@ let names_map_add_function (id_to_string : id -> string) (fid : fun_id) when calling lemmas) we often need to talk about the "past" (i.e., previous values), it is very useful to generate code where all variable names are assigned at most once. - + [append]: function to append an index to a string *) let basename_to_unique (names_set : StringSet.t) diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index 9e72b708..09ece14e 100644 --- a/tests/lean/hashmap_on_disk/Base/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -100,6 +100,7 @@ def USize.checked_sub (n: USize) (m: USize): result USize := fail integerOverflow -- TODO: settle the style for usize_sub before we write these +def USize.checked_add (n: USize) (m: USize): result USize := sorry def USize.checked_mul (n: USize) (m: USize): result USize := sorry def USize.checked_div (n: USize) (m: USize): result USize := sorry diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 3fb121d4..6ef0df22 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -14,9 +14,11 @@ def hashmap_hash_map_allocate_slots_loop_fwd := if n > (USize.ofNatCore 0 (by intlit)) then ( - let slots0 <- vec_push_back (hashmap_list_t T) slots HashmapListNil in - let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) in - hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0) + do + let slots0 <- + vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil + let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) + hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0) else result.ret slots /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ @@ -32,12 +34,13 @@ def hashmap_hash_map_new_with_capacity_fwd (max_load_divisor : USize) : result (hashmap_hash_map_t T) := - let v <- vec_new (hashmap_list_t T) in - let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity in - let i <- USize.checked_mul capacity max_load_dividend in - let i0 <- USize.checked_div i max_load_divisor in - result.ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by intlit)) - (max_load_dividend, max_load_divisor) i0 slots) + do + let v <- vec_new (hashmap_list_t T) + let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity + let i <- USize.checked_mul capacity max_load_dividend + let i0 <- USize.checked_div i max_load_divisor + result.ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by intlit)) + (max_load_dividend, max_load_divisor) i0 slots) /- [hashmap_main::hashmap::HashMap::{0}::new] -/ def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) := @@ -49,14 +52,17 @@ def hashmap_hash_map_clear_slots_loop_fwd_back (T : Type) (slots : vec (hashmap_list_t T)) (i : USize) : result (vec (hashmap_list_t T)) := - let i0 <- vec_len (hashmap_list_t T) slots in - if i < i0 - then ( - let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) in - let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i HashmapListNil - in - hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1) - else result.ret slots + do + let i0 <- vec_len (hashmap_list_t T) slots + if i < i0 + then ( + do + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) + let slots0 <- + vec_index_mut_back (hashmap_list_t T) slots i + hashmap_list_t.HashmapListNil + hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1) + else result.ret slots /- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ def hashmap_hash_map_clear_slots_fwd_back @@ -69,10 +75,11 @@ def hashmap_hash_map_clear_slots_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ def hashmap_hash_map_clear_fwd_back (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := - let v <- hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots - in - result.ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by intlit)) - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + do + let v <- + hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots + result.ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by intlit)) + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) /- [hashmap_main::hashmap::HashMap::{0}::len] -/ def hashmap_hash_map_len_fwd @@ -83,12 +90,12 @@ def hashmap_hash_map_len_fwd def hashmap_hash_map_insert_in_list_loop_fwd (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : result Bool := match ls with - | HashmapListCons ckey cvalue tl => + | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key then result.ret false else hashmap_hash_map_insert_in_list_loop_fwd T key value tl - | HashmapListNil => result.ret true - end + | hashmap_list_t.HashmapListNil => result.ret true + /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_fwd @@ -101,15 +108,18 @@ def hashmap_hash_map_insert_in_list_loop_back result (hashmap_list_t T) := match ls with - | HashmapListCons ckey cvalue tl => + | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key - then result.ret (HashmapListCons ckey value tl) + then result.ret (hashmap_list_t.HashmapListCons ckey value tl) else ( - let l <- hashmap_hash_map_insert_in_list_loop_back T key value tl in - result.ret (HashmapListCons ckey cvalue l)) - | HashmapListNil => - let l <- HashmapListNil in result.ret (HashmapListCons key value l) - end + do + let l <- hashmap_hash_map_insert_in_list_loop_back T key value tl + result.ret (hashmap_list_t.HashmapListCons ckey cvalue l)) + | hashmap_list_t.HashmapListNil => + do + let l <- hashmap_list_t.HashmapListNil + result.ret (hashmap_list_t.HashmapListCons key value l) + /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_back @@ -123,30 +133,34 @@ def hashmap_hash_map_insert_no_resize_fwd_back (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) : result (hashmap_hash_map_t T) := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - in - let inserted <- hashmap_hash_map_insert_in_list_fwd T key value l in - if inserted - then ( - let i0 <- USize.checked_add self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by intlit)) in - let l0 <- hashmap_hash_map_insert_in_list_back T key value l in - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 in - result.ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v)) - else ( - let l0 <- hashmap_hash_map_insert_in_list_back T key value l in - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 in - result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)) + do + let hash <- hashmap_hash_key_fwd key + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let inserted <- hashmap_hash_map_insert_in_list_fwd T key value l + if inserted + then ( + do + let i0 <- USize.checked_add self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by intlit)) + let l0 <- hashmap_hash_map_insert_in_list_back T key value l + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + result.ret (mkhashmap_hash_map_t i0 + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load + v)) + else ( + do + let l0 <- hashmap_hash_map_insert_in_list_back T key value l + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load + v)) /- [core::num::u32::{9}::MAX] -/ def core_num_u32_max_body : result UInt32 := @@ -159,11 +173,12 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back result (hashmap_hash_map_t T) := match ls with - | HashmapListCons k v tl => - let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v in - hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl - | HashmapListNil => result.ret ntable - end + | hashmap_list_t.HashmapListCons k v tl => + do + let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v + hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl + | hashmap_list_t.HashmapListNil => result.ret ntable + /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ def hashmap_hash_map_move_elements_from_list_fwd_back @@ -178,18 +193,22 @@ def hashmap_hash_map_move_elements_loop_fwd_back (i : USize) : result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) := - let i0 <- vec_len (hashmap_list_t T) slots in - if i < i0 - then ( - let l <- vec_index_mut_fwd (hashmap_list_t T) slots i in - let ls <- mem_replace_fwd (hashmap_list_t T) l HashmapListNil in - let ntable0 <- - hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls in - let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) in - let l0 <- mem_replace_back (hashmap_list_t T) l HashmapListNil in - let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i l0 in - hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1) - else result.ret (ntable, slots) + do + let i0 <- vec_len (hashmap_list_t T) slots + if i < i0 + then ( + do + let l <- vec_index_mut_fwd (hashmap_list_t T) slots i + let ls <- + mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.HashmapListNil + let ntable0 <- + hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) + let l0 <- + mem_replace_back (hashmap_list_t T) l hashmap_list_t.HashmapListNil + let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i l0 + hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1) + else result.ret (ntable, slots) /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ def hashmap_hash_map_move_elements_fwd_back @@ -202,45 +221,48 @@ def hashmap_hash_map_move_elements_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ def hashmap_hash_map_try_resize_fwd_back (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := - let max_usize <- scalar_cast U32 Usize core_num_u32_max_c in - let capacity <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by intlit)) in - let (i, i0) <- self.hashmap_hash_map_max_load_factor in - let i1 <- USize.checked_div n1 i in - if capacity <= i1 - then ( - let i2 <- USize.checked_mul capacity (USize.ofNatCore 2 (by intlit)) in - let ntable <- hashmap_hash_map_new_with_capacity_fwd T i2 i i0 in - let (ntable0, _) <- - hashmap_hash_map_move_elements_fwd_back T ntable - self.hashmap_hash_map_slots (USize.ofNatCore 0 (by intlit)) in - result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) - ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots)) - else - result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) - self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) + do + let max_usize <- scalar_cast U32 Usize core_num_u32_max_c + let capacity <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by intlit)) + let (i, i0) <- self.hashmap_hash_map_max_load_factor + let i1 <- USize.checked_div n1 i + if capacity <= i1 + then ( + do + let i2 <- USize.checked_mul capacity (USize.ofNatCore 2 (by intlit)) + let ntable <- hashmap_hash_map_new_with_capacity_fwd T i2 i i0 + let (ntable0, _) <- + hashmap_hash_map_move_elements_fwd_back T ntable + self.hashmap_hash_map_slots (USize.ofNatCore 0 (by intlit)) + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, + i0) ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots)) + else + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, + i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) /- [hashmap_main::hashmap::HashMap::{0}::insert] -/ def hashmap_hash_map_insert_fwd_back (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) : result (hashmap_hash_map_t T) := - let self0 <- hashmap_hash_map_insert_no_resize_fwd_back T self key value in - let i <- hashmap_hash_map_len_fwd T self0 in - if i > self0.hashmap_hash_map_max_load - then hashmap_hash_map_try_resize_fwd_back T self0 - else result.ret self0 + do + let self0 <- hashmap_hash_map_insert_no_resize_fwd_back T self key value + let i <- hashmap_hash_map_len_fwd T self0 + if i > self0.hashmap_hash_map_max_load + then hashmap_hash_map_try_resize_fwd_back T self0 + else result.ret self0 /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ def hashmap_hash_map_contains_key_in_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := match ls with - | HashmapListCons ckey t tl => + | hashmap_list_t.HashmapListCons ckey t tl => if ckey = key then result.ret true else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl - | HashmapListNil => result.ret false - end + | hashmap_list_t.HashmapListNil => result.ret false + /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ def hashmap_hash_map_contains_key_in_list_fwd @@ -250,23 +272,24 @@ def hashmap_hash_map_contains_key_in_list_fwd /- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ def hashmap_hash_map_contains_key_fwd (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result Bool := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in - hashmap_hash_map_contains_key_in_list_fwd T key l + do + let hash <- hashmap_hash_key_fwd key + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + hashmap_hash_map_contains_key_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ def hashmap_hash_map_get_in_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := match ls with - | HashmapListCons ckey cvalue tl => + | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key then result.ret cvalue else hashmap_hash_map_get_in_list_loop_fwd T key tl - | HashmapListNil => result.fail panic - end + | hashmap_list_t.HashmapListNil => result.fail error.panic + /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ def hashmap_hash_map_get_in_list_fwd @@ -276,23 +299,24 @@ def hashmap_hash_map_get_in_list_fwd /- [hashmap_main::hashmap::HashMap::{0}::get] -/ def hashmap_hash_map_get_fwd (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in - hashmap_hash_map_get_in_list_fwd T key l + do + let hash <- hashmap_hash_key_fwd key + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + hashmap_hash_map_get_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_loop_fwd (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := match ls with - | HashmapListCons ckey cvalue tl => + | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key then result.ret cvalue else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key - | HashmapListNil => result.fail panic - end + | hashmap_list_t.HashmapListNil => result.fail error.panic + /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_fwd @@ -301,72 +325,75 @@ def hashmap_hash_map_get_mut_in_list_fwd /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_loop_back - (T : Type) (ls : hashmap_list_t T) (key : USize) (ret : T) : + (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : result (hashmap_list_t T) := match ls with - | HashmapListCons ckey cvalue tl => + | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key - then result.ret (HashmapListCons ckey ret tl) + then result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl) else ( - let l <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret in - result.ret (HashmapListCons ckey cvalue l)) - | HashmapListNil => result.fail panic - end + do + let l <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 + result.ret (hashmap_list_t.HashmapListCons ckey cvalue l)) + | hashmap_list_t.HashmapListNil => result.fail error.panic + /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_back - (T : Type) (ls : hashmap_list_t T) (key : USize) (ret : T) : + (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : result (hashmap_list_t T) := - hashmap_hash_map_get_mut_in_list_loop_back T ls key ret + hashmap_hash_map_get_mut_in_list_loop_back T ls key ret0 /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ def hashmap_hash_map_get_mut_fwd (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - in - hashmap_hash_map_get_mut_in_list_fwd T l key + do + let hash <- hashmap_hash_key_fwd key + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + hashmap_hash_map_get_mut_in_list_fwd T l key /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ def hashmap_hash_map_get_mut_back - (T : Type) (self : hashmap_hash_map_t T) (key : USize) (ret : T) : + (T : Type) (self : hashmap_hash_map_t T) (key : USize) (ret0 : T) : result (hashmap_hash_map_t T) := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - in - let l0 <- hashmap_hash_map_get_mut_in_list_back T l key ret in - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - l0 in - result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + do + let hash <- hashmap_hash_key_fwd key + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let l0 <- hashmap_hash_map_get_mut_in_list_back T l key ret0 + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : result (option T) := match ls with - | HashmapListCons ckey t tl => + | hashmap_list_t.HashmapListCons ckey t tl => if ckey = key then - let mv_ls <- - mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl) - HashmapListNil in - match mv_ls with - | HashmapListCons i cvalue tl0 => result.ret (@some cvalue) - | HashmapListNil => result.fail panic - end + do + let mv_ls <- + mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons + ckey t tl) hashmap_list_t.HashmapListNil + match mv_ls with + | hashmap_list_t.HashmapListCons i cvalue tl0 => + result.ret (option.@some cvalue) + | hashmap_list_t.HashmapListNil => result.fail error.panic + else hashmap_hash_map_remove_from_list_loop_fwd T key tl - | HashmapListNil => result.ret @none - end + | hashmap_list_t.HashmapListNil => result.ret option.@none + /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_fwd @@ -379,21 +406,23 @@ def hashmap_hash_map_remove_from_list_loop_back result (hashmap_list_t T) := match ls with - | HashmapListCons ckey t tl => + | hashmap_list_t.HashmapListCons ckey t tl => if ckey = key then - let mv_ls <- - mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl) - HashmapListNil in - match mv_ls with - | HashmapListCons i cvalue tl0 => result.ret tl0 - | HashmapListNil => result.fail panic - end + do + let mv_ls <- + mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons + ckey t tl) hashmap_list_t.HashmapListNil + match mv_ls with + | hashmap_list_t.HashmapListCons i cvalue tl0 => result.ret tl0 + | hashmap_list_t.HashmapListNil => result.fail error.panic + else ( - let l <- hashmap_hash_map_remove_from_list_loop_back T key tl in - result.ret (HashmapListCons ckey t l)) - | HashmapListNil => result.ret HashmapListNil - end + do + let l <- hashmap_hash_map_remove_from_list_loop_back T key tl + result.ret (hashmap_list_t.HashmapListCons ckey t l)) + | hashmap_list_t.HashmapListNil => result.ret hashmap_list_t.HashmapListNil + /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_back @@ -405,126 +434,140 @@ def hashmap_hash_map_remove_from_list_back /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ def hashmap_hash_map_remove_fwd (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result (option T) := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - in - let x <- hashmap_hash_map_remove_from_list_fwd T key l in - match x with - | @none => result.ret @none - | @some x0 => - let _ <- USize.checked_sub self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by intlit)) in - result.ret (@some x0) - end + do + let hash <- hashmap_hash_key_fwd key + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let x <- hashmap_hash_map_remove_from_list_fwd T key l + match x with + | option.@none => result.ret option.@none + | option.@some x0 => + do + let _ <- USize.checked_sub self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by intlit)) + result.ret (option.@some x0) + /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ def hashmap_hash_map_remove_back (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result (hashmap_hash_map_t T) := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - in - let x <- hashmap_hash_map_remove_from_list_fwd T key l in - match x with - | @none => - let l0 <- hashmap_hash_map_remove_from_list_back T key l in - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 in - result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) - | @some x0 => - let i0 <- USize.checked_sub self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by intlit)) in - let l0 <- hashmap_hash_map_remove_from_list_back T key l in - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 in - result.ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end + do + let hash <- hashmap_hash_key_fwd key + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let x <- hashmap_hash_map_remove_from_list_fwd T key l + match x with + | option.@none => + do + let l0 <- hashmap_hash_map_remove_from_list_back T key l + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load + v) + | option.@some x0 => + do + let i0 <- USize.checked_sub self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by intlit)) + let l0 <- hashmap_hash_map_remove_from_list_back T key l + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + result.ret (mkhashmap_hash_map_t i0 + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load + v) + /- [hashmap_main::hashmap::test1] -/ def hashmap_test1_fwd : result Unit := - let hm <- hashmap_hash_map_new_fwd UInt64 in - let hm0 <- - hashmap_hash_map_insert_fwd_back UInt64 hm (USize.ofNatCore 0 (by intlit)) - (UInt64.ofNatCore 42 (by intlit)) in - let hm1 <- - hashmap_hash_map_insert_fwd_back UInt64 hm0 - (USize.ofNatCore 128 (by intlit)) (UInt64.ofNatCore 18 (by intlit)) in - let hm2 <- - hashmap_hash_map_insert_fwd_back UInt64 hm1 - (USize.ofNatCore 1024 (by intlit)) (UInt64.ofNatCore 138 (by intlit)) in - let hm3 <- - hashmap_hash_map_insert_fwd_back UInt64 hm2 - (USize.ofNatCore 1056 (by intlit)) (UInt64.ofNatCore 256 (by intlit)) in - let i <- - hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by intlit)) in - if not (i = (UInt64.ofNatCore 18 (by intlit))) - then result.fail panic - else ( - let hm4 <- - hashmap_hash_map_get_mut_back UInt64 hm3 - (USize.ofNatCore 1024 (by intlit)) (UInt64.ofNatCore 56 (by intlit)) in - let i0 <- - hashmap_hash_map_get_fwd UInt64 hm4 (USize.ofNatCore 1024 (by intlit)) in - if not (i0 = (UInt64.ofNatCore 56 (by intlit))) - then result.fail panic + do + let hm <- hashmap_hash_map_new_fwd UInt64 + let hm0 <- + hashmap_hash_map_insert_fwd_back UInt64 hm + (USize.ofNatCore 0 (by intlit)) (UInt64.ofNatCore 42 (by intlit)) + let hm1 <- + hashmap_hash_map_insert_fwd_back UInt64 hm0 + (USize.ofNatCore 128 (by intlit)) (UInt64.ofNatCore 18 (by intlit)) + let hm2 <- + hashmap_hash_map_insert_fwd_back UInt64 hm1 + (USize.ofNatCore 1024 (by intlit)) (UInt64.ofNatCore 138 (by intlit)) + let hm3 <- + hashmap_hash_map_insert_fwd_back UInt64 hm2 + (USize.ofNatCore 1056 (by intlit)) (UInt64.ofNatCore 256 (by intlit)) + let i <- + hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by intlit)) + if not (i = (UInt64.ofNatCore 18 (by intlit))) + then result.fail error.panic else ( - let x <- - hashmap_hash_map_remove_fwd UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) in - match x with - | @none => result.fail panic - | @some x0 => - if not (x0 = (UInt64.ofNatCore 56 (by intlit))) - then result.fail panic + do + let hm4 <- + hashmap_hash_map_get_mut_back UInt64 hm3 + (USize.ofNatCore 1024 (by intlit)) + (UInt64.ofNatCore 56 (by intlit)) + let i0 <- + hashmap_hash_map_get_fwd UInt64 hm4 + (USize.ofNatCore 1024 (by intlit)) + if not (i0 = (UInt64.ofNatCore 56 (by intlit))) + then result.fail error.panic else ( - let hm5 <- - hashmap_hash_map_remove_back UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) in - let i1 <- - hashmap_hash_map_get_fwd UInt64 hm5 (USize.ofNatCore 0 (by intlit)) - in - if not (i1 = (UInt64.ofNatCore 42 (by intlit))) - then result.fail panic - else ( - let i2 <- - hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 128 (by intlit)) in - if not (i2 = (UInt64.ofNatCore 18 (by intlit))) - then result.fail panic - else ( - let i3 <- - hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 1056 (by intlit)) in - if not (i3 = (UInt64.ofNatCore 256 (by intlit))) - then result.fail panic - else result.ret ()))) - end)) + do + let x <- + hashmap_hash_map_remove_fwd UInt64 hm4 + (USize.ofNatCore 1024 (by intlit)) + match x with + | option.@none => result.fail error.panic + | option.@some x0 => + if not (x0 = (UInt64.ofNatCore 56 (by intlit))) + then result.fail error.panic + else ( + do + let hm5 <- + hashmap_hash_map_remove_back UInt64 hm4 + (USize.ofNatCore 1024 (by intlit)) + let i1 <- + hashmap_hash_map_get_fwd UInt64 hm5 + (USize.ofNatCore 0 (by intlit)) + if not (i1 = (UInt64.ofNatCore 42 (by intlit))) + then result.fail error.panic + else ( + do + let i2 <- + hashmap_hash_map_get_fwd UInt64 hm5 + (USize.ofNatCore 128 (by intlit)) + if not (i2 = (UInt64.ofNatCore 18 (by intlit))) + then result.fail error.panic + else ( + do + let i3 <- + hashmap_hash_map_get_fwd UInt64 hm5 + (USize.ofNatCore 1056 (by intlit)) + if not (i3 = (UInt64.ofNatCore 256 (by intlit))) + then result.fail error.panic + else result.ret ()))) + )) /- Unit test for [hashmap_main::hashmap::test1] -/ -#assert (hashmap_test1_fwd = result.ret ()) +#assert (hashmap_test1_fwd = ret ()) /- [hashmap_main::insert_on_disk] -/ def insert_on_disk_fwd (key : USize) (value : UInt64) (st : state) : result (state × Unit) := - let (st0, hm) <- hashmap_utils_deserialize_fwd st in - let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value in - let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 in - result.ret (st1, ()) + do + let (st0, hm) <- hashmap_utils_deserialize_fwd st + let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value + let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 + result.ret (st1, ()) /- [hashmap_main::main] -/ def main_fwd : result Unit := result.ret () /- Unit test for [hashmap_main::main] -/ -#assert (main_fwd = result.ret ()) +#assert (main_fwd = ret ()) |