diff options
| -rw-r--r-- | backends/lean/Primitives.lean | 76 | ||||
| -rw-r--r-- | compiler/Extract.ml | 9 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 76 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 378 |
4 files changed, 268 insertions, 271 deletions
diff --git a/backends/lean/Primitives.lean b/backends/lean/Primitives.lean index 3ccb8466..e558e476 100644 --- a/backends/lean/Primitives.lean +++ b/backends/lean/Primitives.lean @@ -63,24 +63,28 @@ instance : Pure Result where -- 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 } +def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := + match o with | .ret x => .ret ⟨x, rfl⟩ - | .fail e => .fail e + | .fail e => .fail e -macro "let" h:ident " : " e:term " <-- " f:term : doElem => - `(doElem| let ⟨$e, $h⟩ ← Result.attach $f) +macro "let" e:term " ⟵ " f:term : doElem => + `(doElem| let ⟨$e, h⟩ ← Result.attach $f) --- Silly example of the kind of reasoning that this notation enables +-- TODO: any way to factorize both definitions? +macro "let" e:term " <-- " f:term : doElem => + `(doElem| let ⟨$e, h⟩ ← Result.attach $f) + +-- We call the hypothesis `h`, in effect making it unavailable to the user +-- (because too much shadowing). But in practice, once can use the French single +-- quote notation (input with f< and f>), where `‹ h ›` finds a suitable +-- hypothesis in the context, this is equivalent to `have x: h := by assumption in x` #eval do - let h: y <-- .ret (0: Nat) - let _: y = 0 := by cases h; decide + let y <-- .ret (0: Nat) + let _: y = 0 := by cases ‹ ret 0 = ret y › ; decide let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩ .ret r --- TODO: ideally, `let <--` would automatically pick the name for the fresh --- hypothesis, of the form `h_x` where `x` is the name of the variable, with --- collision-avoidance. That way, code generation would be simpler. - ---------------------- -- MACHINE INTEGERS -- ---------------------- @@ -151,13 +155,14 @@ def USize.checked_sub (n: USize) (m: USize): Result USize := else fail integerOverflow +@[simp] +theorem usize_fits (n: Nat) (h: n <= 4294967295): n < USize.size := + match USize.size, usize_size_eq with + | _, Or.inl rfl => Nat.lt_of_le_of_lt h (by decide) + | _, Or.inr rfl => Nat.lt_of_le_of_lt h (by decide) + def USize.checked_add (n: USize) (m: USize): Result USize := - if h: n.val.val + m.val.val <= 4294967295 then - .ret ⟨ n.val.val + m.val.val, by - have h': 4294967295 < USize.size := by intlit - apply Nat.lt_of_le_of_lt h h' - ⟩ - else if h: n.val + m.val < USize.size then + if h: n.val + m.val < USize.size then .ret ⟨ n.val + m.val, h ⟩ else .fail integerOverflow @@ -173,12 +178,7 @@ def USize.checked_rem (n: USize) (m: USize): Result USize := .fail integerOverflow def USize.checked_mul (n: USize) (m: USize): Result USize := - if h: n.val.val * m.val.val <= 4294967295 then - .ret ⟨ n.val.val * m.val.val, by - have h': 4294967295 < USize.size := by intlit - apply Nat.lt_of_le_of_lt h h' - ⟩ - else if h: n.val * m.val < USize.size then + if h: n.val * m.val < USize.size then .ret ⟨ n.val * m.val, h ⟩ else .fail integerOverflow @@ -193,7 +193,6 @@ def USize.checked_div (n: USize) (m: USize): Result USize := else .fail integerOverflow - -- Test behavior... #eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0 @@ -358,6 +357,10 @@ def mem_replace_fwd (a : Type) (x : a) (_ : a) : a := def mem_replace_back (a : Type) (_ : a) (y : a) : a := y +/-- Aeneas-translated function -- useful to reduce non-recursive definitions. + Use with `simp [ aeneas ]` -/ +register_simp_attr aeneas + -------------------- -- ASSERT COMMAND -- -------------------- @@ -366,21 +369,24 @@ open Lean Elab Command Term Meta syntax (name := assert) "#assert" term: command --- TODO: figure out how to make #assert behave as #eval followed by a compiler --- error if the term doesn't reduce to True. Once we have that, add some inline --- tests for the arithmetic operations, notably `rem` - @[command_elab assert] +unsafe def assertImpl : CommandElab := fun (_stx: Syntax) => do - logInfo "Reducing and asserting: " - logInfo _stx[1] runTermElabM (fun _ => do - let e ← Term.elabTerm _stx[1] none - logInfo (Expr.dbgToString e) - -- TODO: How to evaluate the term and compare the Result to true? + let r ← evalTerm Bool (mkConst ``Bool) _stx[1] + if not r then + logInfo "Assertion failed for: " + logInfo _stx[1] + logError "Expression reduced to false" pure ()) - -- logInfo (Expr.dbgToString (``true)) - -- throwError "TODO: assert" #eval 2 == 2 #assert (2 == 2) + +------------------- +-- SANITY CHECKS -- +------------------- + +-- TODO: add more once we have signed integers + +#assert (USize.checked_rem 1 2 == .ret 1) diff --git a/compiler/Extract.ml b/compiler/Extract.ml index a2ad37f5..c90d2170 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1809,7 +1809,8 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) match !backend with | FStar -> "=" | Coq -> ":=" - | Lean -> if monadic then "<-" else ":=" + (* TODO: switch to ⟵ once issues are fixed *) + | Lean -> if monadic then "←" else ":=" in F.pp_print_string fmt eq; F.pp_print_space fmt (); @@ -1867,6 +1868,8 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (* Open a box for the [if e] *) F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt "if"; + if !backend = Lean then + F.pp_print_string fmt " h:"; F.pp_print_space fmt (); let scrut_inside = PureUtils.texpression_requires_parentheses scrut in extract_texpression ctx fmt scrut_inside scrut; @@ -1924,7 +1927,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) F.pp_open_hovbox fmt ctx.indent_incr; (* Print the [match ... with] *) let match_begin = - match !backend with FStar -> "begin match" | Coq | Lean -> "match" + match !backend with FStar -> "begin match" | Coq -> "match" | Lean -> "match h:" in F.pp_print_string fmt match_begin; F.pp_print_space fmt (); @@ -2647,7 +2650,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); F.pp_print_string fmt "()"); F.pp_print_space fmt (); - F.pp_print_string fmt "="; + F.pp_print_string fmt "=="; F.pp_print_space fmt (); let success = ctx_get_variant (Assumed Result) result_return_id ctx in F.pp_print_string fmt ("." ^ success ^ " ())")); diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index b201d81a..e230dcab 100644 --- a/tests/lean/hashmap_on_disk/Base/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -63,24 +63,28 @@ instance : Pure Result where -- 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 } +def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := + match o with | .ret x => .ret ⟨x, rfl⟩ - | .fail e => .fail e + | .fail e => .fail e -macro "let" h:ident " : " e:term " <-- " f:term : doElem => - `(doElem| let ⟨$e, $h⟩ ← Result.attach $f) +macro "let" e:term " ⟵ " f:term : doElem => + `(doElem| let ⟨$e, h⟩ ← Result.attach $f) --- Silly example of the kind of reasoning that this notation enables +-- TODO: any way to factorize both definitions? +macro "let" e:term " <-- " f:term : doElem => + `(doElem| let ⟨$e, h⟩ ← Result.attach $f) + +-- We call the hypothesis `h`, in effect making it unavailable to the user +-- (because too much shadowing). But in practice, once can use the French single +-- quote notation (input with f< and f>), where `‹ h ›` finds a suitable +-- hypothesis in the context, this is equivalent to `have x: h := by assumption in x` #eval do - let h: y <-- .ret (0: Nat) - let _: y = 0 := by cases h; decide + let y <-- .ret (0: Nat) + let _: y = 0 := by cases ‹ ret 0 = ret y › ; decide let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩ .ret r --- TODO: ideally, `let <--` would automatically pick the name for the fresh --- hypothesis, of the form `h_x` where `x` is the name of the variable, with --- collision-avoidance. That way, code generation would be simpler. - ---------------------- -- MACHINE INTEGERS -- ---------------------- @@ -151,13 +155,14 @@ def USize.checked_sub (n: USize) (m: USize): Result USize := else fail integerOverflow +@[simp] +theorem usize_fits (n: Nat) (h: n <= 4294967295): n < USize.size := + match USize.size, usize_size_eq with + | _, Or.inl rfl => Nat.lt_of_le_of_lt h (by decide) + | _, Or.inr rfl => Nat.lt_of_le_of_lt h (by decide) + def USize.checked_add (n: USize) (m: USize): Result USize := - if h: n.val.val + m.val.val <= 4294967295 then - .ret ⟨ n.val.val + m.val.val, by - have h': 4294967295 < USize.size := by intlit - apply Nat.lt_of_le_of_lt h h' - ⟩ - else if h: n.val + m.val < USize.size then + if h: n.val + m.val < USize.size then .ret ⟨ n.val + m.val, h ⟩ else .fail integerOverflow @@ -173,12 +178,7 @@ def USize.checked_rem (n: USize) (m: USize): Result USize := .fail integerOverflow def USize.checked_mul (n: USize) (m: USize): Result USize := - if h: n.val.val * m.val.val <= 4294967295 then - .ret ⟨ n.val.val * m.val.val, by - have h': 4294967295 < USize.size := by intlit - apply Nat.lt_of_le_of_lt h h' - ⟩ - else if h: n.val * m.val < USize.size then + if h: n.val * m.val < USize.size then .ret ⟨ n.val * m.val, h ⟩ else .fail integerOverflow @@ -193,7 +193,6 @@ def USize.checked_div (n: USize) (m: USize): Result USize := else .fail integerOverflow - -- Test behavior... #eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0 @@ -358,6 +357,10 @@ def mem_replace_fwd (a : Type) (x : a) (_ : a) : a := def mem_replace_back (a : Type) (_ : a) (y : a) : a := y +/-- Aeneas-translated function -- useful to reduce non-recursive definitions. + Use with `simp [ aeneas ]` -/ +register_simp_attr aeneas + -------------------- -- ASSERT COMMAND -- -------------------- @@ -366,21 +369,24 @@ open Lean Elab Command Term Meta syntax (name := assert) "#assert" term: command --- TODO: figure out how to make #assert behave as #eval followed by a compiler --- error if the term doesn't reduce to True. Once we have that, add some inline --- tests for the arithmetic operations, notably `rem` - @[command_elab assert] +unsafe def assertImpl : CommandElab := fun (_stx: Syntax) => do - logInfo "Reducing and asserting: " - logInfo _stx[1] runTermElabM (fun _ => do - let e ← Term.elabTerm _stx[1] none - logInfo (Expr.dbgToString e) - -- TODO: How to evaluate the term and compare the Result to true? + let r ← evalTerm Bool (mkConst ``Bool) _stx[1] + if not r then + logInfo "Assertion failed for: " + logInfo _stx[1] + logError "Expression reduced to false" pure ()) - -- logInfo (Expr.dbgToString (``true)) - -- throwError "TODO: assert" #eval 2 == 2 #assert (2 == 2) + +------------------- +-- SANITY CHECKS -- +------------------- + +-- TODO: add more once we have signed integers + +#assert (USize.checked_rem 1 2 == .ret 1) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index ee50f126..392c8816 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -3,29 +3,29 @@ import Base.Primitives import HashmapMain.Types import HashmapMain.Opaque -import HashmapMain.Clauses.Template +import HashmapMain.Clauses.Clauses section variable (opaque_defs: OpaqueDefs) /- [hashmap_main::hashmap::hash_key] -/ -def hashmap_hash_key_fwd (k : USize) : Result USize := Result.ret k +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))) := - if n > (USize.ofNatCore 0 (by intlit)) + if h: n > (USize.ofNatCore 0 (by intlit)) then 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)) + 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 slots n => - hashmap_hash_map_allocate_slots_loop_terminates - T slots n + hashmap_hash_map_allocate_slots_loop_terminates T slots n decreasing_by hashmap_hash_map_allocate_slots_loop_decreases slots n /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ @@ -42,10 +42,10 @@ def hashmap_hash_map_new_with_capacity_fwd Result (hashmap_hash_map_t T) := do - let v := vec_new (hashmap_list_t T) - let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity - let i <- USize.checked_mul capacity max_load_dividend - let i0 <- USize.checked_div i max_load_divisor + let v := vec_new (hashmap_list_t T) + let slots ← hashmap_hash_map_allocate_slots_fwd T v capacity + let i ← USize.checked_mul capacity max_load_dividend + let i0 ← USize.checked_div i max_load_divisor Result.ret { hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), @@ -65,19 +65,18 @@ def hashmap_hash_map_clear_slots_loop_fwd_back (T : Type) (slots : Vec (hashmap_list_t T)) (i : USize) : (Result (Vec (hashmap_list_t T))) := - let i0 := vec_len (hashmap_list_t T) slots - if i < i0 + let i0 := vec_len (hashmap_list_t T) slots + if h: i < i0 then do - let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) - let slots0 <- + let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit)) + let slots0 ← vec_index_mut_back (hashmap_list_t T) slots i - hashmap_list_t.HashmapListNil + hashmap_list_t.HashmapListNil hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1 else Result.ret slots termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i => - hashmap_hash_map_clear_slots_loop_terminates - T slots i + hashmap_hash_map_clear_slots_loop_terminates T slots i decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i /- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ @@ -92,8 +91,8 @@ def hashmap_hash_map_clear_slots_fwd_back def hashmap_hash_map_clear_fwd_back (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := do - let v <- - hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots + let v ← + hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots Result.ret { hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), @@ -112,15 +111,14 @@ def hashmap_hash_map_insert_in_list_loop_fwd (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : (Result Bool) := - match ls with + match h: ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => - if ckey = key + if h: ckey = key then Result.ret false else hashmap_hash_map_insert_in_list_loop_fwd T key value tl | hashmap_list_t.HashmapListNil => Result.ret true - termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls => - hashmap_hash_map_insert_in_list_loop_terminates T key value ls + hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -133,20 +131,19 @@ def hashmap_hash_map_insert_in_list_loop_back (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : (Result (hashmap_list_t T)) := - match ls with + match h: ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => - if ckey = key + if h: ckey = key then Result.ret (hashmap_list_t.HashmapListCons ckey value tl) else do - let tl0 <- hashmap_hash_map_insert_in_list_loop_back T key value tl + let tl0 ← hashmap_hash_map_insert_in_list_loop_back T key value tl Result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) | hashmap_list_t.HashmapListNil => - let l := hashmap_list_t.HashmapListNil + let l := hashmap_list_t.HashmapListNil Result.ret (hashmap_list_t.HashmapListCons key value l) - termination_by hashmap_hash_map_insert_in_list_loop_back key value ls => - hashmap_hash_map_insert_in_list_loop_terminates T key value ls + hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -162,21 +159,21 @@ def hashmap_hash_map_insert_no_resize_fwd_back 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 inserted <- hashmap_hash_map_insert_in_list_fwd T key value l - if inserted + let hash ← hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod ← USize.checked_rem hash i + let l ← + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let inserted ← hashmap_hash_map_insert_in_list_fwd T key value l + if h: inserted then do - let i0 <- USize.checked_add self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by intlit)) - let l0 <- hashmap_hash_map_insert_in_list_back T key value l - let v <- + let i0 ← USize.checked_add self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by intlit)) + let l0 ← hashmap_hash_map_insert_in_list_back T key value l + let v ← vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 + hash_mod l0 Result.ret { hashmap_hash_map_num_entries := i0, @@ -186,10 +183,10 @@ def hashmap_hash_map_insert_no_resize_fwd_back } else do - let l0 <- hashmap_hash_map_insert_in_list_back T key value l - let v <- + 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 + hash_mod l0 Result.ret { hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, @@ -208,16 +205,15 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : (Result (hashmap_hash_map_t T)) := - match ls with + match h: ls with | hashmap_list_t.HashmapListCons k v tl => do - let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v + 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 - termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls - => hashmap_hash_map_move_elements_from_list_loop_terminates T - ntable ls + => + hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls decreasing_by hashmap_hash_map_move_elements_from_list_loop_decreases ntable ls /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ @@ -233,23 +229,23 @@ def hashmap_hash_map_move_elements_loop_fwd_back (i : USize) : (Result ((hashmap_hash_map_t T) × (Vec (hashmap_list_t T)))) := - let i0 := vec_len (hashmap_list_t T) slots - if i < i0 + let i0 := vec_len (hashmap_list_t T) slots + if h: i < i0 then do - let l <- vec_index_mut_fwd (hashmap_list_t T) slots i + 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)) + 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 + 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) termination_by hashmap_hash_map_move_elements_loop_fwd_back ntable slots i => - hashmap_hash_map_move_elements_loop_terminates T ntable slots i + hashmap_hash_map_move_elements_loop_terminates T ntable slots i decreasing_by hashmap_hash_map_move_elements_loop_decreases ntable slots i /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ @@ -264,19 +260,19 @@ def hashmap_hash_map_move_elements_fwd_back 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 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 + let max_usize ← scalar_cast 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 h: 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, _) <- + 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)) + self.hashmap_hash_map_slots (USize.ofNatCore 0 (by intlit)) Result.ret { hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, @@ -299,24 +295,23 @@ def hashmap_hash_map_insert_fwd_back 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 + let self0 ← hashmap_hash_map_insert_no_resize_fwd_back T self key value + let i ← hashmap_hash_map_len_fwd T self0 + if h: i > self0.hashmap_hash_map_max_load then hashmap_hash_map_try_resize_fwd_back T self0 else Result.ret self0 /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ def hashmap_hash_map_contains_key_in_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result Bool) := - match ls with + match h: ls with | hashmap_list_t.HashmapListCons ckey t tl => - if ckey = key + if h: 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 - termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls => - hashmap_hash_map_contains_key_in_list_loop_terminates T key ls + hashmap_hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ @@ -328,26 +323,24 @@ def hashmap_hash_map_contains_key_in_list_fwd 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 + let hash ← hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod ← USize.checked_rem hash i + let l ← + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod hashmap_hash_map_contains_key_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ def hashmap_hash_map_get_in_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result T) := - match ls with + match h: ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => - if ckey = key + if h: 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 - termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => - hashmap_hash_map_get_in_list_loop_terminates - T key ls + hashmap_hash_map_get_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ @@ -359,26 +352,24 @@ def hashmap_hash_map_get_in_list_fwd 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 + let hash ← hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod ← USize.checked_rem hash i + let l ← + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod hashmap_hash_map_get_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_loop_fwd (T : Type) (ls : hashmap_list_t T) (key : USize) : (Result T) := - match ls with + match h: ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => - if ckey = key + if h: 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 - termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key => - hashmap_hash_map_get_mut_in_list_loop_terminates - T ls key + hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -391,18 +382,17 @@ def hashmap_hash_map_get_mut_in_list_loop_back (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : (Result (hashmap_list_t T)) := - match ls with + match h: ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => - if ckey = key + if h: ckey = key then Result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl) else do - let tl0 <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 + let tl0 ← hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 Result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) | hashmap_list_t.HashmapListNil => Result.fail Error.panic - termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 => - hashmap_hash_map_get_mut_in_list_loop_terminates T ls key + hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -416,11 +406,11 @@ def hashmap_hash_map_get_mut_in_list_back 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 + 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] -/ @@ -429,15 +419,15 @@ def hashmap_hash_map_get_mut_back 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 <- + 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 + hash_mod l0 Result.ret { hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, @@ -449,24 +439,21 @@ def hashmap_hash_map_get_mut_back /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result (Option T)) := - match ls with + match h: ls with | hashmap_list_t.HashmapListCons ckey t tl => - if ckey = key + if h: 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 + t tl) hashmap_list_t.HashmapListNil + match h: 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 - termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls => - hashmap_hash_map_remove_from_list_loop_terminates - T key ls + hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ @@ -479,26 +466,23 @@ def hashmap_hash_map_remove_from_list_loop_back (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result (hashmap_list_t T)) := - match ls with + match h: ls with | hashmap_list_t.HashmapListCons ckey t tl => - if ckey = key + if h: 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 + t tl) hashmap_list_t.HashmapListNil + match h: mv_ls with | hashmap_list_t.HashmapListCons i cvalue tl0 => Result.ret tl0 | hashmap_list_t.HashmapListNil => Result.fail Error.panic - else do - let tl0 <- hashmap_hash_map_remove_from_list_loop_back T key tl + let tl0 ← hashmap_hash_map_remove_from_list_loop_back T key tl Result.ret (hashmap_list_t.HashmapListCons ckey t tl0) | hashmap_list_t.HashmapListNil => Result.ret hashmap_list_t.HashmapListNil - termination_by hashmap_hash_map_remove_from_list_loop_back key ls => - hashmap_hash_map_remove_from_list_loop_terminates - T key ls + hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ @@ -512,20 +496,19 @@ def hashmap_hash_map_remove_from_list_back 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 + 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 h: 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)) + let _ ← USize.checked_sub self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by intlit)) Result.ret (Option.some x0) - /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ def hashmap_hash_map_remove_back @@ -533,19 +516,19 @@ def hashmap_hash_map_remove_back 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 + 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 h: x with | Option.none => do - let l0 <- hashmap_hash_map_remove_from_list_back T key l - let v <- + 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 + hash_mod l0 Result.ret { hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, @@ -555,12 +538,12 @@ def hashmap_hash_map_remove_back } | 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 <- + 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 + hash_mod l0 Result.ret { hashmap_hash_map_num_entries := i0, @@ -568,91 +551,90 @@ def hashmap_hash_map_remove_back 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 <- + 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 <- + (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 <- + (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 <- + (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))) + (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 h: not (i = (UInt64.ofNatCore 18 (by intlit))) then Result.fail Error.panic else do - let hm4 <- + let hm4 ← hashmap_hash_map_get_mut_back UInt64 hm3 (USize.ofNatCore 1024 (by intlit)) - (UInt64.ofNatCore 56 (by intlit)) - let i0 <- + (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))) + (USize.ofNatCore 1024 (by intlit)) + if h: not (i0 = (UInt64.ofNatCore 56 (by intlit))) then Result.fail Error.panic else do - let x <- + let x ← hashmap_hash_map_remove_fwd UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) - match x with + (USize.ofNatCore 1024 (by intlit)) + match h: x with | Option.none => Result.fail Error.panic | Option.some x0 => - if not (x0 = (UInt64.ofNatCore 56 (by intlit))) + if h: not (x0 = (UInt64.ofNatCore 56 (by intlit))) then Result.fail Error.panic else do - let hm5 <- + let hm5 ← hashmap_hash_map_remove_back UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) - let i1 <- + (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))) + (USize.ofNatCore 0 (by intlit)) + if h: not (i1 = (UInt64.ofNatCore 42 (by intlit))) then Result.fail Error.panic else do - let i2 <- + let i2 ← hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 128 (by intlit)) - if not (i2 = (UInt64.ofNatCore 18 (by intlit))) + (USize.ofNatCore 128 (by intlit)) + if h: not (i2 = (UInt64.ofNatCore 18 (by intlit))) then Result.fail Error.panic else do - let i3 <- + let i3 ← hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 1056 (by intlit)) - if not (i3 = (UInt64.ofNatCore 256 (by intlit))) + (USize.ofNatCore 1056 (by intlit)) + if h: 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 ()) +#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) <- opaque_defs.hashmap_utils_deserialize_fwd st - let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value - let (st1, _) <- opaque_defs.hashmap_utils_serialize_fwd hm0 st0 + let (st0, hm) ← opaque_defs.hashmap_utils_deserialize_fwd st + let hm0 ← hashmap_hash_map_insert_fwd_back UInt64 hm key value + let (st1, _) ← opaque_defs.hashmap_utils_serialize_fwd hm0 st0 Result.ret (st1, ()) /- [hashmap_main::main] -/ -def main_fwd : Result Unit := Result.ret () +def main_fwd : Result Unit := + Result.ret () /- Unit test for [hashmap_main::main] -/ -#assert (main_fwd = .ret ()) +#assert (main_fwd == .ret ()) |