summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backends/lean/primitives.lean33
-rw-r--r--compiler/Extract.ml151
-rw-r--r--compiler/ExtractBase.ml46
-rw-r--r--compiler/Translate.ml5
-rw-r--r--tests/lean/hashmap_on_disk/Base/Primitives.lean33
-rw-r--r--tests/lean/hashmap_on_disk/HashmapMain/Funs.lean894
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 ())
+