diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Config.ml | 11 | ||||
| -rw-r--r-- | compiler/Driver.ml | 4 | ||||
| -rw-r--r-- | compiler/Extract.ml | 13 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 68 | ||||
| -rw-r--r-- | compiler/Translate.ml | 1 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 106 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/Types.lean | 16 | ||||
| -rw-r--r-- | tests/lean/Constants.lean | 15 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Funs.lean | 90 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Types.lean | 8 | ||||
| -rw-r--r-- | tests/lean/HashmapMain/Funs.lean | 116 | ||||
| -rw-r--r-- | tests/lean/HashmapMain/Types.lean | 8 | ||||
| -rw-r--r-- | tests/lean/NoNestedBorrows.lean | 43 |
13 files changed, 232 insertions, 267 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index f58ba89b..0475899c 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -304,3 +304,14 @@ let filter_useless_functions = ref true called opaque_defs, of type OpaqueDefs. *) let wrap_opaque_in_sig = ref false + +(** Use short names for the record fields. + + Some backends can't disambiguate records when their field names have collisions. + When this happens, we use long names, by which we concatenate the record + names with the field names, and check whether there are name collisions. + + For backends which can disambiguate records (typically by using the typing + information), we use short names (i.e., the original field names). + *) +let record_fields_short_names = ref false diff --git a/compiler/Driver.ml b/compiler/Driver.ml index f935a717..166ef11b 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -163,7 +163,9 @@ let () = (* We don't support fuel for the Lean backend *) if !use_fuel then ( log#error "The Lean backend doesn't support the -use-fuel option"; - fail ()) + fail ()); + (* Lean can disambiguate the field names *) + record_fields_short_names := true | HOL4 -> (* We don't support fuel for the HOL4 backend *) if !use_fuel then ( diff --git a/compiler/Extract.ml b/compiler/Extract.ml index cacb9b96..558a981d 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -625,10 +625,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) in let field_name (def_name : name) (field_id : FieldId.id) (field_name : string option) : string = - let def_name = type_name_to_snake_case def_name ^ "_" in - match field_name with - | Some field_name -> def_name ^ field_name - | None -> def_name ^ FieldId.to_string field_id + let field_name = + match field_name with + | Some field_name -> field_name + | None -> FieldId.to_string field_id + in + if !Config.record_fields_short_names then field_name + else + let def_name = type_name_to_snake_case def_name ^ "_" in + def_name ^ field_name in let variant_name (def_name : name) (variant : string) : string = match !backend with diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index ede7af29..655bb033 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -416,7 +416,7 @@ module IdSet = Collections.MakeSet (IdOrderedType) We use it for lookups (during the translation) and to check for name clashes. - [id_to_string] is for debugging. + [id_to_name] is for debugging. *) type names_map = { id_to_name : string IdMap.t; @@ -427,7 +427,9 @@ type names_map = { *) names_set : StringSet.t; opaque_ids : IdSet.t; - (** The set of opaque definitions. + (** TODO: this is obsolete. Remove. + + The set of opaque definitions. See {!formatter.opaque_pre} for detailed explanations about why we need to know which definitions are opaque to compute names. @@ -488,6 +490,20 @@ let names_map_add_function (id_to_string : id -> string) (is_opaque : bool) (fid : fun_id) (name : string) (nm : names_map) : names_map = names_map_add id_to_string is_opaque (FunId fid) name nm +(** The unsafe names map stores mappings from identifiers to names which might + collide. For some backends and some names, it might be acceptable to have + collisions. For instance, in Lean, different records can have fields with + the same name because Lean uses the typing information to resolve the + ambiguities. + + This map complements the {!names_map}, which checks for collisions. + *) +type unsafe_names_map = { id_to_name : string IdMap.t } + +let unsafe_names_map_add (id : id) (name : string) (nm : unsafe_names_map) : + unsafe_names_map = + { id_to_name = IdMap.add id name nm.id_to_name } + (** Make a (variable) basename unique (by adding an index). We do this in an inefficient manner (by testing all indices starting from @@ -532,6 +548,11 @@ type fun_name_info = { keep_fwd : bool; num_backs : int } type extraction_ctx = { trans_ctx : trans_ctx; names_map : names_map; + (** The map for id to names, where we forbid name collisions + (ex.: we always forbid function name collisions). *) + unsafe_names_map : unsafe_names_map; + (** The map for id to names, where we allow name collisions + (ex.: we might allow record field name collisions). *) fmt : formatter; indent_incr : int; (** The indent increment we insert whenever we need to indent more *) @@ -690,23 +711,42 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id | VarId id -> "var_id: " ^ VarId.to_string id +(** We might not check for collisions for some specific ids (ex.: field names) *) +let allow_collisions (id : id) : bool = + match id with + | FieldId (_, _) -> !Config.record_fields_short_names + | _ -> false + let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = - (* The id_to_string function to print nice debugging messages if there are - * collisions *) - let id_to_string (id : id) : string = id_to_string id ctx in - let names_map = names_map_add id_to_string is_opaque id name ctx.names_map in - { ctx with names_map } + (* We do not use the same name map if we allow/disallow collisions *) + if allow_collisions id then ( + assert (not is_opaque); + { + ctx with + unsafe_names_map = unsafe_names_map_add id name ctx.unsafe_names_map; + }) + else + (* The id_to_string function to print nice debugging messages if there are + * collisions *) + let id_to_string (id : id) : string = id_to_string id ctx in + let names_map = + names_map_add id_to_string is_opaque id name ctx.names_map + in + { ctx with names_map } (** [with_opaque_pre]: if [true] and the definition is opaque, add the opaque prefix *) let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string = - match IdMap.find_opt id ctx.names_map.id_to_name with - | Some s -> - let is_opaque = IdSet.mem id ctx.names_map.opaque_ids in - if with_opaque_pre && is_opaque then ctx.fmt.opaque_pre () ^ s else s - | None -> - log#serror ("Could not find: " ^ id_to_string id ctx); - raise Not_found + (* We do not use the same name map if we allow/disallow collisions *) + if allow_collisions id then IdMap.find id ctx.unsafe_names_map.id_to_name + else + match IdMap.find_opt id ctx.names_map.id_to_name with + | Some s -> + let is_opaque = IdSet.mem id ctx.names_map.opaque_ids in + if with_opaque_pre && is_opaque then ctx.fmt.opaque_pre () ^ s else s + | None -> + log#serror ("Could not find: " ^ id_to_string id ctx); + raise Not_found let ctx_get_global (with_opaque_pre : bool) (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 444642c0..c5f7df92 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -922,6 +922,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : { ExtractBase.trans_ctx; names_map; + unsafe_names_map = { id_to_name = ExtractBase.IdMap.empty }; fmt; indent_incr = 2; use_opaque_pre = !Config.split_files; diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index 41e4349e..b0939155 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -48,23 +48,20 @@ def betree.fresh_node_id_back (counter : U64) : Result U64 := /- [betree_main::betree::NodeIdCounter::{0}::new]: forward function -/ def betree.NodeIdCounter.new : Result betree.NodeIdCounter := - Result.ret - { betree_node_id_counter_next_node_id := (U64.ofInt 0 (by intlit)) } + Result.ret { next_node_id := (U64.ofInt 0 (by intlit)) } /- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function -/ def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 := do - let _ ← self.betree_node_id_counter_next_node_id + - (U64.ofInt 1 (by intlit)) - Result.ret self.betree_node_id_counter_next_node_id + let _ ← self.next_node_id + (U64.ofInt 1 (by intlit)) + Result.ret self.next_node_id /- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 -/ def betree.NodeIdCounter.fresh_id_back (self : betree.NodeIdCounter) : Result betree.NodeIdCounter := do - let i ← self.betree_node_id_counter_next_node_id + - (U64.ofInt 1 (by intlit)) - Result.ret { betree_node_id_counter_next_node_id := i } + let i ← self.next_node_id + (U64.ofInt 1 (by intlit)) + Result.ret { next_node_id := i } /- [core::num::u64::{10}::MAX] -/ def core_num_u64_max_body : Result U64 := @@ -181,8 +178,7 @@ def betree.Leaf.split Result (State × betree.Internal) := do - let p ← - betree.List.split_at (U64 × U64) content params.betree_params_split_size + let p ← betree.List.split_at (U64 × U64) content params.split_size let (content0, content1) := p let p0 ← betree.List.hd (U64 × U64) content1 let (pivot, _) := p0 @@ -191,17 +187,9 @@ def betree.Leaf.split let id1 ← betree.NodeIdCounter.fresh_id node_id_cnt0 let (st0, _) ← betree.store_leaf_node id0 content0 st let (st1, _) ← betree.store_leaf_node id1 content1 st0 - let n := betree.Node.Leaf - { - betree_leaf_id := id0, - betree_leaf_size := params.betree_params_split_size - } - let n0 := betree.Node.Leaf - { - betree_leaf_id := id1, - betree_leaf_size := params.betree_params_split_size - } - Result.ret (st1, betree.Internal.mk self.betree_leaf_id pivot n n0) + let n := betree.Node.Leaf { id := id0, size := params.split_size } + let n0 := betree.Node.Leaf { id := id1, size := params.split_size } + Result.ret (st1, betree.Internal.mk self.id pivot n n0) /- [betree_main::betree::Leaf::{3}::split]: backward function 2 -/ def betree.Leaf.split_back @@ -210,8 +198,7 @@ def betree.Leaf.split_back Result betree.NodeIdCounter := do - let p ← - betree.List.split_at (U64 × U64) content params.betree_params_split_size + let p ← betree.List.split_at (U64 × U64) content params.split_size let (content0, content1) := p let _ ← betree.List.hd (U64 × U64) content1 let id0 ← betree.NodeIdCounter.fresh_id node_id_cnt @@ -392,7 +379,7 @@ mutual divergent def betree.Node.lookup Result.ret (st1, opt) | betree.Node.Leaf node => do - let (st0, bindings) ← betree.load_leaf_node node.betree_leaf_id st + let (st0, bindings) ← betree.load_leaf_node node.id st let opt ← betree.Node.lookup_in_bindings key bindings Result.ret (st0, opt) @@ -463,7 +450,7 @@ divergent def betree.Node.lookup_back Result.ret (betree.Node.Internal node0) | betree.Node.Leaf node => do - let (_, bindings) ← betree.load_leaf_node node.betree_leaf_id st + let (_, bindings) ← betree.load_leaf_node node.id st let _ ← betree.Node.lookup_in_bindings key bindings Result.ret (betree.Node.Leaf node) @@ -732,7 +719,7 @@ mutual divergent def betree.Node.apply_messages let (st0, content) ← betree.load_internal_node i st let content0 ← betree.Node.apply_messages_to_internal content msgs let num_msgs ← betree.List.len (U64 × betree.Message) content0 - if num_msgs >= params.betree_params_min_flush_size + if num_msgs >= params.min_flush_size then do let (st1, content1) ← @@ -750,22 +737,20 @@ mutual divergent def betree.Node.apply_messages Result.ret (st1, ()) | betree.Node.Leaf node => do - let (st0, content) ← betree.load_leaf_node node.betree_leaf_id st + let (st0, content) ← betree.load_leaf_node node.id st let content0 ← betree.Node.apply_messages_to_leaf content msgs let len ← betree.List.len (U64 × U64) content0 - let i ← (U64.ofInt 2 (by intlit)) * params.betree_params_split_size + let i ← (U64.ofInt 2 (by intlit)) * params.split_size if len >= i then do let (st1, _) ← betree.Leaf.split node content0 params node_id_cnt st0 - let (st2, _) ← - betree.store_leaf_node node.betree_leaf_id betree.List.Nil st1 + let (st2, _) ← betree.store_leaf_node node.id betree.List.Nil st1 Result.ret (st2, ()) else do - let (st1, _) ← - betree.store_leaf_node node.betree_leaf_id content0 st0 + let (st1, _) ← betree.store_leaf_node node.id content0 st0 Result.ret (st1, ()) /- [betree_main::betree::Node::{5}::apply_messages]: backward function 0 -/ @@ -782,7 +767,7 @@ divergent def betree.Node.apply_messages_back let (st0, content) ← betree.load_internal_node i st let content0 ← betree.Node.apply_messages_to_internal content msgs let num_msgs ← betree.List.len (U64 × betree.Message) content0 - if num_msgs >= params.betree_params_min_flush_size + if num_msgs >= params.min_flush_size then do let (st1, content1) ← @@ -802,25 +787,23 @@ divergent def betree.Node.apply_messages_back node_id_cnt) | betree.Node.Leaf node => do - let (st0, content) ← betree.load_leaf_node node.betree_leaf_id st + let (st0, content) ← betree.load_leaf_node node.id st let content0 ← betree.Node.apply_messages_to_leaf content msgs let len ← betree.List.len (U64 × U64) content0 - let i ← (U64.ofInt 2 (by intlit)) * params.betree_params_split_size + let i ← (U64.ofInt 2 (by intlit)) * params.split_size if len >= i then do let (st1, new_node) ← betree.Leaf.split node content0 params node_id_cnt st0 - let _ ← - betree.store_leaf_node node.betree_leaf_id betree.List.Nil st1 + let _ ← betree.store_leaf_node node.id betree.List.Nil st1 let node_id_cnt0 ← betree.Leaf.split_back node content0 params node_id_cnt st0 Result.ret (betree.Node.Internal new_node, node_id_cnt0) else do - let _ ← betree.store_leaf_node node.betree_leaf_id content0 st0 - Result.ret (betree.Node.Leaf { node with betree_leaf_size := len }, - node_id_cnt) + let _ ← betree.store_leaf_node node.id content0 st0 + Result.ret (betree.Node.Leaf { node with size := len }, node_id_cnt) /- [betree_main::betree::Internal::{4}::flush]: forward function -/ divergent def betree.Internal.flush @@ -834,7 +817,7 @@ divergent def betree.Internal.flush let p ← betree.List.partition_at_pivot betree.Message content i let (msgs_left, msgs_right) := p let len_left ← betree.List.len (U64 × betree.Message) msgs_left - if len_left >= params.betree_params_min_flush_size + if len_left >= params.min_flush_size then do let (st0, _) ← @@ -842,7 +825,7 @@ divergent def betree.Internal.flush let (_, node_id_cnt0) ← betree.Node.apply_messages_back n params node_id_cnt msgs_left st let len_right ← betree.List.len (U64 × betree.Message) msgs_right - if len_right >= params.betree_params_min_flush_size + if len_right >= params.min_flush_size then do let (st1, _) ← @@ -872,7 +855,7 @@ divergent def betree.Internal.flush_back let p ← betree.List.partition_at_pivot betree.Message content i0 let (msgs_left, msgs_right) := p let len_left ← betree.List.len (U64 × betree.Message) msgs_left - if len_left >= params.betree_params_min_flush_size + if len_left >= params.min_flush_size then do let (st0, _) ← @@ -880,7 +863,7 @@ divergent def betree.Internal.flush_back let (n1, node_id_cnt0) ← betree.Node.apply_messages_back n params node_id_cnt msgs_left st let len_right ← betree.List.len (U64 × betree.Message) msgs_right - if len_right >= params.betree_params_min_flush_size + if len_right >= params.min_flush_size then do let (n2, node_id_cnt1) ← @@ -936,18 +919,11 @@ def betree.BeTree.new let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt Result.ret (st0, { - betree_be_tree_params := - { - betree_params_min_flush_size := min_flush_size, - betree_params_split_size := split_size - }, - betree_be_tree_node_id_cnt := node_id_cnt0, - betree_be_tree_root := - (betree.Node.Leaf - { - betree_leaf_id := id, - betree_leaf_size := (U64.ofInt 0 (by intlit)) - }) + params := + { min_flush_size := min_flush_size, split_size := split_size }, + node_id_cnt := node_id_cnt0, + root := + (betree.Node.Leaf { id := id, size := (U64.ofInt 0 (by intlit)) }) }) /- [betree_main::betree::BeTree::{6}::apply]: forward function -/ @@ -957,11 +933,9 @@ def betree.BeTree.apply := do let (st0, _) ← - betree.Node.apply self.betree_be_tree_root self.betree_be_tree_params - self.betree_be_tree_node_id_cnt key msg st + betree.Node.apply self.root self.params self.node_id_cnt key msg st let _ ← - betree.Node.apply_back self.betree_be_tree_root - self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st + betree.Node.apply_back self.root self.params self.node_id_cnt key msg st Result.ret (st0, ()) /- [betree_main::betree::BeTree::{6}::apply]: backward function 0 -/ @@ -971,10 +945,8 @@ def betree.BeTree.apply_back := do let (n, nic) ← - betree.Node.apply_back self.betree_be_tree_root - self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st - Result.ret - { self with betree_be_tree_node_id_cnt := nic, betree_be_tree_root := n } + betree.Node.apply_back self.root self.params self.node_id_cnt key msg st + Result.ret { self with node_id_cnt := nic, root := n } /- [betree_main::betree::BeTree::{6}::insert]: forward function -/ def betree.BeTree.insert @@ -1033,14 +1005,14 @@ def betree.BeTree.lookup (self : betree.BeTree) (key : U64) (st : State) : Result (State × (Option U64)) := - betree.Node.lookup self.betree_be_tree_root key st + betree.Node.lookup self.root key st /- [betree_main::betree::BeTree::{6}::lookup]: backward function 0 -/ def betree.BeTree.lookup_back (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree := do - let n ← betree.Node.lookup_back self.betree_be_tree_root key st - Result.ret { self with betree_be_tree_root := n } + let n ← betree.Node.lookup_back self.root key st + Result.ret { self with root := n } /- [betree_main::main]: forward function -/ def main : Result Unit := diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean index afbdac9a..783ade64 100644 --- a/tests/lean/BetreeMain/Types.lean +++ b/tests/lean/BetreeMain/Types.lean @@ -22,8 +22,8 @@ inductive betree.Message := /- [betree_main::betree::Leaf] -/ structure betree.Leaf where - betree_leaf_id : U64 - betree_leaf_size : U64 + id : U64 + size : U64 mutual @@ -40,18 +40,18 @@ end /- [betree_main::betree::Params] -/ structure betree.Params where - betree_params_min_flush_size : U64 - betree_params_split_size : U64 + min_flush_size : U64 + split_size : U64 /- [betree_main::betree::NodeIdCounter] -/ structure betree.NodeIdCounter where - betree_node_id_counter_next_node_id : U64 + next_node_id : U64 /- [betree_main::betree::BeTree] -/ structure betree.BeTree where - betree_be_tree_params : betree.Params - betree_be_tree_node_id_cnt : betree.NodeIdCounter - betree_be_tree_root : betree.Node + params : betree.Params + node_id_cnt : betree.NodeIdCounter + root : betree.Node /- The state type used in the state-error monad -/ axiom State : Type diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index f37c9204..8f22bfba 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -35,12 +35,12 @@ def mk_pair0 (x : U32) (y : U32) : Result (U32 × U32) := /- [constants::Pair] -/ structure Pair (T1 T2 : Type) where - pair_x : T1 - pair_y : T2 + x : T1 + y : T2 /- [constants::mk_pair1]: forward function -/ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) := - Result.ret { pair_x := x, pair_y := y } + Result.ret { x := x, y := y } /- [constants::P0] -/ def p0_body : Result (U32 × U32) := @@ -59,17 +59,16 @@ def p2_c : (U32 × U32) := eval_global p2_body (by simp) /- [constants::P3] -/ def p3_body : Result (Pair U32 U32) := - Result.ret - { pair_x := (U32.ofInt 0 (by intlit)), pair_y := (U32.ofInt 1 (by intlit)) } + Result.ret { x := (U32.ofInt 0 (by intlit)), y := (U32.ofInt 1 (by intlit)) } def p3_c : Pair U32 U32 := eval_global p3_body (by simp) /- [constants::Wrap] -/ structure Wrap (T : Type) where - wrap_val : T + val : T /- [constants::Wrap::{0}::new]: forward function -/ def Wrap.new (T : Type) (val : T) : Result (Wrap T) := - Result.ret { wrap_val := val } + Result.ret { val := val } /- [constants::Y] -/ def y_body : Result (Wrap I32) := Wrap.new I32 (I32.ofInt 2 (by intlit)) @@ -77,7 +76,7 @@ def y_c : Wrap I32 := eval_global y_body (by simp) /- [constants::unwrap_y]: forward function -/ def unwrap_y : Result I32 := - Result.ret y_c.wrap_val + Result.ret y_c.val /- [constants::YVAL] -/ def yval_body : Result I32 := unwrap_y diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 34ff1379..5e11ffdd 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -38,10 +38,10 @@ def HashMap.new_with_capacity let i0 ← i / max_load_divisor Result.ret { - hash_map_num_entries := (Usize.ofInt 0 (by intlit)), - hash_map_max_load_factor := (max_load_dividend, max_load_divisor), - hash_map_max_load := i0, - hash_map_slots := slots + num_entries := (Usize.ofInt 0 (by intlit)), + max_load_factor := (max_load_dividend, max_load_divisor), + max_load := i0, + slots := slots } /- [hashmap::HashMap::{0}::new]: forward function -/ @@ -66,19 +66,13 @@ divergent def HashMap.clear_loop (there is a single backward function, and the forward function returns ()) -/ def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do - let v ← - HashMap.clear_loop T self.hash_map_slots (Usize.ofInt 0 (by intlit)) + let v ← HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit)) Result.ret - { - self - with - hash_map_num_entries := (Usize.ofInt 0 (by intlit)), - hash_map_slots := v - } + { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v } /- [hashmap::HashMap::{0}::len]: forward function -/ def HashMap.len (T : Type) (self : HashMap T) : Result Usize := - Result.ret self.hash_map_num_entries + Result.ret self.num_entries /- [hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function -/ divergent def HashMap.insert_in_list_loop @@ -122,23 +116,22 @@ def HashMap.insert_no_resize := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.slots hash_mod let inserted ← HashMap.insert_in_list T key value l if inserted then do - let i0 ← self.hash_map_num_entries + (Usize.ofInt 1 (by intlit)) + let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit)) let l0 ← HashMap.insert_in_list_back T key value l - let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 - Result.ret - { self with hash_map_num_entries := i0, hash_map_slots := v } + let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 + Result.ret { self with num_entries := i0, slots := v } else do let l0 ← HashMap.insert_in_list_back T key value l - let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 - Result.ret { self with hash_map_slots := v } + let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 + Result.ret { self with slots := v } /- [core::num::u32::{9}::MAX] -/ def core_num_u32_max_body : Result U32 := @@ -194,9 +187,9 @@ def HashMap.move_elements def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c - let capacity := Vec.len (List T) self.hash_map_slots + let capacity := Vec.len (List T) self.slots let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) - let (i, i0) := self.hash_map_max_load_factor + let (i, i0) := self.max_load_factor let i1 ← n1 / i if capacity <= i1 then @@ -204,16 +197,14 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := let i2 ← capacity * (Usize.ofInt 2 (by intlit)) let ntable ← HashMap.new_with_capacity T i2 i i0 let (ntable0, _) ← - HashMap.move_elements T ntable self.hash_map_slots - (Usize.ofInt 0 (by intlit)) + HashMap.move_elements T ntable self.slots (Usize.ofInt 0 (by intlit)) Result.ret { ntable0 with - hash_map_num_entries := self.hash_map_num_entries, - hash_map_max_load_factor := (i, i0) + num_entries := self.num_entries, max_load_factor := (i, i0) } - else Result.ret { self with hash_map_max_load_factor := (i, i0) } + else Result.ret { self with max_load_factor := (i, i0) } /- [hashmap::HashMap::{0}::insert]: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ @@ -224,7 +215,7 @@ def HashMap.insert do let self0 ← HashMap.insert_no_resize T self key value let i ← HashMap.len T self0 - if i > self0.hash_map_max_load + if i > self0.max_load then HashMap.try_resize T self0 else Result.ret self0 @@ -248,9 +239,9 @@ def HashMap.contains_key (T : Type) (self : HashMap T) (key : Usize) : Result Bool := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index (List T) self.hash_map_slots hash_mod + let l ← Vec.index (List T) self.slots hash_mod HashMap.contains_key_in_list T key l /- [hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/ @@ -271,9 +262,9 @@ def HashMap.get_in_list (T : Type) (key : Usize) (ls : List T) : Result T := def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index (List T) self.hash_map_slots hash_mod + let l ← Vec.index (List T) self.slots hash_mod HashMap.get_in_list T key l /- [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/ @@ -313,9 +304,9 @@ def HashMap.get_mut_in_list_back def HashMap.get_mut (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.slots hash_mod HashMap.get_mut_in_list T l key /- [hashmap::HashMap::{0}::get_mut]: backward function 0 -/ @@ -325,12 +316,12 @@ def HashMap.get_mut_back := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.slots hash_mod let l0 ← HashMap.get_mut_in_list_back T l key ret0 - let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 - Result.ret { self with hash_map_slots := v } + let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 + Result.ret { self with slots := v } /- [hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function -/ divergent def HashMap.remove_from_list_loop @@ -378,15 +369,15 @@ def HashMap.remove (T : Type) (self : HashMap T) (key : Usize) : Result (Option T) := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.slots hash_mod let x ← HashMap.remove_from_list T key l match x with | Option.none => Result.ret Option.none | Option.some x0 => do - let _ ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) + let _ ← self.num_entries - (Usize.ofInt 1 (by intlit)) Result.ret (Option.some x0) /- [hashmap::HashMap::{0}::remove]: backward function 0 -/ @@ -394,23 +385,22 @@ def HashMap.remove_back (T : Type) (self : HashMap T) (key : Usize) : Result (HashMap T) := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.slots hash_mod let x ← HashMap.remove_from_list T key l match x with | Option.none => do let l0 ← HashMap.remove_from_list_back T key l - let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 - Result.ret { self with hash_map_slots := v } + let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 + Result.ret { self with slots := v } | Option.some x0 => do - let i0 ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) + let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit)) let l0 ← HashMap.remove_from_list_back T key l - let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 - Result.ret - { self with hash_map_num_entries := i0, hash_map_slots := v } + let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 + Result.ret { self with num_entries := i0, slots := v } /- [hashmap::test1]: forward function -/ def test1 : Result Unit := diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean index 7530f3b9..6606cf9e 100644 --- a/tests/lean/Hashmap/Types.lean +++ b/tests/lean/Hashmap/Types.lean @@ -11,9 +11,9 @@ inductive List (T : Type) := /- [hashmap::HashMap] -/ structure HashMap (T : Type) where - hash_map_num_entries : Usize - hash_map_max_load_factor : (Usize × Usize) - hash_map_max_load : Usize - hash_map_slots : Vec (List T) + num_entries : Usize + max_load_factor : (Usize × Usize) + max_load : Usize + slots : Vec (List T) end hashmap diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index b1afcd44..e82cc9b2 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -43,11 +43,10 @@ def hashmap.HashMap.new_with_capacity let i0 ← i / max_load_divisor Result.ret { - hashmap_hash_map_num_entries := (Usize.ofInt 0 (by intlit)), - hashmap_hash_map_max_load_factor := - (max_load_dividend, max_load_divisor), - hashmap_hash_map_max_load := i0, - hashmap_hash_map_slots := slots + num_entries := (Usize.ofInt 0 (by intlit)), + max_load_factor := (max_load_dividend, max_load_divisor), + max_load := i0, + slots := slots } /- [hashmap_main::hashmap::HashMap::{0}::new]: forward function -/ @@ -77,19 +76,13 @@ def hashmap.HashMap.clear (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let v ← - hashmap.HashMap.clear_loop T self.hashmap_hash_map_slots - (Usize.ofInt 0 (by intlit)) + hashmap.HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit)) Result.ret - { - self - with - hashmap_hash_map_num_entries := (Usize.ofInt 0 (by intlit)), - hashmap_hash_map_slots := v - } + { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v } /- [hashmap_main::hashmap::HashMap::{0}::len]: forward function -/ def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize := - Result.ret self.hashmap_hash_map_num_entries + Result.ret self.num_entries /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function -/ divergent def hashmap.HashMap.insert_in_list_loop @@ -138,33 +131,22 @@ def hashmap.HashMap.insert_no_resize := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← - Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod let inserted ← hashmap.HashMap.insert_in_list T key value l if inserted then do - let i0 ← self.hashmap_hash_map_num_entries + - (Usize.ofInt 1 (by intlit)) + let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit)) let l0 ← hashmap.HashMap.insert_in_list_back T key value l - let v ← - Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots - hash_mod l0 - Result.ret - { - self - with - hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v - } + let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + Result.ret { self with num_entries := i0, slots := v } else do let l0 ← hashmap.HashMap.insert_in_list_back T key value l - let v ← - Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots - hash_mod l0 - Result.ret { self with hashmap_hash_map_slots := v } + let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + Result.ret { self with slots := v } /- [core::num::u32::{9}::MAX] -/ def core_num_u32_max_body : Result U32 := @@ -227,9 +209,9 @@ def hashmap.HashMap.try_resize (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c - let capacity := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let capacity := Vec.len (hashmap.List T) self.slots let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) - let (i, i0) := self.hashmap_hash_map_max_load_factor + let (i, i0) := self.max_load_factor let i1 ← n1 / i if capacity <= i1 then @@ -237,16 +219,15 @@ def hashmap.HashMap.try_resize let i2 ← capacity * (Usize.ofInt 2 (by intlit)) let ntable ← hashmap.HashMap.new_with_capacity T i2 i i0 let (ntable0, _) ← - hashmap.HashMap.move_elements T ntable self.hashmap_hash_map_slots + hashmap.HashMap.move_elements T ntable self.slots (Usize.ofInt 0 (by intlit)) Result.ret { ntable0 with - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := (i, i0) + num_entries := self.num_entries, max_load_factor := (i, i0) } - else Result.ret { self with hashmap_hash_map_max_load_factor := (i, i0) } + else Result.ret { self with max_load_factor := (i, i0) } /- [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ @@ -257,7 +238,7 @@ def hashmap.HashMap.insert do let self0 ← hashmap.HashMap.insert_no_resize T self key value let i ← hashmap.HashMap.len T self0 - if i > self0.hashmap_hash_map_max_load + if i > self0.max_load then hashmap.HashMap.try_resize T self0 else Result.ret self0 @@ -281,9 +262,9 @@ def hashmap.HashMap.contains_key (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index (hashmap.List T) self.slots hash_mod hashmap.HashMap.contains_key_in_list T key l /- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/ @@ -306,9 +287,9 @@ def hashmap.HashMap.get (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index (hashmap.List T) self.slots hash_mod hashmap.HashMap.get_in_list T key l /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/ @@ -353,10 +334,9 @@ def hashmap.HashMap.get_mut (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← - Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod hashmap.HashMap.get_mut_in_list T l key /- [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 -/ @@ -366,15 +346,12 @@ def hashmap.HashMap.get_mut_back := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← - Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0 - let v ← - Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod - l0 - Result.ret { self with hashmap_hash_map_slots := v } + let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + Result.ret { self with slots := v } /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function -/ divergent def hashmap.HashMap.remove_from_list_loop @@ -426,17 +403,15 @@ def hashmap.HashMap.remove (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result (Option T) := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← - Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod let x ← hashmap.HashMap.remove_from_list T key l match x with | Option.none => Result.ret Option.none | Option.some x0 => do - let _ ← self.hashmap_hash_map_num_entries - - (Usize.ofInt 1 (by intlit)) + let _ ← self.num_entries - (Usize.ofInt 1 (by intlit)) Result.ret (Option.some x0) /- [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 -/ @@ -446,33 +421,22 @@ def hashmap.HashMap.remove_back := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← - Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod let x ← hashmap.HashMap.remove_from_list T key l match x with | Option.none => do let l0 ← hashmap.HashMap.remove_from_list_back T key l - let v ← - Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots - hash_mod l0 - Result.ret { self with hashmap_hash_map_slots := v } + let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + Result.ret { self with slots := v } | Option.some x0 => do - let i0 ← self.hashmap_hash_map_num_entries - - (Usize.ofInt 1 (by intlit)) + let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit)) let l0 ← hashmap.HashMap.remove_from_list_back T key l - let v ← - Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots - hash_mod l0 - Result.ret - { - self - with - hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v - } + let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + Result.ret { self with num_entries := i0, slots := v } /- [hashmap_main::hashmap::test1]: forward function -/ def hashmap.test1 : Result Unit := diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean index ac195e3d..3b3d0d7c 100644 --- a/tests/lean/HashmapMain/Types.lean +++ b/tests/lean/HashmapMain/Types.lean @@ -11,10 +11,10 @@ inductive hashmap.List (T : Type) := /- [hashmap_main::hashmap::HashMap] -/ structure hashmap.HashMap (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) + num_entries : Usize + max_load_factor : (Usize × Usize) + max_load : Usize + slots : Vec (hashmap.List T) /- The state type used in the state-error monad -/ axiom State : Type diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index dc744a29..1c6421bb 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -6,8 +6,8 @@ namespace no_nested_borrows /- [no_nested_borrows::Pair] -/ structure Pair (T1 T2 : Type) where - pair_x : T1 - pair_y : T2 + x : T1 + y : T2 /- [no_nested_borrows::List] -/ inductive List (T : Type) := @@ -431,71 +431,52 @@ def id_mut_pair4_back'b /- [no_nested_borrows::StructWithTuple] -/ structure StructWithTuple (T1 T2 : Type) where - struct_with_tuple_p : (T1 × T2) + p : (T1 × T2) /- [no_nested_borrows::new_tuple1]: forward function -/ def new_tuple1 : Result (StructWithTuple U32 U32) := - Result.ret - { - struct_with_tuple_p := - ((U32.ofInt 1 (by intlit)), (U32.ofInt 2 (by intlit))) - } + Result.ret { p := ((U32.ofInt 1 (by intlit)), (U32.ofInt 2 (by intlit))) } /- [no_nested_borrows::new_tuple2]: forward function -/ def new_tuple2 : Result (StructWithTuple I16 I16) := - Result.ret - { - struct_with_tuple_p := - ((I16.ofInt 1 (by intlit)), (I16.ofInt 2 (by intlit))) - } + Result.ret { p := ((I16.ofInt 1 (by intlit)), (I16.ofInt 2 (by intlit))) } /- [no_nested_borrows::new_tuple3]: forward function -/ def new_tuple3 : Result (StructWithTuple U64 I64) := - Result.ret - { - struct_with_tuple_p := - ((U64.ofInt 1 (by intlit)), (I64.ofInt 2 (by intlit))) - } + Result.ret { p := ((U64.ofInt 1 (by intlit)), (I64.ofInt 2 (by intlit))) } /- [no_nested_borrows::StructWithPair] -/ structure StructWithPair (T1 T2 : Type) where - struct_with_pair_p : Pair T1 T2 + p : Pair T1 T2 /- [no_nested_borrows::new_pair1]: forward function -/ def new_pair1 : Result (StructWithPair U32 U32) := Result.ret - { - struct_with_pair_p := - { - pair_x := (U32.ofInt 1 (by intlit)), - pair_y := (U32.ofInt 2 (by intlit)) - } - } + { p := { x := (U32.ofInt 1 (by intlit)), y := (U32.ofInt 2 (by intlit)) } } /- [no_nested_borrows::test_constants]: forward function -/ def test_constants : Result Unit := do let swt ← new_tuple1 - let (i, _) := swt.struct_with_tuple_p + let (i, _) := swt.p if not (i = (U32.ofInt 1 (by intlit))) then Result.fail Error.panic else do let swt0 ← new_tuple2 - let (i0, _) := swt0.struct_with_tuple_p + let (i0, _) := swt0.p if not (i0 = (I16.ofInt 1 (by intlit))) then Result.fail Error.panic else do let swt1 ← new_tuple3 - let (i1, _) := swt1.struct_with_tuple_p + let (i1, _) := swt1.p if not (i1 = (U64.ofInt 1 (by intlit))) then Result.fail Error.panic else do let swp ← new_pair1 - if not (swp.struct_with_pair_p.pair_x = - (U32.ofInt 1 (by intlit))) + if not (swp.p.x = (U32.ofInt 1 (by intlit))) then Result.fail Error.panic else Result.ret () |