diff options
| -rw-r--r-- | backends/lean/primitives.lean | 33 | ||||
| -rw-r--r-- | compiler/Extract.ml | 151 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 46 | ||||
| -rw-r--r-- | compiler/Translate.ml | 5 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 33 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 894 |
6 files changed, 697 insertions, 465 deletions
diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean index dc2314fc..6a41d1f4 100644 --- a/backends/lean/primitives.lean +++ b/backends/lean/primitives.lean @@ -6,6 +6,8 @@ import Lean -- Results & monadic combinators +-- TODO: use syntactic conventions and capitalize error, result, etc. + inductive error where | assertionFailure: error | integerOverflow: error @@ -23,17 +25,24 @@ deriving Repr, BEq open result +/- HELPERS -/ + -- TODO: is there automated syntax for these discriminators? def is_ret {α: Type} (r: result α): Bool := match r with | result.ret _ => true | result.fail _ => false -def eval_global {α: Type} (x: result α) (h: is_ret x): α := +def massert (b:Bool) : result Unit := + if b then .ret () else fail assertionFailure + +def eval_global {α: Type} (x: result α) (_: is_ret x): α := match x with | result.fail _ => by contradiction | result.ret x => x +/- DO-DSL SUPPORT -/ + def bind (x: result α) (f: α -> result β) : result β := match x with | ret v => f v @@ -47,8 +56,26 @@ instance : Bind result where instance : Pure result where pure := fun x => ret x -def massert (b:Bool) : result Unit := - if b then return () else fail assertionFailure +/- CUSTOM-DSL SUPPORT -/ + +-- Let-binding the result of a monadic operation is oftentimes not sufficient, +-- because we may need a hypothesis for equational reasoning in the scope. We +-- rely on subtype, and a custom let-binding operator, in effect recreating our +-- own variant of the do-dsl + +def result.attach : (o : result α) → result { x : α // o = ret x } + | .ret x => .ret ⟨x, rfl⟩ + | .fail e => .fail e + +macro "let" h:ident " : " e:term " <-- " f:term : doElem => + `(doElem| let ⟨$e, $h⟩ ← result.attach $f) + +-- Silly example of the kind of reasoning that this notation enables +#eval do + let h: y <-- .ret (0: Nat) + let _: y = 0 := by cases h; simp + let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩ + .ret r ---------------------- -- MACHINE INTEGERS -- diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 7670c753..f45b9b58 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -489,6 +489,16 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) fname ^ lp_suffix ^ suffix in + let terminates_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) + (num_loops : int) (loop_id : LoopId.id option) : string = + let fname = fun_name_to_snake_case fname in + let lp_suffix = default_fun_loop_suffix num_loops loop_id in + (* Compute the suffix *) + let suffix = "_terminates" in + (* Concatenate *) + fname ^ lp_suffix ^ suffix + in + let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty) : string = (* If there is a basename, we use it *) @@ -619,6 +629,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) global_name; fun_name; decreases_clause_name; + terminates_clause_name; var_basename; type_var_basename; append_index; @@ -1348,7 +1359,11 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) let (fwd, loop_fwds), back_ls = def in (* Register the decrease clauses, if necessary *) let register_decreases ctx def = - if has_decreases_clause def then ctx_add_decreases_clause def ctx else ctx + if has_decreases_clause def then + let ctx = ctx_add_decreases_clause def ctx in + ctx_add_terminates_clause def ctx + else + ctx in let ctx = List.fold_left register_decreases ctx (fwd :: loop_fwds) in (* Register the function names *) @@ -1626,31 +1641,40 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) in let is_lean_struct = !backend = Lean && adt_cons.variant_id = None in if is_lean_struct then - (* TODO: enclosing curly brace is indented too far to the right *) (* TODO: when only one or two fields differ, considering using the with syntax (peephole optimization) *) let decl_id = match adt_cons.adt_id with | AdtId id -> id | _ -> assert false in let def_kind = (TypeDeclId.Map.find decl_id ctx.trans_ctx.type_context.type_decls).kind in let fields = match def_kind with | T.Struct fields -> fields | _ -> assert false in let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in - F.pp_open_vbox fmt ctx.indent_incr; + F.pp_open_hvbox fmt 0; + F.pp_open_hvbox fmt ctx.indent_incr; F.pp_print_string fmt "{"; F.pp_print_space fmt (); + F.pp_open_hvbox fmt ctx.indent_incr; + F.pp_open_hvbox fmt 0; Collections.List.iter_link (fun () -> F.pp_print_string fmt ","; + F.pp_close_box fmt (); F.pp_print_space fmt () ) (fun ((fid, _), e) -> + F.pp_open_hovbox fmt 0; let f = ctx_get_field adt_cons.adt_id fid ctx in F.pp_print_string fmt f; F.pp_print_string fmt " := "; - extract_texpression ctx fmt true e + F.pp_open_hvbox fmt ctx.indent_incr; + extract_texpression ctx fmt true e; + F.pp_close_box fmt () ) (List.combine fields args); - F.pp_print_space fmt (); F.pp_close_box fmt (); - F.pp_print_string fmt "}"; + F.pp_close_box fmt (); + F.pp_close_box fmt (); + F.pp_close_box fmt (); + F.pp_print_space fmt (); + F.pp_print_string fmt "}" else let use_parentheses = inside && args <> [] in if use_parentheses then F.pp_print_string fmt "("; @@ -2015,7 +2039,7 @@ let assert_backend_supports_decreases_clauses () = *) let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : unit = - assert_backend_supports_decreases_clauses (); + assert (!backend = FStar); (* Retrieve the function name *) let def_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in @@ -2028,16 +2052,14 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) * one line *) F.pp_open_hvbox fmt 0; (* Add the [unfold] keyword *) - if !backend = FStar then begin - F.pp_print_string fmt "unfold"; - F.pp_print_space fmt (); - end; + F.pp_print_string fmt "unfold"; + F.pp_print_space fmt (); (* Open a box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *) F.pp_open_hvbox fmt ctx.indent_incr; (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *) F.pp_open_hovbox fmt ctx.indent_incr; (* > "let FUN_NAME" *) - F.pp_print_string fmt ((if !backend = FStar then "let " else "def ") ^ def_name); + F.pp_print_string fmt ("let " ^ def_name); F.pp_print_space fmt (); (* Extract the parameters *) let space = ref true in @@ -2046,20 +2068,119 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt ":"; (* Print the signature *) F.pp_print_space fmt (); - F.pp_print_string fmt (if !backend = FStar then "nat" else "Nat"); + F.pp_print_string fmt "nat"; (* Print the "=" *) F.pp_print_space fmt (); - F.pp_print_string fmt (if !backend = FStar then "=" else ":="); + F.pp_print_string fmt "="; (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *) F.pp_close_box fmt (); F.pp_print_space fmt (); (* Print the "admit ()" *) - F.pp_print_string fmt (if !backend = FStar then "admit ()" else "sorry"); + F.pp_print_string fmt "admit ()"; + (* Close the box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *) + F.pp_close_box fmt (); + (* Close the box for the whole definition *) + F.pp_close_box fmt (); + (* Add breaks to insert new lines between definitions *) + F.pp_print_break fmt 0 0 + +(** Extract templates for the termination_by and decreases_by clauses of a + recursive function definition. + + For Lean only. + + We extract two commands. The first one is a regular definition for the + termination measure (the value derived from the function arguments that + decreases over function calls). The second one is a macro definition that + defines a proof script (allowed to refer to function arguments) that proves + termination. +*) +let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter) (def: fun_decl): unit = + assert (!backend = Lean); + + (* Retrieve the function name *) + let def_name = ctx_get_terminates_clause def.def_id def.loop_id ctx in + let def_body = Option.get def.body in + (* Add a break before *) + F.pp_print_break fmt 0 0; + (* Print a comment to link the extracted type to its original rust definition *) + extract_comment fmt ("[" ^ Print.fun_name_to_string def.basename ^ "]: termination measure"); + F.pp_print_space fmt (); + (* Open a box for the definition, so that whenever possible it gets printed on + * one line *) + F.pp_open_hvbox fmt 0; + (* Add the [unfold] keyword *) + F.pp_print_string fmt "@[simp]"; + F.pp_print_space fmt (); + (* Open a box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *) + F.pp_open_hvbox fmt ctx.indent_incr; + (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *) + F.pp_open_hovbox fmt ctx.indent_incr; + (* > "let FUN_NAME" *) + F.pp_print_string fmt ("def " ^ def_name); + F.pp_print_space fmt (); + (* Extract the parameters *) + let space = ref true in + let _, ctx_body = extract_fun_parameters space ctx fmt def in + (* Print the ":=" *) + F.pp_print_space fmt (); + F.pp_print_string fmt ":="; + (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *) + F.pp_close_box fmt (); + F.pp_print_space fmt (); + (* Tuple of the arguments *) + let vars = List.map (fun (v: var) -> v.id) def_body.inputs in + if List.length vars = 1 then + F.pp_print_string fmt (ctx_get_var (List.hd vars) ctx_body) + else begin + F.pp_open_hovbox fmt 0; + F.pp_print_string fmt "("; + Collections.List.iter_link + (fun () -> + F.pp_print_string fmt ","; + F.pp_print_space fmt ()) + (fun v -> F.pp_print_string fmt (ctx_get_var v ctx_body)) + vars; + F.pp_print_string fmt ")"; + F.pp_close_box fmt (); + end; (* Close the box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *) F.pp_close_box fmt (); (* Close the box for the whole definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) + F.pp_print_break fmt 0 0; + + (* Now extract a template for the termination proof *) + let def_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in + (* syntax <def_name> term ... term : tactic *) + F.pp_print_break fmt 0 0; + F.pp_open_hvbox fmt 0; + F.pp_print_string fmt "syntax \""; + F.pp_print_string fmt def_name; + F.pp_print_string fmt "\" term+ : tactic"; + F.pp_print_break fmt 0 0; + F.pp_print_break fmt 0 0; + (* macro_rules | `(tactic| fact_termination_proof $x) => `(tactic| ( *) + F.pp_print_string fmt "macro_rules"; + F.pp_print_space fmt (); + F.pp_open_hovbox fmt ctx.indent_incr; + F.pp_open_hovbox fmt 0; + F.pp_print_string fmt "| `(tactic| "; + F.pp_print_string fmt def_name; + F.pp_print_space fmt (); + Collections.List.iter_link (F.pp_print_space fmt) + (fun v -> + F.pp_print_string fmt "$"; + F.pp_print_string fmt (ctx_get_var v ctx_body)) + vars; + F.pp_print_string fmt ") =>"; + F.pp_close_box fmt (); + F.pp_open_hovbox fmt ctx.indent_incr; + F.pp_print_string fmt "`(tactic| sorry)"; + F.pp_close_box fmt (); + F.pp_close_box fmt (); + F.pp_close_box fmt (); F.pp_print_break fmt 0 0 (** Extract a function declaration. diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 152dfc99..77170b5b 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -203,6 +203,21 @@ type formatter = { the same purpose as in {!field:fun_name}. - loop identifier, if this is for a loop *) + terminates_clause_name : + A.FunDeclId.id -> fun_name -> int -> LoopId.id option -> string; + (** Generates the name of the measure used to prove/reason about + termination. The generated code uses this clause where needed, + but its body must be defined by the user. Lean only. + + Inputs: + - function id: this is especially useful to identify whether the + function is an assumed function or a local function + - function basename + - the number of loops in the parent function. This is used for + the same purpose as in {!field:fun_name}. + - loop identifier, if this is for a loop + *) + var_basename : StringSet.t -> string option -> ty -> string; (** Generates a variable basename. @@ -285,6 +300,12 @@ type id = the body of those clauses must be defined by the user, in the proper files. *) + | TerminatesClauseId of (A.fun_id * LoopId.id option) + (** The definition which provides the decreases/termination measure. + We insert calls to this clause to prove/reason about termination: + the body of those clauses must be defined by the user, in the + proper files. + *) | TypeId of type_id | StructId of type_id (** We use this when we manipulate the names of the structure @@ -486,6 +507,19 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | Some lid -> ", loop: " ^ LoopId.to_string lid in "decreases clause for function: " ^ fun_name ^ loop + | TerminatesClauseId (fid, lid) -> + let fun_name = + match fid with + | Regular fid -> + Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name + | Assumed aid -> A.show_assumed_fun_id aid + in + let loop = + match lid with + | None -> "" + | Some lid -> ", loop: " ^ LoopId.to_string lid + in + "terminates clause for function: " ^ fun_name ^ loop | TypeId id -> "type name: " ^ get_type_name id | StructId id -> "struct constructor of: " ^ get_type_name id | VariantId (id, variant_id) -> @@ -596,6 +630,10 @@ let ctx_get_decreases_clause (def_id : A.FunDeclId.id) (loop_id : LoopId.id option) (ctx : extraction_ctx) : string = ctx_get (DecreasesClauseId (Regular def_id, loop_id)) ctx +let ctx_get_terminates_clause (def_id : A.FunDeclId.id) + (loop_id : LoopId.id option) (ctx : extraction_ctx) : string = + ctx_get (TerminatesClauseId (Regular def_id, loop_id)) ctx + (** Generate a unique type variable name and add it to the context *) let ctx_add_type_var (basename : string) (id : TypeVarId.id) (ctx : extraction_ctx) : extraction_ctx * string = @@ -688,6 +726,14 @@ let ctx_add_decreases_clause (def : fun_decl) (ctx : extraction_ctx) : in ctx_add (DecreasesClauseId (Regular def.def_id, def.loop_id)) name ctx +let ctx_add_terminates_clause (def : fun_decl) (ctx : extraction_ctx) : + extraction_ctx = + let name = + ctx.fmt.terminates_clause_name def.def_id def.basename def.num_loops + def.loop_id + in + ctx_add (TerminatesClauseId (Regular def.def_id, def.loop_id)) name ctx + let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : extraction_ctx = let name = ctx.fmt.global_name def.name in diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 4ca9eff2..0a1c8f9a 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -563,7 +563,10 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let extract_decrease decl = let has_decr_clause = has_decreases_clause decl in if has_decr_clause then - Extract.extract_template_decreases_clause ctx.extract_ctx fmt decl + if !Config.backend = Lean then + Extract.extract_termination_and_decreasing ctx.extract_ctx fmt decl + else + Extract.extract_template_decreases_clause ctx.extract_ctx fmt decl in extract_decrease fwd; List.iter extract_decrease loop_fwds) diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index dc2314fc..6a41d1f4 100644 --- a/tests/lean/hashmap_on_disk/Base/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -6,6 +6,8 @@ import Lean -- Results & monadic combinators +-- TODO: use syntactic conventions and capitalize error, result, etc. + inductive error where | assertionFailure: error | integerOverflow: error @@ -23,17 +25,24 @@ deriving Repr, BEq open result +/- HELPERS -/ + -- TODO: is there automated syntax for these discriminators? def is_ret {α: Type} (r: result α): Bool := match r with | result.ret _ => true | result.fail _ => false -def eval_global {α: Type} (x: result α) (h: is_ret x): α := +def massert (b:Bool) : result Unit := + if b then .ret () else fail assertionFailure + +def eval_global {α: Type} (x: result α) (_: is_ret x): α := match x with | result.fail _ => by contradiction | result.ret x => x +/- DO-DSL SUPPORT -/ + def bind (x: result α) (f: α -> result β) : result β := match x with | ret v => f v @@ -47,8 +56,26 @@ instance : Bind result where instance : Pure result where pure := fun x => ret x -def massert (b:Bool) : result Unit := - if b then return () else fail assertionFailure +/- CUSTOM-DSL SUPPORT -/ + +-- Let-binding the result of a monadic operation is oftentimes not sufficient, +-- because we may need a hypothesis for equational reasoning in the scope. We +-- rely on subtype, and a custom let-binding operator, in effect recreating our +-- own variant of the do-dsl + +def result.attach : (o : result α) → result { x : α // o = ret x } + | .ret x => .ret ⟨x, rfl⟩ + | .fail e => .fail e + +macro "let" h:ident " : " e:term " <-- " f:term : doElem => + `(doElem| let ⟨$e, $h⟩ ← result.attach $f) + +-- Silly example of the kind of reasoning that this notation enables +#eval do + let h: y <-- .ret (0: Nat) + let _: y = 0 := by cases h; simp + let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩ + .ret r ---------------------- -- MACHINE INTEGERS -- diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 0dcb6450..29ed735f 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -11,22 +11,17 @@ def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap_hash_map_allocate_slots_loop_fwd (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) : - result (vec (hashmap_list_t T)) + Tot (result (vec (hashmap_list_t T))) + (decreases (hashmap_hash_map_allocate_slots_loop_decreases T slots n)) := if n > (USize.ofNatCore 0 (by intlit)) then - match h: (vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil).val with - | result.fail e => result.fail e - | result.ret slots0 => 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 - termination_by hashmap_hash_map_allocate_slots_loop_fwd T slots n => n - decreasing_by - simp_wf - sorry - /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap_hash_map_allocate_slots_fwd @@ -50,10 +45,10 @@ def hashmap_hash_map_new_with_capacity_fwd { hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), hashmap_hash_map_max_load_factor := (max_load_dividend, - max_load_divisor), + max_load_divisor), hashmap_hash_map_max_load := i0, hashmap_hash_map_slots := slots - } + } /- [hashmap_main::hashmap::HashMap::{0}::new] -/ def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) := @@ -97,7 +92,7 @@ def hashmap_hash_map_clear_fwd_back hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, hashmap_hash_map_slots := v - } + } /- [hashmap_main::hashmap::HashMap::{0}::len] -/ def hashmap_hash_map_len_fwd @@ -176,356 +171,256 @@ def hashmap_hash_map_insert_no_resize_fwd_back hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, hashmap_hash_map_slots := 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 + { + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, + hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, + hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, + hashmap_hash_map_slots := v } - else + + /- [core::num::u32::{9}::MAX] -/ + def core_num_u32_max_body : result UInt32 := + result.ret (UInt32.ofNatCore 4294967295 (by intlit)) + def core_num_u32_max_c : UInt32 := + eval_global core_num_u32_max_body (by simp) + + /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ + def hashmap_hash_map_move_elements_from_list_loop_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : + Tot (result (hashmap_hash_map_t T)) + (decreases ( + hashmap_hash_map_move_elements_from_list_loop_decreases T ntable ls)) + := + match ls with + | hashmap_list_t.HashmapListCons k v tl => 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 - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v - } - -/- [core::num::u32::{9}::MAX] -/ -def core_num_u32_max_body : result UInt32 := - result.ret (UInt32.ofNatCore 4294967295 (by intlit)) -def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) - -/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ -def hashmap_hash_map_move_elements_from_list_loop_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : - Tot (result (hashmap_hash_map_t T)) - (decreases ( - hashmap_hash_map_move_elements_from_list_loop_decreases T ntable ls)) - := - match ls with - | 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 + 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 - (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : - result (hashmap_hash_map_t T) - := - hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable ls - -/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ -def hashmap_hash_map_move_elements_loop_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) - (i : USize) : - Tot (result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))) - (decreases (hashmap_hash_map_move_elements_loop_decreases T ntable slots i)) - := - 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 - (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) - (i : USize) : - result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) - := - hashmap_hash_map_move_elements_loop_fwd_back T ntable slots i - -/- [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) := - 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 + /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ + def hashmap_hash_map_move_elements_from_list_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : + result (hashmap_hash_map_t T) + := + hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable ls + + /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ + def hashmap_hash_map_move_elements_loop_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) + (i : USize) : + Tot (result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))) + (decreases ( + hashmap_hash_map_move_elements_loop_decreases T ntable slots i)) + := + let i0 := vec_len (hashmap_list_t T) slots + if i < i0 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 - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := (i, - i0), - hashmap_hash_map_max_load := ntable0.hashmap_hash_map_max_load, - hashmap_hash_map_slots := ntable0.hashmap_hash_map_slots - } - else - result.ret - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := (i, - i0), - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := 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) - := - 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) : - Tot (result Bool) - (decreases (hashmap_hash_map_contains_key_in_list_loop_decreases T key ls)) - := - match ls with - | 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 - | hashmap_list_t.HashmapListNil => result.ret false + 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}::contains_key_in_list] -/ -def hashmap_hash_map_contains_key_in_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := - hashmap_hash_map_contains_key_in_list_loop_fwd T key ls - -/- [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 := - 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) : - Tot (result T) - (decreases (hashmap_hash_map_get_in_list_loop_decreases T key ls)) - := - match ls with - | 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 - | hashmap_list_t.HashmapListNil => result.fail error.panic - - -/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ -def hashmap_hash_map_get_in_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := - hashmap_hash_map_get_in_list_loop_fwd T key ls - -/- [hashmap_main::hashmap::HashMap::{0}::get] -/ -def hashmap_hash_map_get_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := - 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) : - Tot (result T) - (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases T ls key)) - := - match ls with - | 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 - | hashmap_list_t.HashmapListNil => result.fail error.panic + /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ + def hashmap_hash_map_move_elements_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) + (i : USize) : + result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) + := + hashmap_hash_map_move_elements_loop_fwd_back T ntable slots i - -/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -def hashmap_hash_map_get_mut_in_list_fwd - (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := - hashmap_hash_map_get_mut_in_list_loop_fwd T ls key - -/- [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) (ret0 : T) : - Tot (result (hashmap_list_t T)) - (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases T ls key)) - := - match ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => - if ckey = key - then result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl) - else + /- [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) := + 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 + { + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, + hashmap_hash_map_max_load_factor := (i, i0), + hashmap_hash_map_max_load := ntable0.hashmap_hash_map_max_load, + hashmap_hash_map_slots := ntable0.hashmap_hash_map_slots + } + else + result.ret + { + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, + hashmap_hash_map_max_load_factor := (i, i0), + hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, + hashmap_hash_map_slots := 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) + := 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) (ret0 : T) : - result (hashmap_list_t T) - := - 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 := - 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) (ret0 : T) : - result (hashmap_hash_map_t T) - := - 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 - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := 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) : - Tot (result (Option T)) - (decreases (hashmap_hash_map_remove_from_list_loop_decreases T key ls)) - := - match ls with - | hashmap_list_t.HashmapListCons ckey t tl => - if ckey = key - then - 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 + 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) : + Tot (result Bool) + (decreases ( + hashmap_hash_map_contains_key_in_list_loop_decreases T key ls)) + := + match ls with + | 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 + | hashmap_list_t.HashmapListNil => result.ret false - else hashmap_hash_map_remove_from_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => result.ret Option.none - - -/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -def hashmap_hash_map_remove_from_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result (Option T) := - hashmap_hash_map_remove_from_list_loop_fwd T key ls - -/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -def hashmap_hash_map_remove_from_list_loop_back - (T : Type) (key : USize) (ls : hashmap_list_t T) : - Tot (result (hashmap_list_t T)) - (decreases (hashmap_hash_map_remove_from_list_loop_decreases T key ls)) - := - match ls with - | hashmap_list_t.HashmapListCons ckey t tl => - if ckey = key - then - 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_main::hashmap::HashMap::{0}::contains_key_in_list] -/ + def hashmap_hash_map_contains_key_in_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := + hashmap_hash_map_contains_key_in_list_loop_fwd T key ls + + /- [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 := + 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) : + Tot (result T) + (decreases (hashmap_hash_map_get_in_list_loop_decreases T key ls)) + := + match ls with + | 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 | hashmap_list_t.HashmapListNil => result.fail error.panic - else + + /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ + def hashmap_hash_map_get_in_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := + hashmap_hash_map_get_in_list_loop_fwd T key ls + + /- [hashmap_main::hashmap::HashMap::{0}::get] -/ + def hashmap_hash_map_get_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := 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 - (T : Type) (key : USize) (ls : hashmap_list_t T) : - result (hashmap_list_t T) - := - hashmap_hash_map_remove_from_list_loop_back T key ls - -/- [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) := - 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 => + 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) : + Tot (result T) + (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases T ls key)) + := + match ls with + | 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 + | 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 + (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := + hashmap_hash_map_get_mut_in_list_loop_fwd T ls key + + /- [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) (ret0 : T) : + Tot (result (hashmap_list_t T)) + (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases T ls key)) + := + match ls with + | hashmap_list_t.HashmapListCons ckey cvalue tl => + if ckey = key + then result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl) + else + 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) (ret0 : T) : + result (hashmap_list_t T) + := + 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 := do - let _ <- USize.checked_sub self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by intlit)) - result.ret (Option.some x0) + 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}::remove] -/ -def hashmap_hash_map_remove_back - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : - result (hashmap_hash_map_t T) - := - 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 => + /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ + def hashmap_hash_map_get_mut_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) (ret0 : T) : + result (hashmap_hash_map_t T) + := do - let l0 <- hashmap_hash_map_remove_from_list_back T key l + 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 @@ -535,107 +430,220 @@ def hashmap_hash_map_remove_back hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, hashmap_hash_map_slots := v - } - | Option.some x0 => + } + + /- [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) : + Tot (result (Option T)) + (decreases (hashmap_hash_map_remove_from_list_loop_decreases T key ls)) + := + match ls with + | hashmap_list_t.HashmapListCons ckey t tl => + if ckey = key + then + 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 + | hashmap_list_t.HashmapListNil => result.ret Option.none + + + /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ + def hashmap_hash_map_remove_from_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result (Option T) := + hashmap_hash_map_remove_from_list_loop_fwd T key ls + + /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ + def hashmap_hash_map_remove_from_list_loop_back + (T : Type) (key : USize) (ls : hashmap_list_t T) : + Tot (result (hashmap_list_t T)) + (decreases (hashmap_hash_map_remove_from_list_loop_decreases T key ls)) + := + match ls with + | hashmap_list_t.HashmapListCons ckey t tl => + if ckey = key + then + 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 + 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 + (T : Type) (key : USize) (ls : hashmap_list_t T) : + result (hashmap_list_t T) + := + hashmap_hash_map_remove_from_list_loop_back T key ls + + /- [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) + := 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 - { - hashmap_hash_map_num_entries := i0, - hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v - } + 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::test1] -/ -def hashmap_test1_fwd : result Unit := - 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 + /- [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) + := 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 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 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))) + 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 + { + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, + hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, + hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, + hashmap_hash_map_slots := 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 + { + hashmap_hash_map_num_entries := i0, + hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, + hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, + hashmap_hash_map_slots := v + } + + /- [hashmap_main::hashmap::test1] -/ + def hashmap_test1_fwd : result Unit := + 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 + 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 do - let hm5 <- - hashmap_hash_map_remove_back UInt64 hm4 + let x <- + hashmap_hash_map_remove_fwd 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 = ret ()) - -/- [hashmap_main::insert_on_disk] -/ -def insert_on_disk_fwd - (key : USize) (value : UInt64) (st : state) : result (state × Unit) := - 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 = ret ()) - + 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 = ret ()) + + /- [hashmap_main::insert_on_disk] -/ + def insert_on_disk_fwd + (key : USize) (value : UInt64) (st : state) : result (state × Unit) := + 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 = ret ()) + |