diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Primitives.lean | 92 | ||||
| -rw-r--r-- | compiler/Extract.ml | 9 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 100 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean | 15 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 445 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 4 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Types.lean | 4 |
7 files changed, 350 insertions, 319 deletions
diff --git a/backends/lean/Primitives.lean b/backends/lean/Primitives.lean index 79958d94..a0892ca7 100644 --- a/backends/lean/Primitives.lean +++ b/backends/lean/Primitives.lean @@ -9,69 +9,69 @@ import Mathlib.Tactic.RunCmd -- Results & monadic combinators --- TODO: use syntactic conventions and capitalize error, result, etc. - -inductive error where - | assertionFailure: error - | integerOverflow: error - | arrayOutOfBounds: error - | maximumSizeExceeded: error - | panic: error +-- TODO: use syntactic conventions and capitalize Error, Result, etc. + +inductive Error where + | assertionFailure: Error + | integerOverflow: Error + | arrayOutOfBounds: Error + | maximumSizeExceeded: Error + | panic: Error deriving Repr, BEq -open error +open Error -inductive result (α : Type u) where - | ret (v: α): result α - | fail (e: error): result α +inductive Result (α : Type u) where + | ret (v: α): Result α + | fail (e: Error): Result α deriving Repr, BEq -open result +open Result /- HELPERS -/ -- TODO: is there automated syntax for these discriminators? -def is_ret {α: Type} (r: result α): Bool := +def is_ret {α: Type} (r: Result α): Bool := match r with - | result.ret _ => true - | result.fail _ => false + | Result.ret _ => true + | Result.fail _ => false -def massert (b:Bool) : result Unit := +def massert (b:Bool) : Result Unit := if b then .ret () else fail assertionFailure -def eval_global {α: Type} (x: result α) (_: is_ret x): α := +def eval_global {α: Type} (x: Result α) (_: is_ret x): α := match x with - | result.fail _ => by contradiction - | result.ret x => x + | Result.fail _ => by contradiction + | Result.ret x => x /- DO-DSL SUPPORT -/ -def bind (x: result α) (f: α -> result β) : result β := +def bind (x: Result α) (f: α -> Result β) : Result β := match x with | ret v => f v | fail v => fail v --- Allows using result in do-blocks -instance : Bind result where +-- Allows using Result in do-blocks +instance : Bind Result where bind := bind -- Allows using return x in do-blocks -instance : Pure result where +instance : Pure Result where pure := fun x => ret x /- CUSTOM-DSL SUPPORT -/ --- Let-binding the result of a monadic operation is oftentimes not sufficient, +-- 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 } +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) + `(doElem| let ⟨$e, $h⟩ ← Result.attach $f) -- Silly example of the kind of reasoning that this notation enables #eval do @@ -99,8 +99,8 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem => -- total function over nats...? the hypothesis in the if condition is not used -- in the then-branch which confuses me quite a bit --- TODO: add a refinement for the result (just like vec_push_back below) that --- explains that the toNat of the result (in the case of success) is the sub of +-- TODO: add a refinement for the Result (just like vec_push_back below) that +-- explains that the toNat of the Result (in the case of success) is the sub of -- the toNat of the arguments (i.e. intrinsic specification) -- ... do we want intrinsic specifications for the builtins? that might require -- some careful type annotations in the monadic notation for clients, but may @@ -134,7 +134,7 @@ macro_rules -- and -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean -- which both contain a fair amount of reasoning already! -def USize.checked_sub (n: USize) (m: USize): result USize := +def USize.checked_sub (n: USize) (m: USize): Result USize := -- NOTE: the test USize.toNat n - m >= 0 seems to always succeed? if n >= m then let n' := USize.toNat n @@ -150,7 +150,7 @@ def USize.checked_sub (n: USize) (m: USize): result USize := else fail integerOverflow -def USize.checked_add (n: USize) (m: USize): result USize := +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 @@ -161,7 +161,7 @@ def USize.checked_add (n: USize) (m: USize): result USize := else .fail integerOverflow -def USize.checked_rem (n: USize) (m: USize): result USize := +def USize.checked_rem (n: USize) (m: USize): Result USize := if h: m > 0 then .ret ⟨ n.val % m.val, by have h1: ↑m.val < USize.size := m.val.isLt @@ -171,7 +171,7 @@ def USize.checked_rem (n: USize) (m: USize): result USize := else .fail integerOverflow -def USize.checked_mul (n: USize) (m: USize): result USize := +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 @@ -182,7 +182,7 @@ def USize.checked_mul (n: USize) (m: USize): result USize := else .fail integerOverflow -def USize.checked_div (n: USize) (m: USize): result USize := +def USize.checked_div (n: USize) (m: USize): Result USize := if m > 0 then .ret ⟨ n.val / m.val, by have h1: ↑n.val < USize.size := n.val.isLt @@ -209,7 +209,7 @@ run_cmd end $typeName )) -def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineInteger dst ] (x: src): result dst := +def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineInteger dst ] (x: src): Result dst := if h: MachineInteger.val x < MachineInteger.size dst then .ret (MachineInteger.ofNatCore (MachineInteger.val x).val h) else @@ -249,11 +249,11 @@ def vec_len (α : Type u) (v : vec α) : USize := def vec_push_fwd (α : Type u) (_ : vec α) (_ : α) : Unit := () -- NOTE: old version trying to use a subtype notation, but probably better to --- leave result elimination to auxiliary lemmas with suitable preconditions +-- leave Result elimination to auxiliary lemmas with suitable preconditions -- TODO: I originally wrote `List.length v.val < USize.size - 1`; how can one -- make the proof work in that case? Probably need to import tactics from -- mathlib to deal with inequalities... would love to see an example. -def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec α) // +def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: Result (vec α) // match res with | fail _ => True | ret v' => List.length v'.val = List.length v.val + 1} := if h : List.length v.val + 1 < USize.size then @@ -272,12 +272,12 @@ def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec -- annotate `x`, which relieves us of having to write `.val` on the right-hand -- side of the monadic let. let v := vec_new Nat - let x: vec Nat ← (vec_push_back_old Nat v 1: result (vec Nat)) -- WHY do we need the type annotation here? + let x: vec Nat ← (vec_push_back_old Nat v 1: Result (vec Nat)) -- WHY do we need the type annotation here? -- TODO: strengthen post-condition above and do a demo to show that we can -- safely eliminate the `fail` case return (vec_len Nat x) -def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α) +def vec_push_back (α : Type u) (v : vec α) (x : α) : Result (vec α) := if h : List.length v.val + 1 <= 4294967295 then return ⟨ List.concat v.val x, @@ -295,13 +295,13 @@ def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α) else fail maximumSizeExceeded -def vec_insert_fwd (α : Type u) (v: vec α) (i: USize) (_: α): result Unit := +def vec_insert_fwd (α : Type u) (v: vec α) (i: USize) (_: α): Result Unit := if i.val < List.length v.val then .ret () else .fail arrayOutOfBounds -def vec_insert_back (α : Type u) (v: vec α) (i: USize) (x: α): result (vec α) := +def vec_insert_back (α : Type u) (v: vec α) (i: USize) (x: α): Result (vec α) := if i.val < List.length v.val then .ret ⟨ List.set v.val i.val x, by have h: List.length v.val < USize.size := v.property @@ -311,25 +311,25 @@ def vec_insert_back (α : Type u) (v: vec α) (i: USize) (x: α): result (vec α else .fail arrayOutOfBounds -def vec_index_fwd (α : Type u) (v: vec α) (i: USize): result α := +def vec_index_fwd (α : Type u) (v: vec α) (i: USize): Result α := if h: i.val < List.length v.val then .ret (List.get v.val ⟨i.val, h⟩) else .fail arrayOutOfBounds -def vec_index_back (α : Type u) (v: vec α) (i: USize) (_: α): result Unit := +def vec_index_back (α : Type u) (v: vec α) (i: USize) (_: α): Result Unit := if i.val < List.length v.val then .ret () else .fail arrayOutOfBounds -def vec_index_mut_fwd (α : Type u) (v: vec α) (i: USize): result α := +def vec_index_mut_fwd (α : Type u) (v: vec α) (i: USize): Result α := if h: i.val < List.length v.val then .ret (List.get v.val ⟨i.val, h⟩) else .fail arrayOutOfBounds -def vec_index_mut_back (α : Type u) (v: vec α) (i: USize) (x: α): result (vec α) := +def vec_index_mut_back (α : Type u) (v: vec α) (i: USize) (x: α): Result (vec α) := if i.val < List.length v.val then .ret ⟨ List.set v.val i.val x, by have h: List.length v.val < USize.size := v.property @@ -364,7 +364,7 @@ def assertImpl : CommandElab := fun (_stx: Syntax) => do runTermElabM (fun _ => do let e ← Term.elabTerm _stx[1] none logInfo (Expr.dbgToString e) - -- How to evaluate the term and compare the result to true? + -- How to evaluate the term and compare the Result to true? pure ()) -- logInfo (Expr.dbgToString (``true)) -- throwError "TODO: assert" diff --git a/compiler/Extract.ml b/compiler/Extract.ml index df7f37e1..a2ad37f5 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -136,12 +136,17 @@ let keywords () = List.concat [ named_unops; named_binops; misc ] let assumed_adts () : (assumed_ty * string) list = - [ + List.map (fun (t, s) -> + if !backend = Lean then + t, Printf.sprintf "%c%s" (Char.uppercase_ascii s.[0]) (String.sub s 1 (String.length s - 1)) + else + t, s + ) [ (State, "state"); (Result, "result"); (Error, "error"); (Fuel, "nat"); - (Option, if !backend = Lean then "Option" else "option"); + (Option, "option"); (Vec, "vec"); ] diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index 79958d94..b3f3a1a0 100644 --- a/tests/lean/hashmap_on_disk/Base/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -9,69 +9,69 @@ import Mathlib.Tactic.RunCmd -- Results & monadic combinators --- TODO: use syntactic conventions and capitalize error, result, etc. - -inductive error where - | assertionFailure: error - | integerOverflow: error - | arrayOutOfBounds: error - | maximumSizeExceeded: error - | panic: error +-- TODO: use syntactic conventions and capitalize Error, Result, etc. + +inductive Error where + | assertionFailure: Error + | integerOverflow: Error + | arrayOutOfBounds: Error + | maximumSizeExceeded: Error + | panic: Error deriving Repr, BEq -open error +open Error -inductive result (α : Type u) where - | ret (v: α): result α - | fail (e: error): result α +inductive Result (α : Type u) where + | ret (v: α): Result α + | fail (e: Error): Result α deriving Repr, BEq -open result +open Result /- HELPERS -/ -- TODO: is there automated syntax for these discriminators? -def is_ret {α: Type} (r: result α): Bool := +def is_ret {α: Type} (r: Result α): Bool := match r with - | result.ret _ => true - | result.fail _ => false + | Result.ret _ => true + | Result.fail _ => false -def massert (b:Bool) : result Unit := +def massert (b:Bool) : Result Unit := if b then .ret () else fail assertionFailure -def eval_global {α: Type} (x: result α) (_: is_ret x): α := +def eval_global {α: Type} (x: Result α) (_: is_ret x): α := match x with - | result.fail _ => by contradiction - | result.ret x => x + | Result.fail _ => by contradiction + | Result.ret x => x /- DO-DSL SUPPORT -/ -def bind (x: result α) (f: α -> result β) : result β := +def bind (x: Result α) (f: α -> Result β) : Result β := match x with | ret v => f v | fail v => fail v --- Allows using result in do-blocks -instance : Bind result where +-- Allows using Result in do-blocks +instance : Bind Result where bind := bind -- Allows using return x in do-blocks -instance : Pure result where +instance : Pure Result where pure := fun x => ret x /- CUSTOM-DSL SUPPORT -/ --- Let-binding the result of a monadic operation is oftentimes not sufficient, +-- 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 } +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) + `(doElem| let ⟨$e, $h⟩ ← Result.attach $f) -- Silly example of the kind of reasoning that this notation enables #eval do @@ -99,8 +99,8 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem => -- total function over nats...? the hypothesis in the if condition is not used -- in the then-branch which confuses me quite a bit --- TODO: add a refinement for the result (just like vec_push_back below) that --- explains that the toNat of the result (in the case of success) is the sub of +-- TODO: add a refinement for the Result (just like vec_push_back below) that +-- explains that the toNat of the Result (in the case of success) is the sub of -- the toNat of the arguments (i.e. intrinsic specification) -- ... do we want intrinsic specifications for the builtins? that might require -- some careful type annotations in the monadic notation for clients, but may @@ -134,7 +134,7 @@ macro_rules -- and -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean -- which both contain a fair amount of reasoning already! -def USize.checked_sub (n: USize) (m: USize): result USize := +def USize.checked_sub (n: USize) (m: USize): Result USize := -- NOTE: the test USize.toNat n - m >= 0 seems to always succeed? if n >= m then let n' := USize.toNat n @@ -150,7 +150,7 @@ def USize.checked_sub (n: USize) (m: USize): result USize := else fail integerOverflow -def USize.checked_add (n: USize) (m: USize): result USize := +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 @@ -161,7 +161,7 @@ def USize.checked_add (n: USize) (m: USize): result USize := else .fail integerOverflow -def USize.checked_rem (n: USize) (m: USize): result USize := +def USize.checked_rem (n: USize) (m: USize): Result USize := if h: m > 0 then .ret ⟨ n.val % m.val, by have h1: ↑m.val < USize.size := m.val.isLt @@ -171,7 +171,7 @@ def USize.checked_rem (n: USize) (m: USize): result USize := else .fail integerOverflow -def USize.checked_mul (n: USize) (m: USize): result USize := +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 @@ -182,7 +182,7 @@ def USize.checked_mul (n: USize) (m: USize): result USize := else .fail integerOverflow -def USize.checked_div (n: USize) (m: USize): result USize := +def USize.checked_div (n: USize) (m: USize): Result USize := if m > 0 then .ret ⟨ n.val / m.val, by have h1: ↑n.val < USize.size := n.val.isLt @@ -209,7 +209,7 @@ run_cmd end $typeName )) -def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineInteger dst ] (x: src): result dst := +def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineInteger dst ] (x: src): Result dst := if h: MachineInteger.val x < MachineInteger.size dst then .ret (MachineInteger.ofNatCore (MachineInteger.val x).val h) else @@ -230,9 +230,9 @@ def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineIntege -- Note: unlike F*, Lean seems to use strict upper bounds (e.g. USize.size) -- rather than maximum values (usize_max). -def vec (α : Type u) := { l : List α // List.length l < USize.size } +def Vec (α : Type u) := { l : List α // List.length l < USize.size } -def vec_new (α : Type u): vec α := ⟨ [], by { +def vec_new (α : Type u): Vec α := ⟨ [], by { match USize.size, usize_size_eq with | _, Or.inl rfl => simp | _, Or.inr rfl => simp @@ -240,20 +240,20 @@ def vec_new (α : Type u): vec α := ⟨ [], by { #check vec_new -def vec_len (α : Type u) (v : vec α) : USize := +def vec_len (α : Type u) (v : Vec α) : USize := let ⟨ v, l ⟩ := v USize.ofNatCore (List.length v) l #eval vec_len Nat (vec_new Nat) -def vec_push_fwd (α : Type u) (_ : vec α) (_ : α) : Unit := () +def vec_push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := () -- NOTE: old version trying to use a subtype notation, but probably better to --- leave result elimination to auxiliary lemmas with suitable preconditions +-- leave Result elimination to auxiliary lemmas with suitable preconditions -- TODO: I originally wrote `List.length v.val < USize.size - 1`; how can one -- make the proof work in that case? Probably need to import tactics from -- mathlib to deal with inequalities... would love to see an example. -def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec α) // +def vec_push_back_old (α : Type u) (v : Vec α) (x : α) : { res: Result (Vec α) // match res with | fail _ => True | ret v' => List.length v'.val = List.length v.val + 1} := if h : List.length v.val + 1 < USize.size then @@ -272,12 +272,12 @@ def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec -- annotate `x`, which relieves us of having to write `.val` on the right-hand -- side of the monadic let. let v := vec_new Nat - let x: vec Nat ← (vec_push_back_old Nat v 1: result (vec Nat)) -- WHY do we need the type annotation here? + let x: Vec Nat ← (vec_push_back_old Nat v 1: Result (Vec Nat)) -- WHY do we need the type annotation here? -- TODO: strengthen post-condition above and do a demo to show that we can -- safely eliminate the `fail` case return (vec_len Nat x) -def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α) +def vec_push_back (α : Type u) (v : Vec α) (x : α) : Result (Vec α) := if h : List.length v.val + 1 <= 4294967295 then return ⟨ List.concat v.val x, @@ -295,13 +295,13 @@ def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α) else fail maximumSizeExceeded -def vec_insert_fwd (α : Type u) (v: vec α) (i: USize) (_: α): result Unit := +def vec_insert_fwd (α : Type u) (v: Vec α) (i: USize) (_: α): Result Unit := if i.val < List.length v.val then .ret () else .fail arrayOutOfBounds -def vec_insert_back (α : Type u) (v: vec α) (i: USize) (x: α): result (vec α) := +def vec_insert_back (α : Type u) (v: Vec α) (i: USize) (x: α): Result (Vec α) := if i.val < List.length v.val then .ret ⟨ List.set v.val i.val x, by have h: List.length v.val < USize.size := v.property @@ -311,25 +311,25 @@ def vec_insert_back (α : Type u) (v: vec α) (i: USize) (x: α): result (vec α else .fail arrayOutOfBounds -def vec_index_fwd (α : Type u) (v: vec α) (i: USize): result α := +def vec_index_fwd (α : Type u) (v: Vec α) (i: USize): Result α := if h: i.val < List.length v.val then .ret (List.get v.val ⟨i.val, h⟩) else .fail arrayOutOfBounds -def vec_index_back (α : Type u) (v: vec α) (i: USize) (_: α): result Unit := +def vec_index_back (α : Type u) (v: Vec α) (i: USize) (_: α): Result Unit := if i.val < List.length v.val then .ret () else .fail arrayOutOfBounds -def vec_index_mut_fwd (α : Type u) (v: vec α) (i: USize): result α := +def vec_index_mut_fwd (α : Type u) (v: Vec α) (i: USize): Result α := if h: i.val < List.length v.val then .ret (List.get v.val ⟨i.val, h⟩) else .fail arrayOutOfBounds -def vec_index_mut_back (α : Type u) (v: vec α) (i: USize) (x: α): result (vec α) := +def vec_index_mut_back (α : Type u) (v: Vec α) (i: USize) (x: α): Result (Vec α) := if i.val < List.length v.val then .ret ⟨ List.set v.val i.val x, by have h: List.length v.val < USize.size := v.property @@ -364,7 +364,7 @@ def assertImpl : CommandElab := fun (_stx: Syntax) => do runTermElabM (fun _ => do let e ← Term.elabTerm _stx[1] none logInfo (Expr.dbgToString e) - -- How to evaluate the term and compare the result to true? + -- How to evaluate the term and compare the Result to true? pure ()) -- logInfo (Expr.dbgToString (``true)) -- throwError "TODO: assert" diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean index 3466e7e0..a514c58a 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean @@ -6,7 +6,7 @@ import HashmapMain.Types /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: termination measure -/ @[simp] def hashmap_hash_map_allocate_slots_loop_terminates (T : Type) - (slots : vec (hashmap_list_t T)) (n : USize) := + (slots : Vec (hashmap_list_t T)) (n : USize) := (slots, n) syntax "hashmap_hash_map_allocate_slots_loop_decreases" term+ : tactic @@ -15,16 +15,17 @@ macro_rules | `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) => `(tactic| sorry) -/- [hashmap_main::hashmap::HashMap::{0}::clear]: termination measure -/ +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/ @[simp] -def hashmap_hash_map_clear_loop_terminates (T : Type) - (slots : vec (hashmap_list_t T)) (i : USize) := +def hashmap_hash_map_clear_slots_loop_terminates (T : Type) + (slots : Vec (hashmap_list_t T)) (i : USize) := (slots, i) -syntax "hashmap_hash_map_clear_loop_decreases" term+ : tactic +syntax "hashmap_hash_map_clear_slots_loop_decreases" term+ : tactic macro_rules -| `(tactic| hashmap_hash_map_clear_loop_decreases $slots $i) =>`(tactic| sorry) +| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) => + `(tactic| sorry) /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/ @[simp] @@ -53,7 +54,7 @@ $ls) =>`(tactic| sorry) /- [hashmap_main::hashmap::HashMap::{0}::move_elements]: termination measure -/ @[simp] def hashmap_hash_map_move_elements_loop_terminates (T : Type) - (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) (i : USize) + (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) (i : USize) := (ntable, slots, i) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 1abc9f8d..ee50f126 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -3,35 +3,35 @@ import Base.Primitives import HashmapMain.Types import HashmapMain.Opaque -import HashmapMain.Clauses.Clauses +import HashmapMain.Clauses.Template 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))) + (T : Type) (slots : Vec (hashmap_list_t T)) (n : USize) : + (Result (Vec (hashmap_list_t T))) := if 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)) + 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 + 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] -/ def hashmap_hash_map_allocate_slots_fwd - (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) : - result (vec (hashmap_list_t T)) + (T : Type) (slots : Vec (hashmap_list_t T)) (n : USize) : + Result (Vec (hashmap_list_t T)) := hashmap_hash_map_allocate_slots_loop_fwd T slots n @@ -39,14 +39,14 @@ def hashmap_hash_map_allocate_slots_fwd def hashmap_hash_map_new_with_capacity_fwd (T : Type) (capacity : USize) (max_load_dividend : USize) (max_load_divisor : USize) : - result (hashmap_hash_map_t T) + 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 - result.ret + 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)), hashmap_hash_map_max_load_factor := (max_load_dividend, @@ -56,37 +56,45 @@ def hashmap_hash_map_new_with_capacity_fwd } /- [hashmap_main::hashmap::HashMap::{0}::new] -/ -def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) := +def hashmap_hash_map_new_fwd (T : Type) : Result (hashmap_hash_map_t T) := hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by intlit)) (USize.ofNatCore 4 (by intlit)) (USize.ofNatCore 5 (by intlit)) -/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ -def hashmap_hash_map_clear_loop_fwd_back - (T : Type) (slots : vec (hashmap_list_t T)) (i : USize) : - (result (vec (hashmap_list_t T))) +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ +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 + let i0 := vec_len (hashmap_list_t T) slots if i < i0 then do - let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i - hashmap_list_t.HashmapListNil - hashmap_hash_map_clear_loop_fwd_back T slots0 i1 - else result.ret slots -termination_by hashmap_hash_map_clear_loop_fwd_back slots i => - hashmap_hash_map_clear_loop_terminates T slots i -decreasing_by hashmap_hash_map_clear_loop_decreases slots i + 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 +decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i + +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ +def hashmap_hash_map_clear_slots_fwd_back + (T : Type) (slots : Vec (hashmap_list_t T)) : + Result (Vec (hashmap_list_t T)) + := + hashmap_hash_map_clear_slots_loop_fwd_back T slots + (USize.ofNatCore 0 (by intlit)) /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ def hashmap_hash_map_clear_fwd_back - (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := + (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := do let v <- - hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots - (USize.ofNatCore 0 (by intlit)) - result.ret + 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)), hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, @@ -96,78 +104,80 @@ def hashmap_hash_map_clear_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::len] -/ def hashmap_hash_map_len_fwd - (T : Type) (self : hashmap_hash_map_t T) : result USize := - result.ret self.hashmap_hash_map_num_entries + (T : Type) (self : hashmap_hash_map_t T) : Result USize := + Result.ret self.hashmap_hash_map_num_entries /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_loop_fwd (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : - (result Bool) + (Result Bool) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key - then result.ret false + then Result.ret false else hashmap_hash_map_insert_in_list_loop_fwd T key value tl - | hashmap_list_t.HashmapListNil => result.ret true + | 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] -/ def hashmap_hash_map_insert_in_list_fwd - (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : result Bool := + (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : Result Bool := hashmap_hash_map_insert_in_list_loop_fwd T key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ 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)) + (Result (hashmap_list_t T)) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key - then result.ret (hashmap_list_t.HashmapListCons ckey value tl) + 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 - result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) + 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 - result.ret (hashmap_list_t.HashmapListCons key value l) + 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] -/ def hashmap_hash_map_insert_in_list_back (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : - result (hashmap_list_t T) + Result (hashmap_list_t T) := hashmap_hash_map_insert_in_list_loop_back T key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] -/ def hashmap_hash_map_insert_no_resize_fwd_back (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) : - result (hashmap_hash_map_t T) + 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 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 + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let inserted <- hashmap_hash_map_insert_in_list_fwd T key value l if inserted then do let i0 <- USize.checked_add self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by intlit)) - let l0 <- hashmap_hash_map_insert_in_list_back T key value l + (USize.ofNatCore 1 (by intlit)) + let l0 <- hashmap_hash_map_insert_in_list_back T key value l let v <- vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 - result.ret + hash_mod l0 + Result.ret { hashmap_hash_map_num_entries := i0, hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, @@ -176,11 +186,11 @@ 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 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 + 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, @@ -189,84 +199,85 @@ def hashmap_hash_map_insert_no_resize_fwd_back } /- [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_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) : - (result (hashmap_hash_map_t T)) + (Result (hashmap_hash_map_t T)) := 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 + 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_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] -/ 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) + 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)) + (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)))) + (Result ((hashmap_hash_map_t T) × (Vec (hashmap_list_t T)))) := - let i0 := vec_len (hashmap_list_t T) slots + 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 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 + 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)) + 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) + 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] -/ def hashmap_hash_map_move_elements_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) + (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))) + 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) := + (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 + 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 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 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 + 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), @@ -274,7 +285,7 @@ def hashmap_hash_map_try_resize_fwd_back hashmap_hash_map_slots := ntable0.hashmap_hash_map_slots } else - result.ret + Result.ret { hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, hashmap_hash_map_max_load_factor := (i, i0), @@ -285,143 +296,149 @@ def hashmap_hash_map_try_resize_fwd_back /- [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) + 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 + 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 + 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) := + (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result Bool) := match ls with | hashmap_list_t.HashmapListCons ckey t tl => if ckey = key - then result.ret true + then Result.ret true else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => result.ret false + | 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] -/ def hashmap_hash_map_contains_key_in_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := + (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 := + (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 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 + 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) := + (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result T) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key - then result.ret cvalue + 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_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] -/ def hashmap_hash_map_get_in_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := + (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 := + (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 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 + 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) := + (T : Type) (ls : hashmap_list_t T) (key : USize) : (Result T) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key - then result.ret cvalue + 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_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] -/ def hashmap_hash_map_get_mut_in_list_fwd - (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := + (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) : - (result (hashmap_list_t T)) + (Result (hashmap_list_t T)) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key - then result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl) + 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 - result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) - | hashmap_list_t.HashmapListNil => result.fail error.panic + 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] -/ 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) + 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 := + (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 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 + 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) + 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 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 + 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 + 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, @@ -431,33 +448,36 @@ 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)) := + (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result (Option T)) := 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 + 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 + 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_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] -/ def hashmap_hash_map_remove_from_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result (Option T) := + (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) : - (result (hashmap_list_t T)) + (Result (hashmap_list_t T)) := match ls with | hashmap_list_t.HashmapListCons ckey t tl => @@ -465,64 +485,68 @@ def hashmap_hash_map_remove_from_list_loop_back then let mv_ls := mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey - t tl) hashmap_list_t.HashmapListNil + 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 + | 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 - result.ret (hashmap_list_t.HashmapListCons ckey t tl0) - | hashmap_list_t.HashmapListNil => result.ret hashmap_list_t.HashmapListNil + 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] -/ def hashmap_hash_map_remove_from_list_back (T : Type) (key : USize) (ls : hashmap_list_t T) : - result (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) := + (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 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 + 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.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) + (USize.ofNatCore 1 (by intlit)) + Result.ret (Option.some x0) + /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ def hashmap_hash_map_remove_back (T : Type) (self : hashmap_hash_map_t T) (key : USize) : - result (hashmap_hash_map_t T) + 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 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 + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let x <- hashmap_hash_map_remove_from_list_fwd T key l match x with | Option.none => do - let l0 <- hashmap_hash_map_remove_from_list_back T key l + let 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 + 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, @@ -532,101 +556,102 @@ 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 + (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 + 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 := +def hashmap_test1_fwd : Result Unit := do - let hm <- hashmap_hash_map_new_fwd UInt64 + 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)) + (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)) + (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)) + (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)) + (USize.ofNatCore 1056 (by intlit)) (UInt64.ofNatCore 256 (by intlit)) let i <- - hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by intlit)) + 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 + 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)) + (UInt64.ofNatCore 56 (by intlit)) let i0 <- hashmap_hash_map_get_fwd UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) + (USize.ofNatCore 1024 (by intlit)) if not (i0 = (UInt64.ofNatCore 56 (by intlit))) - then result.fail error.panic + then Result.fail Error.panic else do let x <- hashmap_hash_map_remove_fwd UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) + (USize.ofNatCore 1024 (by intlit)) match x with - | Option.none => result.fail error.panic + | Option.none => Result.fail Error.panic | Option.some x0 => if not (x0 = (UInt64.ofNatCore 56 (by intlit))) - then result.fail error.panic + then Result.fail Error.panic else do let hm5 <- hashmap_hash_map_remove_back UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) + (USize.ofNatCore 1024 (by intlit)) let i1 <- hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 0 (by intlit)) + (USize.ofNatCore 0 (by intlit)) if not (i1 = (UInt64.ofNatCore 42 (by intlit))) - then result.fail error.panic + then Result.fail Error.panic else do let i2 <- hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 128 (by intlit)) + (USize.ofNatCore 128 (by intlit)) if not (i2 = (UInt64.ofNatCore 18 (by intlit))) - then result.fail error.panic + then Result.fail Error.panic else do let i3 <- hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 1056 (by intlit)) + (USize.ofNatCore 1056 (by intlit)) if not (i3 = (UInt64.ofNatCore 256 (by intlit))) - then result.fail error.panic - else result.ret () + 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) := + (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 - result.ret (st1, ()) + 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 ()) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean index ce618a6c..3531e6e0 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean @@ -7,9 +7,9 @@ structure OpaqueDefs where /- [hashmap_main::hashmap_utils::deserialize] -/ hashmap_utils_deserialize_fwd - : state -> result (state × (hashmap_hash_map_t UInt64)) + : State -> Result (State × (hashmap_hash_map_t UInt64)) /- [hashmap_main::hashmap_utils::serialize] -/ hashmap_utils_serialize_fwd - : hashmap_hash_map_t UInt64 -> state -> result (state × Unit) + : hashmap_hash_map_t UInt64 -> State -> Result (State × Unit) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean index 2a3ea462..40f9b7e9 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -13,7 +13,7 @@ structure hashmap_hash_map_t (T : Type) where hashmap_hash_map_num_entries : USize hashmap_hash_map_max_load_factor : (USize × USize) hashmap_hash_map_max_load : USize - hashmap_hash_map_slots : vec (hashmap_list_t T) + hashmap_hash_map_slots : Vec (hashmap_list_t T) -/- The state type used in the state-error monad -/ axiom state : Type +/- The state type used in the state-error monad -/ axiom State : Type |