From e1ee59f6a45482e93901f6a549f594fd6ef15234 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 25 Jan 2023 13:12:01 -0800 Subject: New directory structure and corresponding extraction, + misc fixes, for Lean --- .gitignore | 1 + backends/lean/primitives.lean | 16 +- compiler/Extract.ml | 23 +- compiler/ExtractBase.ml | 2 +- compiler/Translate.ml | 62 ++- tests/lean/hashmap_on_disk/Base/Primitives.lean | 176 +++++++ tests/lean/hashmap_on_disk/Hashmap.lean | 1 - tests/lean/hashmap_on_disk/Hashmap/Funs.lean | 535 --------------------- tests/lean/hashmap_on_disk/Hashmap/Opaque.lean | 11 - tests/lean/hashmap_on_disk/Hashmap/Primitives.lean | 174 ------- tests/lean/hashmap_on_disk/Hashmap/Types.lean | 23 - tests/lean/hashmap_on_disk/HashmapMain.lean | 1 + tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 530 ++++++++++++++++++++ tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 13 + tests/lean/hashmap_on_disk/HashmapMain/Types.lean | 26 + tests/lean/hashmap_on_disk/Main.lean | 4 +- tests/lean/hashmap_on_disk/lakefile.lean | 6 +- 17 files changed, 812 insertions(+), 792 deletions(-) create mode 100644 tests/lean/hashmap_on_disk/Base/Primitives.lean delete mode 100644 tests/lean/hashmap_on_disk/Hashmap.lean delete mode 100644 tests/lean/hashmap_on_disk/Hashmap/Funs.lean delete mode 100644 tests/lean/hashmap_on_disk/Hashmap/Opaque.lean delete mode 100644 tests/lean/hashmap_on_disk/Hashmap/Primitives.lean delete mode 100644 tests/lean/hashmap_on_disk/Hashmap/Types.lean create mode 100644 tests/lean/hashmap_on_disk/HashmapMain.lean create mode 100644 tests/lean/hashmap_on_disk/HashmapMain/Funs.lean create mode 100644 tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean create mode 100644 tests/lean/hashmap_on_disk/HashmapMain/Types.lean diff --git a/.gitignore b/.gitignore index d0a4be47..e8b8b7a4 100644 --- a/.gitignore +++ b/.gitignore @@ -67,3 +67,4 @@ nohup.out *.txt */.#* *.smt2 +.DS_Store diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean index d86c0423..9e72b708 100644 --- a/backends/lean/primitives.lean +++ b/backends/lean/primitives.lean @@ -131,26 +131,28 @@ macro_rules def vec (α : Type u) := { l : List α // List.length l < USize.size } -def vec_new : result (vec α) := return ⟨ [], by { +def vec_new (α : Type u): result (vec α) := return ⟨ [], by { match USize.size, usize_size_eq with | _, Or.inl rfl => simp | _, Or.inr rfl => simp } ⟩ -def vec_len (v : vec α) : USize := +#check vec_new + +def vec_len (α : Type u) (v : vec α) : USize := let ⟨ v, l ⟩ := v USize.ofNatCore (List.length v) l #eval do - return (vec_len (<- @vec_new Nat)) + return (vec_len Nat (<- vec_new Nat)) -def vec_push_fwd (_ : vec α) (_ : α) : Unit := () +def vec_push_fwd (α : Type u) (_ : vec α) (_ : α) : Unit := () -- TODO: more precise error condition here for the fail case -- 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 (v : vec α) (x : α) : { res: result (vec α) // +def vec_push_back (α : 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 @@ -168,7 +170,7 @@ def vec_push_back (v : vec α) (x : α) : { res: result (vec α) // -- select the `val` field if the context provides a type annotation. We -- annotate `x`, which relieves us of having to write `.val` on the right-hand -- side of the monadic let. - let x: vec Nat ← vec_push_back (<- vec_new) 1 + let x: vec Nat ← vec_push_back Nat (<- vec_new Nat) 1 -- TODO: strengthen post-condition above and do a demo to show that we can -- safely eliminate the `fail` case - return (vec_len x) + return (vec_len Nat x) diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 9496fcf9..af510a84 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -175,8 +175,8 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = ] | Lean -> [ - (Result, result_return_id, "ret"); - (Result, result_fail_id, "fail_"); (* TODO: why the _ *) + (Result, result_return_id, "result.ret"); + (Result, result_fail_id, "result.fail"); (Error, error_failure_id, "panic"); (* No Fuel::Zero on purpose *) (* No Fuel::Succ on purpose *) @@ -218,7 +218,7 @@ let assumed_pure_functions : (pure_assumed_fun_id * string) list = | Lean -> [ (Return, "return"); - (Fail, "fail_"); + (Fail, "fail"); (Assert, "massert"); (* TODO: figure out how to deal with this *) (FuelDecrease, "decrease"); @@ -296,7 +296,7 @@ let extract_binop (extract_expr : bool -> texpression -> unit) if inside then F.pp_print_string fmt ")" let type_decl_kind_to_qualif (kind : decl_kind) - (type_kind : type_decl_kind option) (is_rec: bool): string = + (type_kind : type_decl_kind option): string = match !backend with | FStar -> ( match kind with @@ -321,8 +321,7 @@ let type_decl_kind_to_qualif (kind : decl_kind) | _ -> raise (Failure "Unexpected")) | Lean -> ( match kind with - | SingleNonRec -> - if type_kind = Some Struct && not is_rec then "structure" else "inductive" + | SingleNonRec -> if type_kind = Some Struct then "structure" else "inductive" | SingleRec -> "inductive" | MutRecFirst -> "mutual inductive" | MutRecInner -> "inductive" @@ -640,7 +639,8 @@ let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) = F.pp_print_cut fmt (); F.pp_print_string fmt ".") -let unit_name = match !backend with | Lean -> "Unit" | Coq | FStar -> "unit" +let unit_name () = + match !backend with | Lean -> "Unit" | Coq | FStar -> "unit" (** [inside] constrols whether we should add parentheses or not around type applications (if [true] we add parentheses). @@ -653,7 +653,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) | Tuple -> (* This is a bit annoying, but in F*/Coq [()] is not the unit type: * we have to write [unit]... *) - if tys = [] then F.pp_print_string fmt unit_name + if tys = [] then F.pp_print_string fmt (unit_name ()) else ( F.pp_print_string fmt "("; Collections.List.iter_link @@ -882,7 +882,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) let _ = if !backend = FStar && fields = [] then ( F.pp_print_space fmt (); - F.pp_print_string fmt unit_name) + F.pp_print_string fmt (unit_name ())) else if (not is_rec) || !backend = FStar then ( F.pp_print_space fmt (); (* If Coq: print the constructor name *) @@ -983,8 +983,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *) F.pp_open_hovbox fmt ctx.indent_incr; (* > "type TYPE_NAME" *) - let is_rec = decl_is_from_rec_group kind in - let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind is_rec in + let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in F.pp_print_string fmt (qualif ^ " " ^ def_name); (* Print the type parameters *) let type_keyword = match !backend with FStar -> "Type0" | Coq | Lean -> "Type" in @@ -1011,7 +1010,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) let eq = match !backend with | FStar -> "=" | Coq -> ":=" - | Lean -> if type_kind = Some Struct && not is_rec then "where" else ":=" + | Lean -> if type_kind = Some Struct && kind = SingleNonRec then "where" else ":=" in F.pp_print_string fmt eq) else ( diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index c8094128..3ad55d37 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -118,7 +118,7 @@ type formatter = { char_name : string; int_name : integer_type -> string; str_name : string; - type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> bool -> string; + type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> string; (** Compute the qualified for a type definition/declaration. For instance: "type", "and", etc. diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 6b3d00f3..b2162b20 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -708,7 +708,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) custom_includes; Printf.fprintf out "Module %s.\n" module_name | Lean -> - Printf.fprintf out "import Primitives\nopen result\n\n"; + Printf.fprintf out "import Base.Primitives\n"; (* Add the custom imports *) List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports; (* Add the custom includes *) @@ -845,11 +845,30 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : trans_funs) in + let mkdir_if dest_dir = + if not (Sys.file_exists dest_dir) then ( + log#linfo (lazy ("Creating missing directory: " ^ dest_dir)); + (* Create a directory with *default* permissions *) + Core_unix.mkdir_p dest_dir) + in + (* Create the directory, if necessary *) - if not (Sys.file_exists dest_dir) then ( - log#linfo (lazy ("Creating missing directory: " ^ dest_dir)); - (* Create a directory with *default* permissions *) - Core_unix.mkdir_p dest_dir); + mkdir_if dest_dir; + + let needs_clauses_module = + !Config.extract_decreases_clauses + && not (PureUtils.FunLoopIdSet.is_empty rec_functions) + in + + (* Lean reflects the module hierarchy within the filesystem, so we need to + create more directories *) + if !Config.backend = Lean then begin + let (^^) = Filename.concat in + mkdir_if (dest_dir ^^ "Base"); + mkdir_if (dest_dir ^^ module_name); + if needs_clauses_module then + mkdir_if (dest_dir ^^ module_name ^^ "Clauses"); + end; (* Copy the "Primitives" file *) let _ = @@ -859,7 +878,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : match !Config.backend with | Config.FStar -> ("/backends/fstar/Primitives.fst", "Primitives.fst") | Config.Coq -> ("/backends/coq/Primitives.v", "Primitives.v") - | Config.Lean -> ("/backends/lean/Primitives.lean", "Primitives.lean") + | Config.Lean -> ("/backends/lean/Primitives.lean", "Base/Primitives.lean") in let src = open_in (exe_dir ^ primitives_src) in let tgt_filename = Filename.concat dest_dir primitives_destname in @@ -889,7 +908,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : in let module_delimiter = - match !Config.backend with FStar | Lean -> "." | Coq -> "_" + match !Config.backend with FStar -> "." | Coq -> "_" | Lean -> "." + in + let file_delimiter = + if !Config.backend = Lean then "/" else module_delimiter in let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" in @@ -922,11 +944,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : | Coq -> ".v" | Lean -> ".lean" in - let types_file_suffix = module_delimiter ^ "Types" in let types_filename = - extract_filebasename ^ types_file_suffix ^ types_filename_ext + extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext in - let types_module = module_name ^ types_file_suffix in + let types_module = module_name ^ module_delimiter ^ "Types" in let types_config = { base_gen_config with @@ -940,16 +961,9 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : ": type definitions" [] []; (* Extract the template clauses *) - let needs_clauses_module = - !Config.extract_decreases_clauses - && not (PureUtils.FunLoopIdSet.is_empty rec_functions) - in if needs_clauses_module && !Config.extract_template_decreases_clauses then ( - let clauses_file_suffix = - module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template" - in - let clauses_filename = extract_filebasename ^ clauses_file_suffix ^ ext in - let clauses_module = module_name ^ clauses_file_suffix in + let clauses_filename = extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter ^ "Template" ^ ext in + let clauses_module = module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template" in let clauses_config = { base_gen_config with extract_template_decreases_clauses = true } in @@ -960,9 +974,8 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : (* Extract the opaque functions, if needed *) let opaque_funs_module = if has_opaque_funs then ( - let opaque_file_suffix = module_delimiter ^ "Opaque" in - let opaque_filename = extract_filebasename ^ opaque_file_suffix ^ ext in - let opaque_module = module_name ^ opaque_file_suffix in + let opaque_filename = extract_filebasename ^ file_delimiter ^ "Opaque" ^ ext in + let opaque_module = module_name ^ module_delimiter ^ "Opaque" in let opaque_config = { base_gen_config with @@ -979,9 +992,8 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : in (* Extract the functions *) - let fun_file_suffix = module_delimiter ^ "Funs" in - let fun_filename = extract_filebasename ^ fun_file_suffix ^ ext in - let fun_module = module_name ^ fun_file_suffix in + let fun_filename = extract_filebasename ^ file_delimiter ^ "Funs" ^ ext in + let fun_module = module_name ^ module_delimiter ^ "Funs" in let fun_config = { base_gen_config with diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean new file mode 100644 index 00000000..9e72b708 --- /dev/null +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -0,0 +1,176 @@ +------------- +-- PRELUDE -- +------------- + +-- Results & monadic combinators + +inductive error where + | assertionFailure: error + | integerOverflow: error + | arrayOutOfBounds: error + | maximumSizeExceeded: error + | panic: error +deriving Repr + +open error + +inductive result (α : Type u) where + | ret (v: α): result α + | fail (e: error): result α +deriving Repr + +open result + +-- TODO: is there automated syntax for these discriminators? +def is_ret {α: Type} (r: result α): Bool := + match r with + | result.ret _ => true + | result.fail _ => false + +def eval_global {α: Type} (x: result α) (h: is_ret x): α := + match x with + | result.fail _ => by contradiction + | result.ret x => x + +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 + bind := bind + +-- Allows using return x in do-blocks +instance : Pure result where + pure := fun x => ret x + +def massert (b:Bool) : result Unit := + if b then return () else fail assertionFailure + +-- Machine integers + +-- NOTE: we reuse the USize type from prelude.lean, because at least we know +-- it's defined in an idiomatic style that is going to make proofs easy (and +-- indeed, several proofs here are much shortened compared to Aymeric's earlier +-- attempt.) This is not stricto sensu the *correct* thing to do, because one +-- can query at run-time the value of USize, which we do *not* want to do (we +-- don't know what target we'll run on!), but when the day comes, we'll just +-- define our own USize. +-- ANOTHER NOTE: there is USize.sub but it has wraparound semantics, which is +-- not something we want to define (I think), so we use our own monadic sub (but +-- is it in line with the Rust behavior?) + +-- TODO: I am somewhat under the impression that subtraction is defined as a +-- 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 +-- 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 +-- give us more "for free" + +-- Note from Chris Bailey: "If there's more than one salient property of your +-- definition then the subtyping strategy might get messy, and the property part +-- of a subtype is less discoverable by the simplifier or tactics like +-- library_search." Try to settle this with a Lean expert on what is the most +-- productive way to go about this? + +-- Further thoughts: look at what has been done here: +-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean +-- 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 := + -- NOTE: the test USize.toNat n - m >= 0 seems to always succeed? + if n >= m then + let n' := USize.toNat n + let m' := USize.toNat n + let r := USize.ofNatCore (n' - m') (by + have h: n' - m' <= n' := by + apply Nat.sub_le_of_le_add + case h => rewrite [ Nat.add_comm ]; apply Nat.le_add_left + apply Nat.lt_of_le_of_lt h + apply n.val.isLt + ) + return r + else + fail integerOverflow + +-- TODO: settle the style for usize_sub before we write these +def USize.checked_mul (n: USize) (m: USize): result USize := sorry +def USize.checked_div (n: USize) (m: USize): result USize := sorry + +-- One needs to perform a little bit of reasoning in order to successfully +-- inject constants into USize, so we provide a general-purpose macro + +syntax "intlit" : tactic + +macro_rules + | `(tactic| intlit) => `(tactic| + match USize.size, usize_size_eq with + | _, Or.inl rfl => decide + | _, Or.inr rfl => decide) + +-- This is how the macro is expected to be used +#eval USize.ofNatCore 0 (by intlit) + +-- Also works for other integer types (at the expense of a needless disjunction) +#eval UInt32.ofNatCore 0 (by intlit) + +-- Test behavior... +#eval USize.checked_sub 10 20 +#eval USize.checked_sub 20 10 +-- NOTE: compare with concrete behavior here, which I do not think we want +#eval USize.sub 0 1 +#eval UInt8.add 255 255 + +-- Vectors + +def vec (α : Type u) := { l : List α // List.length l < USize.size } + +def vec_new (α : Type u): result (vec α) := return ⟨ [], by { + match USize.size, usize_size_eq with + | _, Or.inl rfl => simp + | _, Or.inr rfl => simp + } ⟩ + +#check vec_new + +def vec_len (α : Type u) (v : vec α) : USize := + let ⟨ v, l ⟩ := v + USize.ofNatCore (List.length v) l + +#eval do + return (vec_len Nat (<- vec_new Nat)) + +def vec_push_fwd (α : Type u) (_ : vec α) (_ : α) : Unit := () + +-- TODO: more precise error condition here for the fail case +-- 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 (α : 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 + ⟨ return ⟨List.concat v.val x, + by + rw [List.length_concat] + assumption + ⟩, by simp ⟩ + else + ⟨ fail maximumSizeExceeded, by simp ⟩ + +#eval do + -- NOTE: the // notation is syntactic sugar for Subtype, a refinement with + -- fields val and property. However, Lean's elaborator can automatically + -- select the `val` field if the context provides a type annotation. We + -- annotate `x`, which relieves us of having to write `.val` on the right-hand + -- side of the monadic let. + let x: vec Nat ← vec_push_back Nat (<- vec_new Nat) 1 + -- TODO: strengthen post-condition above and do a demo to show that we can + -- safely eliminate the `fail` case + return (vec_len Nat x) diff --git a/tests/lean/hashmap_on_disk/Hashmap.lean b/tests/lean/hashmap_on_disk/Hashmap.lean deleted file mode 100644 index e99d3a6f..00000000 --- a/tests/lean/hashmap_on_disk/Hashmap.lean +++ /dev/null @@ -1 +0,0 @@ -def hello := "world" \ No newline at end of file diff --git a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean deleted file mode 100644 index c67a37ff..00000000 --- a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean +++ /dev/null @@ -1,535 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [hashmap_main]: function definitions -import Hashmap.Primitives -import Hashmap.Opaque -import Hashmap.Types - -open result -open hashmap_list_t - -/- [hashmap_main::hashmap::hash_key] -/ -def hashmap_hash_key_fwd (k : USize) : result USize := 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)) - then do - let slots0: vec (hashmap_list_t T) <- @vec_push_back (hashmap_list_t T) slots HashmapListNil - let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) - hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 - else ret slots -termination_by hashmap_hash_map_allocate_slots_loop_fwd _ _ n => n -decreasing_by sorry - -/- [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)) - := - hashmap_hash_map_allocate_slots_loop_fwd T slots n - -/- [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] -/ -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) - := - let v <- vec_new (hashmap_list_t T) in - let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity in - let i <- USize.checked_mul capacity max_load_dividend in - let i0 <- USize.checked_div i max_load_divisor in - ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by simp)) (max_load_dividend, - max_load_divisor) i0 slots) - -/- [hashmap_main::hashmap::HashMap::{0}::new] -/ -def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) := - hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by simp)) - (USize.ofNatCore 4 (by simp)) (USize.ofNatCore 5 (by simp)) - -/- [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 in - if i < i0 - then ( - let i1 <- USize.checked_add i (USize.ofNatCore 1 (by simp)) in - let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i HashmapListNil - in - hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1) - else ret slots - -/- [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 simp)) - -/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ -def hashmap_hash_map_clear_fwd_back - (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := - let v <- hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots - in - ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by simp)) - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) - -/- [hashmap_main::hashmap::HashMap::{0}::len] -/ -def hashmap_hash_map_len_fwd - (T : Type) (self : hashmap_hash_map_t T) : result USize := - 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 := - match ls with - | HashmapListCons ckey cvalue tl => - if ckey = key - then ret false - else hashmap_hash_map_insert_in_list_loop_fwd T key value tl - | HashmapListNil => ret true - end - -/- [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 := - 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) - := - match ls with - | HashmapListCons ckey cvalue tl => - if ckey = key - then ret (HashmapListCons ckey value tl) - else ( - let l <- hashmap_hash_map_insert_in_list_loop_back T key value tl in - ret (HashmapListCons ckey cvalue l)) - | HashmapListNil => - let l <- HashmapListNil in ret (HashmapListCons key value l) - end - -/- [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) - := - 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) - := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - in - let inserted <- hashmap_hash_map_insert_in_list_fwd T key value l in - if inserted - then ( - let i0 <- USize.checked_add self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by simp)) in - let l0 <- hashmap_hash_map_insert_in_list_back T key value l in - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 in - ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v)) - else ( - let l0 <- hashmap_hash_map_insert_in_list_back T key value l in - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 in - ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)) - -/- [core::num::u32::{9}::MAX] -/ -def core_num_u32_max_body : result UInt32 := - ret (UInt32.ofNatCore 4294967295 (by simp)) -def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body - -/- [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) - := - match ls with - | HashmapListCons k v tl => - let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v in - hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl - | HashmapListNil => ret ntable - end - -/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ -def hashmap_hash_map_move_elements_from_list_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : - result (hashmap_hash_map_t T) - := - hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable ls - -/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ -def hashmap_hash_map_move_elements_loop_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) - (i : USize) : - result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) - := - let i0 <- vec_len (hashmap_list_t T) slots in - if i < i0 - then ( - let l <- vec_index_mut_fwd (hashmap_list_t T) slots i in - let ls <- mem_replace_fwd (hashmap_list_t T) l HashmapListNil in - let ntable0 <- - hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls in - let i1 <- USize.checked_add i (USize.ofNatCore 1 (by simp)) in - let l0 <- mem_replace_back (hashmap_list_t T) l HashmapListNil in - let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i l0 in - hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1) - else ret (ntable, slots) - -/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ -def hashmap_hash_map_move_elements_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) - (i : USize) : - result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) - := - hashmap_hash_map_move_elements_loop_fwd_back T ntable slots i - -/- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ -def hashmap_hash_map_try_resize_fwd_back - (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := - let max_usize <- scalar_cast U32 Usize core_num_u32_max_c in - let capacity <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by simp)) in - let (i, i0) <- self.hashmap_hash_map_max_load_factor in - let i1 <- USize.checked_div n1 i in - if capacity <= i1 - then ( - let i2 <- USize.checked_mul capacity (USize.ofNatCore 2 (by simp)) in - let ntable <- hashmap_hash_map_new_with_capacity_fwd T i2 i i0 in - let (ntable0, _) <- - hashmap_hash_map_move_elements_fwd_back T ntable - self.hashmap_hash_map_slots (USize.ofNatCore 0 (by simp)) in - ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) - ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots)) - else - ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) - self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) - -/- [hashmap_main::hashmap::HashMap::{0}::insert] -/ -def hashmap_hash_map_insert_fwd_back - (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) : - result (hashmap_hash_map_t T) - := - let self0 <- hashmap_hash_map_insert_no_resize_fwd_back T self key value in - let i <- hashmap_hash_map_len_fwd T self0 in - if i > self0.hashmap_hash_map_max_load - then hashmap_hash_map_try_resize_fwd_back T self0 - else ret self0 - -/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ -def hashmap_hash_map_contains_key_in_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := - match ls with - | HashmapListCons ckey t tl => - if ckey = key - then ret true - else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl - | HashmapListNil => ret false - end - -/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ -def hashmap_hash_map_contains_key_in_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := - hashmap_hash_map_contains_key_in_list_loop_fwd T key ls - -/- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ -def hashmap_hash_map_contains_key_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result Bool := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in - hashmap_hash_map_contains_key_in_list_fwd T key l - -/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ -def hashmap_hash_map_get_in_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := - match ls with - | HashmapListCons ckey cvalue tl => - if ckey = key - then ret cvalue - else hashmap_hash_map_get_in_list_loop_fwd T key tl - | HashmapListNil => fail_ panic - end - -/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ -def hashmap_hash_map_get_in_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := - hashmap_hash_map_get_in_list_loop_fwd T key ls - -/- [hashmap_main::hashmap::HashMap::{0}::get] -/ -def hashmap_hash_map_get_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in - hashmap_hash_map_get_in_list_fwd T key l - -/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -def hashmap_hash_map_get_mut_in_list_loop_fwd - (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := - match ls with - | HashmapListCons ckey cvalue tl => - if ckey = key - then ret cvalue - else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key - | HashmapListNil => fail_ panic - end - -/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -def hashmap_hash_map_get_mut_in_list_fwd - (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := - hashmap_hash_map_get_mut_in_list_loop_fwd T ls key - -/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -def hashmap_hash_map_get_mut_in_list_loop_back - (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : - result (hashmap_list_t T) - := - match ls with - | HashmapListCons ckey cvalue tl => - if ckey = key - then ret (HashmapListCons ckey ret0 tl) - else ( - let l <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 in - ret (HashmapListCons ckey cvalue l)) - | HashmapListNil => fail_ panic - end - -/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -def hashmap_hash_map_get_mut_in_list_back - (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : - result (hashmap_list_t T) - := - hashmap_hash_map_get_mut_in_list_loop_back T ls key ret0 - -/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ -def hashmap_hash_map_get_mut_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - in - hashmap_hash_map_get_mut_in_list_fwd T l key - -/- [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) - := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - in - let l0 <- hashmap_hash_map_get_mut_in_list_back T l key ret0 in - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - l0 in - ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) - -/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -def hashmap_hash_map_remove_from_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result (option T) := - match ls with - | HashmapListCons ckey t tl => - if ckey = key - then - let mv_ls <- - mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl) - HashmapListNil in - match mv_ls with - | HashmapListCons i cvalue tl0 => ret (@some cvalue) - | HashmapListNil => fail_ panic - end - else hashmap_hash_map_remove_from_list_loop_fwd T key tl - | HashmapListNil => ret @none - end - -/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -def hashmap_hash_map_remove_from_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result (option T) := - hashmap_hash_map_remove_from_list_loop_fwd T key ls - -/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -def hashmap_hash_map_remove_from_list_loop_back - (T : Type) (key : USize) (ls : hashmap_list_t T) : - result (hashmap_list_t T) - := - match ls with - | HashmapListCons ckey t tl => - if ckey = key - then - let mv_ls <- - mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl) - HashmapListNil in - match mv_ls with - | HashmapListCons i cvalue tl0 => ret tl0 - | HashmapListNil => fail_ panic - end - else ( - let l <- hashmap_hash_map_remove_from_list_loop_back T key tl in - ret (HashmapListCons ckey t l)) - | HashmapListNil => ret HashmapListNil - end - -/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -def hashmap_hash_map_remove_from_list_back - (T : Type) (key : USize) (ls : hashmap_list_t T) : - result (hashmap_list_t T) - := - hashmap_hash_map_remove_from_list_loop_back T key ls - -/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ -def hashmap_hash_map_remove_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result (option T) := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - in - let x <- hashmap_hash_map_remove_from_list_fwd T key l in - match x with - | @none => ret @none - | @some x0 => - let _ <- USize.checked_sub self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by simp)) in - ret (@some x0) - end - -/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ -def hashmap_hash_map_remove_back - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : - result (hashmap_hash_map_t T) - := - let hash <- hashmap_hash_key_fwd key in - let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let hash_mod <- USize.checked_rem hash i in - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - in - let x <- hashmap_hash_map_remove_from_list_fwd T key l in - match x with - | @none => - let l0 <- hashmap_hash_map_remove_from_list_back T key l in - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 in - ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) - | @some x0 => - let i0 <- USize.checked_sub self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by simp)) in - let l0 <- hashmap_hash_map_remove_from_list_back T key l in - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 in - ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - -/- [hashmap_main::hashmap::test1] -/ -def hashmap_test1_fwd : result unit := - let hm <- hashmap_hash_map_new_fwd UInt64 in - let hm0 <- - hashmap_hash_map_insert_fwd_back UInt64 hm (USize.ofNatCore 0 (by simp)) - (UInt64.ofNatCore 42 (by simp)) in - let hm1 <- - hashmap_hash_map_insert_fwd_back UInt64 hm0 (USize.ofNatCore 128 (by simp)) - (UInt64.ofNatCore 18 (by simp)) in - let hm2 <- - hashmap_hash_map_insert_fwd_back UInt64 hm1 - (USize.ofNatCore 1024 (by simp)) (UInt64.ofNatCore 138 (by simp)) in - let hm3 <- - hashmap_hash_map_insert_fwd_back UInt64 hm2 - (USize.ofNatCore 1056 (by simp)) (UInt64.ofNatCore 256 (by simp)) in - let i <- hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by simp)) - in - if not (i = (UInt64.ofNatCore 18 (by simp))) - then fail_ panic - else ( - let hm4 <- - hashmap_hash_map_get_mut_back UInt64 hm3 (USize.ofNatCore 1024 (by simp)) - (UInt64.ofNatCore 56 (by simp)) in - let i0 <- - hashmap_hash_map_get_fwd UInt64 hm4 (USize.ofNatCore 1024 (by simp)) in - if not (i0 = (UInt64.ofNatCore 56 (by simp))) - then fail_ panic - else ( - let x <- - hashmap_hash_map_remove_fwd UInt64 hm4 (USize.ofNatCore 1024 (by simp)) - in - match x with - | @none => fail_ panic - | @some x0 => - if not (x0 = (UInt64.ofNatCore 56 (by simp))) - then fail_ panic - else ( - let hm5 <- - hashmap_hash_map_remove_back UInt64 hm4 - (USize.ofNatCore 1024 (by simp)) in - let i1 <- - hashmap_hash_map_get_fwd UInt64 hm5 (USize.ofNatCore 0 (by simp)) - in - if not (i1 = (UInt64.ofNatCore 42 (by simp))) - then fail_ panic - else ( - let i2 <- - hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 128 (by simp)) in - if not (i2 = (UInt64.ofNatCore 18 (by simp))) - then fail_ panic - else ( - let i3 <- - hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 1056 (by simp)) in - if not (i3 = (UInt64.ofNatCore 256 (by simp))) - then fail_ panic - else ret ()))) - end)) - -/- 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) := - let (st0, hm) <- hashmap_utils_deserialize_fwd st in - let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value in - let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 in - ret (st1, ()) - -/- [hashmap_main::main] -/ -def main_fwd : result unit := ret () - -/- Unit test for [hashmap_main::main] -/ -#assert (main_fwd = ret ()) - diff --git a/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean b/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean deleted file mode 100644 index 164995f0..00000000 --- a/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean +++ /dev/null @@ -1,11 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [hashmap_main]: opaque function definitions -import Hashmap.Primitives -import Hashmap.Types - -/- [hashmap_main::hashmap_utils::deserialize] -/ -axiom hashmap_utils_deserialize_fwd: state → result (state × (hashmap_hash_map_t UInt64)) - -/- [hashmap_main::hashmap_utils::serialize] -/ -axiom hashmap_utils_serialize_fwd: hashmap_hash_map_t UInt64 -> state -> result (state × Unit) - diff --git a/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean b/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean deleted file mode 100644 index d86c0423..00000000 --- a/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean +++ /dev/null @@ -1,174 +0,0 @@ -------------- --- PRELUDE -- -------------- - --- Results & monadic combinators - -inductive error where - | assertionFailure: error - | integerOverflow: error - | arrayOutOfBounds: error - | maximumSizeExceeded: error - | panic: error -deriving Repr - -open error - -inductive result (α : Type u) where - | ret (v: α): result α - | fail (e: error): result α -deriving Repr - -open result - --- TODO: is there automated syntax for these discriminators? -def is_ret {α: Type} (r: result α): Bool := - match r with - | result.ret _ => true - | result.fail _ => false - -def eval_global {α: Type} (x: result α) (h: is_ret x): α := - match x with - | result.fail _ => by contradiction - | result.ret x => x - -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 - bind := bind - --- Allows using return x in do-blocks -instance : Pure result where - pure := fun x => ret x - -def massert (b:Bool) : result Unit := - if b then return () else fail assertionFailure - --- Machine integers - --- NOTE: we reuse the USize type from prelude.lean, because at least we know --- it's defined in an idiomatic style that is going to make proofs easy (and --- indeed, several proofs here are much shortened compared to Aymeric's earlier --- attempt.) This is not stricto sensu the *correct* thing to do, because one --- can query at run-time the value of USize, which we do *not* want to do (we --- don't know what target we'll run on!), but when the day comes, we'll just --- define our own USize. --- ANOTHER NOTE: there is USize.sub but it has wraparound semantics, which is --- not something we want to define (I think), so we use our own monadic sub (but --- is it in line with the Rust behavior?) - --- TODO: I am somewhat under the impression that subtraction is defined as a --- 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 --- 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 --- give us more "for free" - --- Note from Chris Bailey: "If there's more than one salient property of your --- definition then the subtyping strategy might get messy, and the property part --- of a subtype is less discoverable by the simplifier or tactics like --- library_search." Try to settle this with a Lean expert on what is the most --- productive way to go about this? - --- Further thoughts: look at what has been done here: --- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean --- 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 := - -- NOTE: the test USize.toNat n - m >= 0 seems to always succeed? - if n >= m then - let n' := USize.toNat n - let m' := USize.toNat n - let r := USize.ofNatCore (n' - m') (by - have h: n' - m' <= n' := by - apply Nat.sub_le_of_le_add - case h => rewrite [ Nat.add_comm ]; apply Nat.le_add_left - apply Nat.lt_of_le_of_lt h - apply n.val.isLt - ) - return r - else - fail integerOverflow - --- TODO: settle the style for usize_sub before we write these -def USize.checked_mul (n: USize) (m: USize): result USize := sorry -def USize.checked_div (n: USize) (m: USize): result USize := sorry - --- One needs to perform a little bit of reasoning in order to successfully --- inject constants into USize, so we provide a general-purpose macro - -syntax "intlit" : tactic - -macro_rules - | `(tactic| intlit) => `(tactic| - match USize.size, usize_size_eq with - | _, Or.inl rfl => decide - | _, Or.inr rfl => decide) - --- This is how the macro is expected to be used -#eval USize.ofNatCore 0 (by intlit) - --- Also works for other integer types (at the expense of a needless disjunction) -#eval UInt32.ofNatCore 0 (by intlit) - --- Test behavior... -#eval USize.checked_sub 10 20 -#eval USize.checked_sub 20 10 --- NOTE: compare with concrete behavior here, which I do not think we want -#eval USize.sub 0 1 -#eval UInt8.add 255 255 - --- Vectors - -def vec (α : Type u) := { l : List α // List.length l < USize.size } - -def vec_new : result (vec α) := return ⟨ [], by { - match USize.size, usize_size_eq with - | _, Or.inl rfl => simp - | _, Or.inr rfl => simp - } ⟩ - -def vec_len (v : vec α) : USize := - let ⟨ v, l ⟩ := v - USize.ofNatCore (List.length v) l - -#eval do - return (vec_len (<- @vec_new Nat)) - -def vec_push_fwd (_ : vec α) (_ : α) : Unit := () - --- TODO: more precise error condition here for the fail case --- 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 (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 - ⟨ return ⟨List.concat v.val x, - by - rw [List.length_concat] - assumption - ⟩, by simp ⟩ - else - ⟨ fail maximumSizeExceeded, by simp ⟩ - -#eval do - -- NOTE: the // notation is syntactic sugar for Subtype, a refinement with - -- fields val and property. However, Lean's elaborator can automatically - -- select the `val` field if the context provides a type annotation. We - -- annotate `x`, which relieves us of having to write `.val` on the right-hand - -- side of the monadic let. - let x: vec Nat ← vec_push_back (<- vec_new) 1 - -- TODO: strengthen post-condition above and do a demo to show that we can - -- safely eliminate the `fail` case - return (vec_len x) diff --git a/tests/lean/hashmap_on_disk/Hashmap/Types.lean b/tests/lean/hashmap_on_disk/Hashmap/Types.lean deleted file mode 100644 index 90022fe5..00000000 --- a/tests/lean/hashmap_on_disk/Hashmap/Types.lean +++ /dev/null @@ -1,23 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [hashmap_main]: type definitions -import Hashmap.Primitives - -/- [hashmap_main::hashmap::List] -/ -inductive hashmap_list_t (T : Type) := -| HashmapListCons : USize -> T -> hashmap_list_t T -> hashmap_list_t T -| HashmapListNil : hashmap_list_t T - -/- [hashmap_main::hashmap::HashMap] -/ -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) - -/- [core::num::u32::{9}::MAX] -/ -def core_num_u32_max_body : result UInt32 := - return (UInt32.ofNatCore 4294967295 (by simp)) -def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) - -/- The state type used in the state-error monad -/ -axiom state : Type \ No newline at end of file diff --git a/tests/lean/hashmap_on_disk/HashmapMain.lean b/tests/lean/hashmap_on_disk/HashmapMain.lean new file mode 100644 index 00000000..e99d3a6f --- /dev/null +++ b/tests/lean/hashmap_on_disk/HashmapMain.lean @@ -0,0 +1 @@ +def hello := "world" \ No newline at end of file diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean new file mode 100644 index 00000000..3fb121d4 --- /dev/null +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -0,0 +1,530 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: function definitions +import Base.Primitives +import HashmapMain.Types +import HashmapMain.Opaque + +/- [hashmap_main::hashmap::hash_key] -/ +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)) + then ( + let slots0 <- vec_push_back (hashmap_list_t T) slots HashmapListNil in + let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) in + hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0) + else result.ret slots + +/- [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)) + := + hashmap_hash_map_allocate_slots_loop_fwd T slots n + +/- [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] -/ +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) + := + let v <- vec_new (hashmap_list_t T) in + let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity in + let i <- USize.checked_mul capacity max_load_dividend in + let i0 <- USize.checked_div i max_load_divisor in + result.ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by intlit)) + (max_load_dividend, max_load_divisor) i0 slots) + +/- [hashmap_main::hashmap::HashMap::{0}::new] -/ +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_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 in + if i < i0 + then ( + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) in + let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i HashmapListNil + in + hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1) + else result.ret slots + +/- [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) := + let v <- hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots + in + result.ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by intlit)) + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + +/- [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 + +/- [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 := + match ls with + | HashmapListCons ckey cvalue tl => + if ckey = key + then result.ret false + else hashmap_hash_map_insert_in_list_loop_fwd T key value tl + | HashmapListNil => result.ret true + end + +/- [hashmap_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 := + 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) + := + match ls with + | HashmapListCons ckey cvalue tl => + if ckey = key + then result.ret (HashmapListCons ckey value tl) + else ( + let l <- hashmap_hash_map_insert_in_list_loop_back T key value tl in + result.ret (HashmapListCons ckey cvalue l)) + | HashmapListNil => + let l <- HashmapListNil in result.ret (HashmapListCons key value l) + end + +/- [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) + := + 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) + := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + in + let inserted <- hashmap_hash_map_insert_in_list_fwd T key value l in + if inserted + then ( + let i0 <- USize.checked_add self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by intlit)) in + let l0 <- hashmap_hash_map_insert_in_list_back T key value l in + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 in + result.ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v)) + else ( + let l0 <- hashmap_hash_map_insert_in_list_back T key value l in + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 in + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)) + +/- [core::num::u32::{9}::MAX] -/ +def core_num_u32_max_body : result UInt32 := + result.ret (UInt32.ofNatCore 4294967295 (by intlit)) +def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ +def hashmap_hash_map_move_elements_from_list_loop_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : + result (hashmap_hash_map_t T) + := + match ls with + | HashmapListCons k v tl => + let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v in + hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl + | HashmapListNil => result.ret ntable + end + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ +def hashmap_hash_map_move_elements_from_list_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : + result (hashmap_hash_map_t T) + := + hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable ls + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ +def hashmap_hash_map_move_elements_loop_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) + (i : USize) : + result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) + := + let i0 <- vec_len (hashmap_list_t T) slots in + if i < i0 + then ( + let l <- vec_index_mut_fwd (hashmap_list_t T) slots i in + let ls <- mem_replace_fwd (hashmap_list_t T) l HashmapListNil in + let ntable0 <- + hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls in + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) in + let l0 <- mem_replace_back (hashmap_list_t T) l HashmapListNil in + let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i l0 in + hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1) + else result.ret (ntable, slots) + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ +def hashmap_hash_map_move_elements_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) + (i : USize) : + result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) + := + hashmap_hash_map_move_elements_loop_fwd_back T ntable slots i + +/- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ +def hashmap_hash_map_try_resize_fwd_back + (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := + let max_usize <- scalar_cast U32 Usize core_num_u32_max_c in + let capacity <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by intlit)) in + let (i, i0) <- self.hashmap_hash_map_max_load_factor in + let i1 <- USize.checked_div n1 i in + if capacity <= i1 + then ( + let i2 <- USize.checked_mul capacity (USize.ofNatCore 2 (by intlit)) in + let ntable <- hashmap_hash_map_new_with_capacity_fwd T i2 i i0 in + let (ntable0, _) <- + hashmap_hash_map_move_elements_fwd_back T ntable + self.hashmap_hash_map_slots (USize.ofNatCore 0 (by intlit)) in + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) + ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots)) + else + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) + self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) + +/- [hashmap_main::hashmap::HashMap::{0}::insert] -/ +def hashmap_hash_map_insert_fwd_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) : + result (hashmap_hash_map_t T) + := + let self0 <- hashmap_hash_map_insert_no_resize_fwd_back T self key value in + let i <- hashmap_hash_map_len_fwd T self0 in + if i > self0.hashmap_hash_map_max_load + then hashmap_hash_map_try_resize_fwd_back T self0 + else result.ret self0 + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ +def hashmap_hash_map_contains_key_in_list_loop_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := + match ls with + | HashmapListCons ckey t tl => + if ckey = key + then result.ret true + else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl + | HashmapListNil => result.ret false + end + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ +def hashmap_hash_map_contains_key_in_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := + hashmap_hash_map_contains_key_in_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ +def hashmap_hash_map_contains_key_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result Bool := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in + hashmap_hash_map_contains_key_in_list_fwd T key l + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ +def hashmap_hash_map_get_in_list_loop_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := + match ls with + | HashmapListCons ckey cvalue tl => + if ckey = key + then result.ret cvalue + else hashmap_hash_map_get_in_list_loop_fwd T key tl + | HashmapListNil => result.fail panic + end + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ +def hashmap_hash_map_get_in_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := + hashmap_hash_map_get_in_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::get] -/ +def hashmap_hash_map_get_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in + hashmap_hash_map_get_in_list_fwd T key l + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_loop_fwd + (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := + match ls with + | HashmapListCons ckey cvalue tl => + if ckey = key + then result.ret cvalue + else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key + | HashmapListNil => result.fail panic + end + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_fwd + (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := + hashmap_hash_map_get_mut_in_list_loop_fwd T ls key + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_loop_back + (T : Type) (ls : hashmap_list_t T) (key : USize) (ret : T) : + result (hashmap_list_t T) + := + match ls with + | HashmapListCons ckey cvalue tl => + if ckey = key + then result.ret (HashmapListCons ckey ret tl) + else ( + let l <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret in + result.ret (HashmapListCons ckey cvalue l)) + | HashmapListNil => result.fail panic + end + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_back + (T : Type) (ls : hashmap_list_t T) (key : USize) (ret : T) : + result (hashmap_list_t T) + := + hashmap_hash_map_get_mut_in_list_loop_back T ls key ret + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ +def hashmap_hash_map_get_mut_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + in + hashmap_hash_map_get_mut_in_list_fwd T l key + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ +def hashmap_hash_map_get_mut_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) (ret : T) : + result (hashmap_hash_map_t T) + := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + in + let l0 <- hashmap_hash_map_get_mut_in_list_back T l key ret in + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + l0 in + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_loop_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result (option T) := + match ls with + | HashmapListCons ckey t tl => + if ckey = key + then + let mv_ls <- + mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl) + HashmapListNil in + match mv_ls with + | HashmapListCons i cvalue tl0 => result.ret (@some cvalue) + | HashmapListNil => result.fail panic + end + else hashmap_hash_map_remove_from_list_loop_fwd T key tl + | HashmapListNil => result.ret @none + end + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result (option T) := + hashmap_hash_map_remove_from_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_loop_back + (T : Type) (key : USize) (ls : hashmap_list_t T) : + result (hashmap_list_t T) + := + match ls with + | HashmapListCons ckey t tl => + if ckey = key + then + let mv_ls <- + mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl) + HashmapListNil in + match mv_ls with + | HashmapListCons i cvalue tl0 => result.ret tl0 + | HashmapListNil => result.fail panic + end + else ( + let l <- hashmap_hash_map_remove_from_list_loop_back T key tl in + result.ret (HashmapListCons ckey t l)) + | HashmapListNil => result.ret HashmapListNil + end + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_back + (T : Type) (key : USize) (ls : hashmap_list_t T) : + result (hashmap_list_t T) + := + hashmap_hash_map_remove_from_list_loop_back T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ +def hashmap_hash_map_remove_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result (option T) := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + in + let x <- hashmap_hash_map_remove_from_list_fwd T key l in + match x with + | @none => result.ret @none + | @some x0 => + let _ <- USize.checked_sub self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by intlit)) in + result.ret (@some x0) + end + +/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ +def hashmap_hash_map_remove_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : + result (hashmap_hash_map_t T) + := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + in + let x <- hashmap_hash_map_remove_from_list_fwd T key l in + match x with + | @none => + let l0 <- hashmap_hash_map_remove_from_list_back T key l in + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 in + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + | @some x0 => + let i0 <- USize.checked_sub self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by intlit)) in + let l0 <- hashmap_hash_map_remove_from_list_back T key l in + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 in + result.ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) + end + +/- [hashmap_main::hashmap::test1] -/ +def hashmap_test1_fwd : result Unit := + let hm <- hashmap_hash_map_new_fwd UInt64 in + let hm0 <- + hashmap_hash_map_insert_fwd_back UInt64 hm (USize.ofNatCore 0 (by intlit)) + (UInt64.ofNatCore 42 (by intlit)) in + let hm1 <- + hashmap_hash_map_insert_fwd_back UInt64 hm0 + (USize.ofNatCore 128 (by intlit)) (UInt64.ofNatCore 18 (by intlit)) in + let hm2 <- + hashmap_hash_map_insert_fwd_back UInt64 hm1 + (USize.ofNatCore 1024 (by intlit)) (UInt64.ofNatCore 138 (by intlit)) in + let hm3 <- + hashmap_hash_map_insert_fwd_back UInt64 hm2 + (USize.ofNatCore 1056 (by intlit)) (UInt64.ofNatCore 256 (by intlit)) in + let i <- + hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by intlit)) in + if not (i = (UInt64.ofNatCore 18 (by intlit))) + then result.fail panic + else ( + let hm4 <- + hashmap_hash_map_get_mut_back UInt64 hm3 + (USize.ofNatCore 1024 (by intlit)) (UInt64.ofNatCore 56 (by intlit)) in + let i0 <- + hashmap_hash_map_get_fwd UInt64 hm4 (USize.ofNatCore 1024 (by intlit)) in + if not (i0 = (UInt64.ofNatCore 56 (by intlit))) + then result.fail panic + else ( + let x <- + hashmap_hash_map_remove_fwd UInt64 hm4 + (USize.ofNatCore 1024 (by intlit)) in + match x with + | @none => result.fail panic + | @some x0 => + if not (x0 = (UInt64.ofNatCore 56 (by intlit))) + then result.fail panic + else ( + let hm5 <- + hashmap_hash_map_remove_back UInt64 hm4 + (USize.ofNatCore 1024 (by intlit)) in + let i1 <- + hashmap_hash_map_get_fwd UInt64 hm5 (USize.ofNatCore 0 (by intlit)) + in + if not (i1 = (UInt64.ofNatCore 42 (by intlit))) + then result.fail panic + else ( + let i2 <- + hashmap_hash_map_get_fwd UInt64 hm5 + (USize.ofNatCore 128 (by intlit)) in + if not (i2 = (UInt64.ofNatCore 18 (by intlit))) + then result.fail panic + else ( + let i3 <- + hashmap_hash_map_get_fwd UInt64 hm5 + (USize.ofNatCore 1056 (by intlit)) in + if not (i3 = (UInt64.ofNatCore 256 (by intlit))) + then result.fail panic + else result.ret ()))) + end)) + +/- Unit test for [hashmap_main::hashmap::test1] -/ +#assert (hashmap_test1_fwd = result.ret ()) + +/- [hashmap_main::insert_on_disk] -/ +def insert_on_disk_fwd + (key : USize) (value : UInt64) (st : state) : result (state × Unit) := + let (st0, hm) <- hashmap_utils_deserialize_fwd st in + let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value in + let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 in + result.ret (st1, ()) + +/- [hashmap_main::main] -/ +def main_fwd : result Unit := result.ret () + +/- Unit test for [hashmap_main::main] -/ +#assert (main_fwd = result.ret ()) + diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean new file mode 100644 index 00000000..87b10c59 --- /dev/null +++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean @@ -0,0 +1,13 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: opaque function definitions +import Base.Primitives +import HashmapMain.Types + +/- [hashmap_main::hashmap_utils::deserialize] -/ +axiom hashmap_utils_deserialize_fwd + : state -> result (state × (hashmap_hash_map_t UInt64)) + +/- [hashmap_main::hashmap_utils::serialize] -/ +axiom hashmap_utils_serialize_fwd + : 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 new file mode 100644 index 00000000..1b8f8954 --- /dev/null +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -0,0 +1,26 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: type definitions +import Base.Primitives + +/- [hashmap_main::hashmap::List] -/ +inductive hashmap_list_t (T : Type) := +| HashmapListCons : USize -> T -> hashmap_list_t T -> hashmap_list_t T +| HashmapListNil : hashmap_list_t T + +/- [hashmap_main::hashmap::HashMap] -/ +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) + + +/- [core::num::u32::{9}::MAX] -/ +def core_num_u32_max_body : result UInt32 := + result.ret (UInt32.ofNatCore 4294967295 (by intlit)) +def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) + +/- The state type used in the state-error monad -/ +axiom state : Type + diff --git a/tests/lean/hashmap_on_disk/Main.lean b/tests/lean/hashmap_on_disk/Main.lean index 7bde1315..9fe6cf4a 100644 --- a/tests/lean/hashmap_on_disk/Main.lean +++ b/tests/lean/hashmap_on_disk/Main.lean @@ -1,5 +1,5 @@ -import «Hashmap» -import Hashmap.Primitives +import «HashmapMain» +import Base.Primitives def main : IO Unit := IO.println s!"Hello, {hello}!" diff --git a/tests/lean/hashmap_on_disk/lakefile.lean b/tests/lean/hashmap_on_disk/lakefile.lean index d2a31ffe..5b9adebb 100644 --- a/tests/lean/hashmap_on_disk/lakefile.lean +++ b/tests/lean/hashmap_on_disk/lakefile.lean @@ -5,7 +5,11 @@ package «hashmap» { -- add package configuration options here } -lean_lib «Hashmap» { +lean_lib «HashmapMain» { + -- add library configuration options here +} + +lean_lib «Base» { -- add library configuration options here } -- cgit v1.2.3