diff options
45 files changed, 446 insertions, 396 deletions
@@ -9,9 +9,9 @@ Wall in Pompei, digital image from Michael Lahanis. </figcaption> </div></p> -# Aeneas +# Aeneas [Ae-ne-as] -Aeneas is a verification toolchain for Rust programs. It relies on a translation from Rusts's MIR +Aeneas (pronunced [Ae-ne-as]) is a verification toolchain for Rust programs. It relies on a translation from Rusts's MIR internal language to a pure lamdba calculus. It is intended to be used in combination with [Charon](https://github.com/AeneasVerif/charon), which compiles Rust programs to an intermediate representation called LLBC. It currently has backends for [F\*](https://www.fstar-lang.org), diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index ba75f580..6130528c 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -237,7 +237,7 @@ module IdSet = Collections.MakeSet (IdOrderedType) *) type names_map = { id_to_name : string IdMap.t; - name_to_id : id StringMap.t; + name_to_id : (id * Meta.meta option) StringMap.t; (** The name to id map is used to look for name clashes, and generate nice debugging messages: if there is a name clash, it is useful to know precisely which identifiers are mapped to the same name... @@ -253,42 +253,53 @@ let empty_names_map : names_map = } (** Small helper to report name collision *) -let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id) +let report_name_collision (id_to_string : id -> string) + ((id1, meta1) : id * Meta.meta option) (id2 : id) (meta2 : Meta.meta option) (name : string) : unit = - let id1 = "\n- " ^ id_to_string id1 in - let id2 = "\n- " ^ id_to_string id2 in + let meta_to_string (meta : Meta.meta option) = + match meta with + | None -> "" + | Some meta -> "\n " ^ Errors.meta_to_string meta.span + in + let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in + let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in let err = "Name clash detected: the following identifiers are bound to the same name \ \"" ^ name ^ "\":" ^ id1 ^ id2 ^ "\nYou may want to rename some of your definitions, or report an issue." in - (* If we fail hard on errors, raise an exception *) + (* Register the error. + + We don't link this error to any meta information because we already put + the span information about the two problematic definitions in the error + message above. *) save_error __FILE__ __LINE__ None err -let names_map_get_id_from_name (name : string) (nm : names_map) : id option = +let names_map_get_id_from_name (name : string) (nm : names_map) : + (id * Meta.meta option) option = StringMap.find_opt name nm.name_to_id let names_map_check_collision (id_to_string : id -> string) (id : id) - (name : string) (nm : names_map) : unit = + (meta : Meta.meta option) (name : string) (nm : names_map) : unit = match names_map_get_id_from_name name nm with | None -> () (* Ok *) | Some clash -> (* There is a clash: print a nice debugging message for the user *) - report_name_collision id_to_string clash id name + report_name_collision id_to_string clash id meta name (** Insert bindings in a names map without checking for collisions *) -let names_map_add_unchecked (id : id) (name : string) (nm : names_map) : - names_map = +let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string) + (nm : names_map) : names_map = (* Insert *) let id_to_name = IdMap.add id name nm.id_to_name in - let name_to_id = StringMap.add name id nm.name_to_id in + let name_to_id = StringMap.add name (id, meta) nm.name_to_id in let names_set = StringSet.add name nm.names_set in { id_to_name; name_to_id; names_set } -let names_map_add (id_to_string : id -> string) (id : id) (name : string) - (nm : names_map) : names_map = +let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option) + (name : string) (nm : names_map) : names_map = (* Check if there is a clash *) - names_map_check_collision id_to_string id name nm; + names_map_check_collision id_to_string id meta name nm; (* Sanity check *) (if StringSet.mem name nm.names_set then let err = @@ -296,9 +307,9 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string) ^ ":\nThe chosen name is already in the names set: " ^ name in (* If we fail hard on errors, raise an exception *) - save_error __FILE__ __LINE__ None err); + save_error __FILE__ __LINE__ meta err); (* Insert *) - names_map_add_unchecked id name nm + names_map_add_unchecked (id, meta) 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 @@ -384,8 +395,8 @@ let allow_collisions (id : id) : bool = (** The [id_to_string] function to print nice debugging messages if there are collisions *) -let names_maps_add (id_to_string : id -> string) (id : id) (name : string) - (nm : names_maps) : names_maps = +let names_maps_add (id_to_string : id -> string) (id : id) + (meta : Meta.meta option) (name : string) (nm : names_maps) : names_maps = (* We do not use the same name map if we allow/disallow collisions. We notably use it for field names: some backends like Lean can use the type information to disambiguate field projections. @@ -400,7 +411,7 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string) *) if allow_collisions id then ( (* Check with the ids which are considered to be strict on collisions *) - names_map_check_collision id_to_string id name nm.strict_names_map; + names_map_check_collision id_to_string id meta name nm.strict_names_map; { nm with unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map; @@ -415,10 +426,10 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string) *) let strict_names_map = if strict_collisions id then - names_map_add id_to_string id name nm.strict_names_map + names_map_add id_to_string (id, meta) name nm.strict_names_map else nm.strict_names_map in - let names_map = names_map_add id_to_string id name nm.names_map in + let names_map = names_map_add id_to_string (id, meta) name nm.names_map in { nm with strict_names_map; names_map } (** The [id_to_string] function to print nice debugging messages if there are @@ -468,20 +479,21 @@ type names_map_init = { let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty) (name : string) (nm : names_maps) : names_maps = - names_maps_add id_to_string (TypeId (TAssumed id)) name nm + names_maps_add id_to_string (TypeId (TAssumed id)) None name nm let names_maps_add_assumed_struct (id_to_string : id -> string) (id : assumed_ty) (name : string) (nm : names_maps) : names_maps = - names_maps_add id_to_string (StructId (TAssumed id)) name nm + names_maps_add id_to_string (StructId (TAssumed id)) None name nm let names_maps_add_assumed_variant (id_to_string : id -> string) (id : assumed_ty) (variant_id : VariantId.id) (name : string) (nm : names_maps) : names_maps = - names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) name nm + names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) None name nm -let names_maps_add_function (id_to_string : id -> string) (fid : fun_id) - (name : string) (nm : names_maps) : names_maps = - names_maps_add id_to_string (FunId fid) name nm +let names_maps_add_function (id_to_string : id -> string) + ((fid, meta) : fun_id * meta option) (name : string) (nm : names_maps) : + names_maps = + names_maps_add id_to_string (FunId fid) meta name nm let bool_name () = if !backend = Lean then "Bool" else "bool" let char_name () = if !backend = Lean then "Char" else "char" @@ -659,7 +671,9 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in - let names_maps = names_maps_add id_to_string id name ctx.names_maps in + let names_maps = + names_maps_add id_to_string id (Some meta) name ctx.names_maps + in { ctx with names_maps } let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string @@ -1125,7 +1139,7 @@ let initialize_names_maps () : names_maps = (* There is duplication in the keywords so we don't check the collisions while registering them (what is important is that there are no collisions between keywords and user-defined identifiers) *) - names_map_add_unchecked UnknownId name nm) + names_map_add_unchecked (UnknownId, None) name nm) strict_names_map keywords in let nm = { names_map; unsafe_names_map; strict_names_map } in @@ -1155,9 +1169,12 @@ let initialize_names_maps () : names_maps = in let assumed_functions = List.map - (fun (fid, name) -> (FromLlbc (Pure.FunId (FAssumed fid), None), name)) + (fun (fid, name) -> + ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name)) init.assumed_llbc_functions - @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions + @ List.map + (fun (fid, name) -> ((Pure fid, None), name)) + init.assumed_pure_functions in let nm = List.fold_left @@ -1662,9 +1679,11 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx) in (* If there is a basename, we use it *) match basename with - | Some basename -> + | Some basename -> ( (* This should be a no-op *) - to_snake_case basename + match !Config.backend with + | Lean -> basename + | FStar | Coq | HOL4 -> to_snake_case basename) | None -> ( (* No basename: we use the first letter of the type *) match ty with diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 87f0b5f7..1bef43b4 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -75,10 +75,15 @@ let inputs_info_is_wf (info : inputs_info) : bool = let fun_sig_info_is_wf (info : fun_sig_info) : bool = inputs_info_is_wf info.fwd_info +let opt_dest_arrow_ty (ty : ty) : (ty * ty) option = + match ty with TArrow (arg_ty, ret_ty) -> Some (arg_ty, ret_ty) | _ -> None + +let is_arrow_ty (ty : ty) : bool = Option.is_some (opt_dest_arrow_ty ty) + let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty = - match ty with - | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty) - | _ -> craise __FILE__ __LINE__ meta "Not an arrow type" + match opt_dest_arrow_ty ty with + | Some (arg_ty, ret_ty) -> (arg_ty, ret_ty) + | None -> craise __FILE__ __LINE__ meta "Not an arrow type" let compute_literal_type (cv : literal) : literal_type = match cv with diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 53ab1c08..f036cc37 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1499,9 +1499,27 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) let back_vars = List.map (fun (name, ty) -> - match ty with None -> None | Some ty -> Some (name, ty)) + match ty with + | None -> None + | Some ty -> + (* If the type is not an arrow type, don't use the name "back" + (it is a backward function with no inputs, that is to say a + value) *) + let name = if is_arrow_ty ty then name else None in + Some (name, ty)) back_vars in + (* If there is one backward function or less, we use the name "back" + (there is no point in using the lifetime name, and it makes the + code generation more stable) *) + let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in + let back_vars = + if num_back_vars = 1 then + List.map + (Option.map (fun (name, ty) -> (Option.map (fun _ -> "back") name, ty))) + back_vars + else back_vars + in fresh_opt_vars back_vars ctx (** IMPORTANT: do not use this one directly, but rather {!symbolic_value_to_texpression} *) @@ -2244,15 +2262,14 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (fun ty -> match ty with | None -> None - | Some (back_sg, ty) -> - (* We insert a name for the variable only if the function - can fail: if it can fail, it means the call returns a backward - function. Otherwise, it directly returns the value given - back by the backward function, which means we shouldn't - give it a name like "back..." (it doesn't make sense) *) + | Some (_back_sg, ty) -> + (* We insert a name for the variable only if the type + is an arrow type. If it is not, it means the backward + function is degenerate (it takes no inputs) so it is + not a function anymore but a value: it doesn't make + sense to use a name like "back...". *) let name = - if back_sg.effect_info.can_fail then Some back_fun_name - else None + if is_arrow_ty ty then Some back_fun_name else None in Some (name, ty)) back_tys) diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index c2cca26d..9256b149 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -240,11 +240,11 @@ Fixpoint betree_Node_lookup_first_message_for_key else ( p <- betree_Node_lookup_first_message_for_key n1 key next_msgs; let (l, lookup_first_message_for_key_back) := p in - let back_'a := + let back := fun (ret : betree_List_t (u64 * betree_Message_t)) => next_msgs1 <- lookup_first_message_for_key_back ret; Return (Betree_List_Cons (i, m) next_msgs1) in - Return (l, back_'a)) + Return (l, back)) | Betree_List_Nil => Return (Betree_List_Nil, Return) end end @@ -440,11 +440,11 @@ Fixpoint betree_Node_lookup_first_message_after_key then ( p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs; let (l, lookup_first_message_after_key_back) := p1 in - let back_'a := + let back := fun (ret : betree_List_t (u64 * betree_Message_t)) => next_msgs1 <- lookup_first_message_after_key_back ret; Return (Betree_List_Cons (k, m) next_msgs1) in - Return (l, back_'a)) + Return (l, back)) else Return (Betree_List_Cons (k, m) next_msgs, Return) | Betree_List_Nil => Return (Betree_List_Nil, Return) end @@ -550,11 +550,11 @@ Fixpoint betree_Node_lookup_mut_in_bindings else ( p <- betree_Node_lookup_mut_in_bindings n1 key tl; let (l, lookup_mut_in_bindings_back) := p in - let back_'a := + let back := fun (ret : betree_List_t (u64 * u64)) => tl1 <- lookup_mut_in_bindings_back ret; Return (Betree_List_Cons (i, i1) tl1) in - Return (l, back_'a)) + Return (l, back)) | Betree_List_Nil => Return (Betree_List_Nil, Return) end end diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v index a9969448..1367bac2 100644 --- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v +++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v @@ -38,7 +38,8 @@ Axiom betree_utils_store_leaf_node . (** [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 + Name pattern: core::option::{core::option::Option<@T>}::unwrap *) Axiom core_option_Option_unwrap : forall(T : Type), option T -> state -> result (state * T) . diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index d5a6e535..abec8e88 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -13,8 +13,8 @@ Module Demo. Definition choose (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) := if b - then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a) - else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a) + then let back := fun (ret : T) => Return (ret, y) in Return (x, back) + else let back := fun (ret : T) => Return (x, ret) in Return (y, back) . (** [demo::mul2_add1]: @@ -79,16 +79,16 @@ Fixpoint list_nth_mut | CList_CCons x tl => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in - Return (x, back_'a) + let back := fun (ret : T) => Return (CList_CCons ret tl) in + Return (x, back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut T n1 tl i1; let (t, list_nth_mut_back) := p in - let back_'a := + let back := fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (CList_CCons x tl1) in - Return (t, back_'a)) + Return (t, back)) | CList_CNil => Fail_ Failure end end @@ -107,15 +107,15 @@ Fixpoint list_nth_mut1_loop | CList_CCons x tl => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in - Return (x, back_'a) + let back := fun (ret : T) => Return (CList_CCons ret tl) in + Return (x, back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut1_loop T n1 tl i1; - let (t, back_'a) := p in - let back_'a1 := - fun (ret : T) => tl1 <- back_'a ret; Return (CList_CCons x tl1) in - Return (t, back_'a1)) + let (t, back) := p in + let back1 := + fun (ret : T) => tl1 <- back ret; Return (CList_CCons x tl1) in + Return (t, back1)) | CList_CNil => Fail_ Failure end end @@ -155,10 +155,10 @@ Fixpoint list_tail | CList_CCons t tl => p <- list_tail T n1 tl; let (c, list_tail_back) := p in - let back_'a := + let back := fun (ret : CList_t T) => tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in - Return (c, back_'a) + Return (c, back) | CList_CNil => Return (CList_CNil, Return) end end diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index d709a8d5..c0cde78d 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -94,13 +94,13 @@ Fixpoint hashMap_clear_loop Source: 'src/hashmap.rs', lines 80:4-80:27 *) Definition hashMap_clear (T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) := - back <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize; + hm <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize; Return {| hashMap_num_entries := 0%usize; hashMap_max_load_factor := self.(hashMap_max_load_factor); hashMap_max_load := self.(hashMap_max_load); - hashMap_slots := back + hashMap_slots := hm |} . @@ -125,8 +125,8 @@ Fixpoint hashMap_insert_in_list_loop then Return (false, List_Cons ckey value tl) else ( p <- hashMap_insert_in_list_loop T n1 key value tl; - let (b, back) := p in - Return (b, List_Cons ckey cvalue back)) + let (b, tl1) := p in + Return (b, List_Cons ckey cvalue tl1)) | List_Nil => Return (true, List_Cons key value List_Nil) end end @@ -376,15 +376,15 @@ Fixpoint hashMap_get_mut_in_list_loop | List_Cons ckey cvalue tl => if ckey s= key then - let back_'a := fun (ret : T) => Return (List_Cons ckey ret tl) in - Return (cvalue, back_'a) + let back := fun (ret : T) => Return (List_Cons ckey ret tl) in + Return (cvalue, back) else ( p <- hashMap_get_mut_in_list_loop T n1 tl key; - let (t, back_'a) := p in - let back_'a1 := - fun (ret : T) => - tl1 <- back_'a ret; Return (List_Cons ckey cvalue tl1) in - Return (t, back_'a1)) + let (t, back) := p in + let back1 := + fun (ret : T) => tl1 <- back ret; Return (List_Cons ckey cvalue tl1) + in + Return (t, back1)) | List_Nil => Fail_ Failure end end @@ -415,7 +415,7 @@ Definition hashMap_get_mut let (l, index_mut_back) := p in p1 <- hashMap_get_mut_in_list T n l key; let (t, get_mut_in_list_back) := p1 in - let back_'a := + let back := fun (ret : T) => l1 <- get_mut_in_list_back ret; v <- index_mut_back l1; @@ -426,7 +426,7 @@ Definition hashMap_get_mut hashMap_max_load := self.(hashMap_max_load); hashMap_slots := v |} in - Return (t, back_'a) + Return (t, back) . (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0: @@ -450,8 +450,8 @@ Fixpoint hashMap_remove_from_list_loop end else ( p <- hashMap_remove_from_list_loop T n1 key tl; - let (o, back) := p in - Return (o, List_Cons ckey t back)) + let (o, tl1) := p in + Return (o, List_Cons ckey t tl1)) | List_Nil => Return (None, List_Nil) end end diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 9fb3c482..8e299800 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -104,13 +104,13 @@ Definition hashmap_HashMap_clear (T : Type) (n : nat) (self : hashmap_HashMap_t T) : result (hashmap_HashMap_t T) := - back <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize; + hm <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize; Return {| hashmap_HashMap_num_entries := 0%usize; hashmap_HashMap_max_load_factor := self.(hashmap_HashMap_max_load_factor); hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); - hashmap_HashMap_slots := back + hashmap_HashMap_slots := hm |} . @@ -136,8 +136,8 @@ Fixpoint hashmap_HashMap_insert_in_list_loop then Return (false, Hashmap_List_Cons ckey value tl) else ( p <- hashmap_HashMap_insert_in_list_loop T n1 key value tl; - let (b, back) := p in - Return (b, Hashmap_List_Cons ckey cvalue back)) + let (b, tl1) := p in + Return (b, Hashmap_List_Cons ckey cvalue tl1)) | Hashmap_List_Nil => Return (true, Hashmap_List_Cons key value Hashmap_List_Nil) end @@ -398,16 +398,15 @@ Fixpoint hashmap_HashMap_get_mut_in_list_loop | Hashmap_List_Cons ckey cvalue tl => if ckey s= key then - let back_'a := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl) - in - Return (cvalue, back_'a) + let back := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl) in + Return (cvalue, back) else ( p <- hashmap_HashMap_get_mut_in_list_loop T n1 tl key; - let (t, back_'a) := p in - let back_'a1 := + let (t, back) := p in + let back1 := fun (ret : T) => - tl1 <- back_'a ret; Return (Hashmap_List_Cons ckey cvalue tl1) in - Return (t, back_'a1)) + tl1 <- back ret; Return (Hashmap_List_Cons ckey cvalue tl1) in + Return (t, back1)) | Hashmap_List_Nil => Fail_ Failure end end @@ -438,7 +437,7 @@ Definition hashmap_HashMap_get_mut let (l, index_mut_back) := p in p1 <- hashmap_HashMap_get_mut_in_list T n l key; let (t, get_mut_in_list_back) := p1 in - let back_'a := + let back := fun (ret : T) => l1 <- get_mut_in_list_back ret; v <- index_mut_back l1; @@ -450,7 +449,7 @@ Definition hashmap_HashMap_get_mut hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); hashmap_HashMap_slots := v |} in - Return (t, back_'a) + Return (t, back) . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0: @@ -475,8 +474,8 @@ Fixpoint hashmap_HashMap_remove_from_list_loop end else ( p <- hashmap_HashMap_remove_from_list_loop T n1 key tl; - let (o, back) := p in - Return (o, Hashmap_List_Cons ckey t back)) + let (o, tl1) := p in + Return (o, Hashmap_List_Cons ckey t tl1)) | Hashmap_List_Nil => Return (None, Hashmap_List_Nil) end end diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index faf91fef..a6832854 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -46,8 +46,8 @@ Definition custom_swap p <- core_mem_swap T x y st; let (st1, p1) := p in let (x1, y1) := p1 in - let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in - Return (st1, (x1, back_'a)) + let back := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in + Return (st1, (x1, back)) . (** [external::test_custom_swap]: diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v index 6773ac18..24dd2d47 100644 --- a/tests/coq/misc/External_FunsExternal_Template.v +++ b/tests/coq/misc/External_FunsExternal_Template.v @@ -12,19 +12,22 @@ Include External_Types. Module External_FunsExternal_Template. (** [core::mem::swap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 + Name pattern: core::mem::swap *) Axiom core_mem_swap : forall(T : Type), T -> T -> state -> result (state * (T * T)) . (** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 + Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *) Axiom core_num_nonzero_NonZeroU32_new : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t)) . (** [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 + Name pattern: core::option::{core::option::Option<@T>}::unwrap *) Axiom core_option_Option_unwrap : forall(T : Type), option T -> state -> result (state * T) . diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v index 7ba79d8e..7d6af202 100644 --- a/tests/coq/misc/External_TypesExternal_Template.v +++ b/tests/coq/misc/External_TypesExternal_Template.v @@ -10,7 +10,8 @@ Local Open Scope Primitives_scope. Module External_TypesExternal_Template. (** [core::num::nonzero::NonZeroU32] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 + Name pattern: core::num::nonzero::NonZeroU32 *) Axiom core_num_nonzero_NonZeroU32_t : Type. (** The state type used in the state-error monad *) diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 7c83a014..ae529cf8 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -375,18 +375,18 @@ Fixpoint list_nth_mut_loop_pair_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in - let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in - Return ((x0, x1), back_'a, back_'b) + let back'a := fun (ret : T) => Return (List_Cons ret tl0) in + let back'b := fun (ret : T) => Return (List_Cons ret tl1) in + Return ((x0, x1), back'a, back'b) else ( i1 <- u32_sub i 1%u32; t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1; - let '(p, back_'a, back_'b) := t in - let back_'a1 := - fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in - let back_'b1 := - fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in - Return (p, back_'a1, back_'b1)) + let '(p, back'a, back'b) := t in + let back'a1 := + fun (ret : T) => tl01 <- back'a ret; Return (List_Cons x0 tl01) in + let back'b1 := + fun (ret : T) => tl11 <- back'b ret; Return (List_Cons x1 tl11) in + Return (p, back'a1, back'b1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -451,21 +451,21 @@ Fixpoint list_nth_mut_loop_pair_merge_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'a := + let back := fun (ret : (T * T)) => let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1) in - Return ((x0, x1), back_'a) + Return ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1; - let (p1, back_'a) := p in - let back_'a1 := + let (p1, back) := p in + let back1 := fun (ret : (T * T)) => - p2 <- back_'a ret; + p2 <- back ret; let (tl01, tl11) := p2 in Return (List_Cons x0 tl01, List_Cons x1 tl11) in - Return (p1, back_'a1)) + Return (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -531,15 +531,15 @@ Fixpoint list_nth_mut_shared_loop_pair_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in - Return ((x0, x1), back_'a) + let back := fun (ret : T) => Return (List_Cons ret tl0) in + Return ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1; - let (p1, back_'a) := p in - let back_'a1 := - fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in - Return (p1, back_'a1)) + let (p1, back) := p in + let back1 := + fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in + Return (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -571,15 +571,15 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in - Return ((x0, x1), back_'a) + let back := fun (ret : T) => Return (List_Cons ret tl0) in + Return ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1; - let (p1, back_'a) := p in - let back_'a1 := - fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in - Return (p1, back_'a1)) + let (p1, back) := p in + let back1 := + fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in + Return (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -611,15 +611,15 @@ Fixpoint list_nth_shared_mut_loop_pair_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in - Return ((x0, x1), back_'b) + let back := fun (ret : T) => Return (List_Cons ret tl1) in + Return ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1; - let (p1, back_'b) := p in - let back_'b1 := - fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in - Return (p1, back_'b1)) + let (p1, back) := p in + let back1 := + fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in + Return (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -651,15 +651,15 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (List_Cons ret tl1) in - Return ((x0, x1), back_'a) + let back := fun (ret : T) => Return (List_Cons ret tl1) in + Return ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1; - let (p1, back_'a) := p in - let back_'a1 := - fun (ret : T) => tl11 <- back_'a ret; Return (List_Cons x1 tl11) in - Return (p1, back_'a1)) + let (p1, back) := p in + let back1 := + fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in + Return (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 76dc4cf6..d4035104 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -321,8 +321,8 @@ Check (test_split_list )%return. Definition choose (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) := if b - then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a) - else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a) + then let back := fun (ret : T) => Return (ret, y) in Return (x, back) + else let back := fun (ret : T) => Return (x, ret) in Return (y, back) . (** [no_nested_borrows::choose_test]: @@ -399,16 +399,16 @@ Fixpoint list_nth_mut | List_Cons x tl => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (List_Cons ret tl) in - Return (x, back_'a) + let back := fun (ret : T) => Return (List_Cons ret tl) in + Return (x, back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut T tl i1; let (t, list_nth_mut_back) := p in - let back_'a := + let back := fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1) in - Return (t, back_'a)) + Return (t, back)) | List_Nil => Fail_ Failure end . diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index ad77fa2a..77276223 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -27,8 +27,8 @@ Check (test_incr )%return. Definition choose (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) := if b - then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a) - else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a) + then let back := fun (ret : T) => Return (ret, y) in Return (x, back) + else let back := fun (ret : T) => Return (x, ret) in Return (y, back) . (** [paper::test_choose]: @@ -70,16 +70,16 @@ Fixpoint list_nth_mut | List_Cons x tl => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (List_Cons ret tl) in - Return (x, back_'a) + let back := fun (ret : T) => Return (List_Cons ret tl) in + Return (x, back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut T tl i1; let (t, list_nth_mut_back) := p in - let back_'a := + let back := fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1) in - Return (t, back_'a)) + Return (t, back)) | List_Nil => Fail_ Failure end . diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v index 8f403a8e..dfa09328 100644 --- a/tests/coq/misc/PoloniusList.v +++ b/tests/coq/misc/PoloniusList.v @@ -31,10 +31,10 @@ Fixpoint get_list_at_x else ( p <- get_list_at_x tl x; let (l, get_list_at_x_back) := p in - let back_'a := + let back := fun (ret : List_t u32) => tl1 <- get_list_at_x_back ret; Return (List_Cons hd tl1) in - Return (l, back_'a)) + Return (l, back)) | List_Nil => Return (List_Nil, Return) end . diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v index a861c114..0e942c7d 100644 --- a/tests/coq/traits/Traits.v +++ b/tests/coq/traits/Traits.v @@ -671,7 +671,8 @@ Arguments foo_x { _ _ }. Arguments foo_y { _ _ }. (** [core::result::Result] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 + Name pattern: core::result::Result *) Inductive core_result_Result_t (T E : Type) := | Core_result_Result_Ok : T -> core_result_Result_t T E | Core_result_Result_Err : E -> core_result_Result_t T E diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 2469f98c..129e6f7e 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -195,11 +195,11 @@ let rec betree_Node_lookup_first_message_for_key else let* (l, lookup_first_message_for_key_back) = betree_Node_lookup_first_message_for_key key next_msgs in - let back_'a = + let back = fun ret -> let* next_msgs1 = lookup_first_message_for_key_back ret in Return (Betree_List_Cons (i, m) next_msgs1) in - Return (l, back_'a) + Return (l, back) | Betree_List_Nil -> Return (Betree_List_Nil, Return) end @@ -352,11 +352,11 @@ let rec betree_Node_lookup_first_message_after_key then let* (l, lookup_first_message_after_key_back) = betree_Node_lookup_first_message_after_key key next_msgs in - let back_'a = + let back = fun ret -> let* next_msgs1 = lookup_first_message_after_key_back ret in Return (Betree_List_Cons (k, m) next_msgs1) in - Return (l, back_'a) + Return (l, back) else Return (Betree_List_Cons (k, m) next_msgs, Return) | Betree_List_Nil -> Return (Betree_List_Nil, Return) end @@ -453,11 +453,11 @@ let rec betree_Node_lookup_mut_in_bindings else let* (l, lookup_mut_in_bindings_back) = betree_Node_lookup_mut_in_bindings key tl in - let back_'a = + let back = fun ret -> let* tl1 = lookup_mut_in_bindings_back ret in Return (Betree_List_Cons (i, i1) tl1) in - Return (l, back_'a) + Return (l, back) | Betree_List_Nil -> Return (Betree_List_Nil, Return) end diff --git a/tests/fstar/betree/BetreeMain.FunsExternal.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti index de9b96fd..3aad9390 100644 --- a/tests/fstar/betree/BetreeMain.FunsExternal.fsti +++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti @@ -29,7 +29,8 @@ val betree_utils_store_leaf_node : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit) (** [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 + Name pattern: core::option::{core::option::Option<@T>}::unwrap *) val core_option_Option_unwrap (t : Type0) : option t -> state -> result (state & t) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 2469f98c..129e6f7e 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -195,11 +195,11 @@ let rec betree_Node_lookup_first_message_for_key else let* (l, lookup_first_message_for_key_back) = betree_Node_lookup_first_message_for_key key next_msgs in - let back_'a = + let back = fun ret -> let* next_msgs1 = lookup_first_message_for_key_back ret in Return (Betree_List_Cons (i, m) next_msgs1) in - Return (l, back_'a) + Return (l, back) | Betree_List_Nil -> Return (Betree_List_Nil, Return) end @@ -352,11 +352,11 @@ let rec betree_Node_lookup_first_message_after_key then let* (l, lookup_first_message_after_key_back) = betree_Node_lookup_first_message_after_key key next_msgs in - let back_'a = + let back = fun ret -> let* next_msgs1 = lookup_first_message_after_key_back ret in Return (Betree_List_Cons (k, m) next_msgs1) in - Return (l, back_'a) + Return (l, back) else Return (Betree_List_Cons (k, m) next_msgs, Return) | Betree_List_Nil -> Return (Betree_List_Nil, Return) end @@ -453,11 +453,11 @@ let rec betree_Node_lookup_mut_in_bindings else let* (l, lookup_mut_in_bindings_back) = betree_Node_lookup_mut_in_bindings key tl in - let back_'a = + let back = fun ret -> let* tl1 = lookup_mut_in_bindings_back ret in Return (Betree_List_Cons (i, i1) tl1) in - Return (l, back_'a) + Return (l, back) | Betree_List_Nil -> Return (Betree_List_Nil, Return) end diff --git a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti index de9b96fd..3aad9390 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti +++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti @@ -29,7 +29,8 @@ val betree_utils_store_leaf_node : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit) (** [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 + Name pattern: core::option::{core::option::Option<@T>}::unwrap *) val core_option_Option_unwrap (t : Type0) : option t -> state -> result (state & t) diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst index d93bc847..9c59ab9b 100644 --- a/tests/fstar/demo/Demo.fst +++ b/tests/fstar/demo/Demo.fst @@ -10,8 +10,8 @@ open Primitives let choose (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) = if b - then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a) - else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a) + then let back = fun ret -> Return (ret, y) in Return (x, back) + else let back = fun ret -> Return (x, ret) in Return (y, back) (** [demo::mul2_add1]: Source: 'src/demo.rs', lines 13:0-13:31 *) @@ -66,15 +66,14 @@ let rec list_nth_mut | CList_CCons x tl -> if i = 0 then - let back_'a = fun ret -> Return (CList_CCons ret tl) in - Return (x, back_'a) + let back = fun ret -> Return (CList_CCons ret tl) in Return (x, back) else let* i1 = u32_sub i 1 in let* (x1, list_nth_mut_back) = list_nth_mut t n1 tl i1 in - let back_'a = + let back = fun ret -> let* tl1 = list_nth_mut_back ret in Return (CList_CCons x tl1) in - Return (x1, back_'a) + Return (x1, back) | CList_CNil -> Fail Failure end @@ -92,14 +91,13 @@ let rec list_nth_mut1_loop | CList_CCons x tl -> if i = 0 then - let back_'a = fun ret -> Return (CList_CCons ret tl) in - Return (x, back_'a) + let back = fun ret -> Return (CList_CCons ret tl) in Return (x, back) else let* i1 = u32_sub i 1 in - let* (x1, back_'a) = list_nth_mut1_loop t n1 tl i1 in - let back_'a1 = - fun ret -> let* tl1 = back_'a ret in Return (CList_CCons x tl1) in - Return (x1, back_'a1) + let* (x1, back) = list_nth_mut1_loop t n1 tl i1 in + let back1 = + fun ret -> let* tl1 = back ret in Return (CList_CCons x tl1) in + Return (x1, back1) | CList_CNil -> Fail Failure end @@ -135,10 +133,10 @@ let rec list_tail begin match l with | CList_CCons x tl -> let* (c, list_tail_back) = list_tail t n1 tl in - let back_'a = + let back = fun ret -> let* tl1 = list_tail_back ret in Return (CList_CCons x tl1) in - Return (c, back_'a) + Return (c, back) | CList_CNil -> Return (CList_CNil, Return) end diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index fba711f1..d897933a 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -79,8 +79,8 @@ let rec hashMap_clear_loop (** [hashmap::{hashmap::HashMap<T>}::clear]: Source: 'src/hashmap.rs', lines 80:4-80:27 *) let hashMap_clear (t : Type0) (self : hashMap_t t) : result (hashMap_t t) = - let* back = hashMap_clear_loop t self.slots 0 in - Return { self with num_entries = 0; slots = back } + let* hm = hashMap_clear_loop t self.slots 0 in + Return { self with num_entries = 0; slots = hm } (** [hashmap::{hashmap::HashMap<T>}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 *) @@ -99,8 +99,8 @@ let rec hashMap_insert_in_list_loop if ckey = key then Return (false, List_Cons ckey value tl) else - let* (b, back) = hashMap_insert_in_list_loop t key value tl in - Return (b, List_Cons ckey cvalue back) + let* (b, tl1) = hashMap_insert_in_list_loop t key value tl in + Return (b, List_Cons ckey cvalue tl1) | List_Nil -> Return (true, List_Cons key value List_Nil) end @@ -287,14 +287,13 @@ let rec hashMap_get_mut_in_list_loop | List_Cons ckey cvalue tl -> if ckey = key then - let back_'a = fun ret -> Return (List_Cons ckey ret tl) in - Return (cvalue, back_'a) + let back = fun ret -> Return (List_Cons ckey ret tl) in + Return (cvalue, back) else - let* (x, back_'a) = hashMap_get_mut_in_list_loop t tl key in - let back_'a1 = - fun ret -> let* tl1 = back_'a ret in Return (List_Cons ckey cvalue tl1) - in - Return (x, back_'a1) + let* (x, back) = hashMap_get_mut_in_list_loop t tl key in + let back1 = + fun ret -> let* tl1 = back ret in Return (List_Cons ckey cvalue tl1) in + Return (x, back1) | List_Nil -> Fail Failure end @@ -320,12 +319,12 @@ let hashMap_get_mut (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots hash_mod in let* (x, get_mut_in_list_back) = hashMap_get_mut_in_list t l key in - let back_'a = + let back = fun ret -> let* l1 = get_mut_in_list_back ret in let* v = index_mut_back l1 in Return { self with slots = v } in - Return (x, back_'a) + Return (x, back) (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0: Source: 'src/hashmap.rs', lines 265:4-291:5 *) @@ -345,8 +344,8 @@ let rec hashMap_remove_from_list_loop | List_Nil -> Fail Failure end else - let* (o, back) = hashMap_remove_from_list_loop t key tl in - Return (o, List_Cons ckey x back) + let* (o, tl1) = hashMap_remove_from_list_loop t key tl in + Return (o, List_Cons ckey x tl1) | List_Nil -> Return (None, List_Nil) end diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 97f4151f..e0005c81 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -84,8 +84,8 @@ let rec hashmap_HashMap_clear_loop Source: 'src/hashmap.rs', lines 80:4-80:27 *) let hashmap_HashMap_clear (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) = - let* back = hashmap_HashMap_clear_loop t self.slots 0 in - Return { self with num_entries = 0; slots = back } + let* hm = hashmap_HashMap_clear_loop t self.slots 0 in + Return { self with num_entries = 0; slots = hm } (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 *) @@ -105,8 +105,8 @@ let rec hashmap_HashMap_insert_in_list_loop if ckey = key then Return (false, Hashmap_List_Cons ckey value tl) else - let* (b, back) = hashmap_HashMap_insert_in_list_loop t key value tl in - Return (b, Hashmap_List_Cons ckey cvalue back) + let* (b, tl1) = hashmap_HashMap_insert_in_list_loop t key value tl in + Return (b, Hashmap_List_Cons ckey cvalue tl1) | Hashmap_List_Nil -> Return (true, Hashmap_List_Cons key value Hashmap_List_Nil) end @@ -305,15 +305,14 @@ let rec hashmap_HashMap_get_mut_in_list_loop | Hashmap_List_Cons ckey cvalue tl -> if ckey = key then - let back_'a = fun ret -> Return (Hashmap_List_Cons ckey ret tl) in - Return (cvalue, back_'a) + let back = fun ret -> Return (Hashmap_List_Cons ckey ret tl) in + Return (cvalue, back) else - let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t tl key in - let back_'a1 = + let* (x, back) = hashmap_HashMap_get_mut_in_list_loop t tl key in + let back1 = fun ret -> - let* tl1 = back_'a ret in Return (Hashmap_List_Cons ckey cvalue tl1) - in - Return (x, back_'a1) + let* tl1 = back ret in Return (Hashmap_List_Cons ckey cvalue tl1) in + Return (x, back1) | Hashmap_List_Nil -> Fail Failure end @@ -339,12 +338,12 @@ let hashmap_HashMap_get_mut (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) self.slots hash_mod in let* (x, get_mut_in_list_back) = hashmap_HashMap_get_mut_in_list t l key in - let back_'a = + let back = fun ret -> let* l1 = get_mut_in_list_back ret in let* v = index_mut_back l1 in Return { self with slots = v } in - Return (x, back_'a) + Return (x, back) (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0: Source: 'src/hashmap.rs', lines 265:4-291:5 *) @@ -365,8 +364,8 @@ let rec hashmap_HashMap_remove_from_list_loop | Hashmap_List_Nil -> Fail Failure end else - let* (o, back) = hashmap_HashMap_remove_from_list_loop t key tl in - Return (o, Hashmap_List_Cons ckey x back) + let* (o, tl1) = hashmap_HashMap_remove_from_list_loop t key tl in + Return (o, Hashmap_List_Cons ckey x tl1) | Hashmap_List_Nil -> Return (None, Hashmap_List_Nil) end diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index 3ba20022..78960404 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -34,8 +34,8 @@ let custom_swap result (state & (t & (t -> state -> result (state & (t & t))))) = let* (st1, (x1, y1)) = core_mem_swap t x y st in - let back_'a = fun ret st2 -> Return (st2, (ret, y1)) in - Return (st1, (x1, back_'a)) + let back = fun ret st2 -> Return (st2, (ret, y1)) in + Return (st1, (x1, back)) (** [external::test_custom_swap]: Source: 'src/external.rs', lines 29:0-29:59 *) diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti index a412aea9..4c1c58b7 100644 --- a/tests/fstar/misc/External.FunsExternal.fsti +++ b/tests/fstar/misc/External.FunsExternal.fsti @@ -7,16 +7,19 @@ include External.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [core::mem::swap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 + Name pattern: core::mem::swap *) val core_mem_swap (t : Type0) : t -> t -> state -> result (state & (t & t)) (** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 + Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *) val core_num_nonzero_NonZeroU32_new : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t)) (** [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 + Name pattern: core::option::{core::option::Option<@T>}::unwrap *) val core_option_Option_unwrap (t : Type0) : option t -> state -> result (state & t) diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti index 4bfbe0c5..45174c7e 100644 --- a/tests/fstar/misc/External.TypesExternal.fsti +++ b/tests/fstar/misc/External.TypesExternal.fsti @@ -6,7 +6,8 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [core::num::nonzero::NonZeroU32] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 + Name pattern: core::num::nonzero::NonZeroU32 *) val core_num_nonzero_NonZeroU32_t : Type0 (** The state type used in the state-error monad *) diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 7c099da2..93683deb 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -289,18 +289,17 @@ let rec list_nth_mut_loop_pair_loop | List_Cons x1 tl1 -> if i = 0 then - let back_'a = fun ret -> Return (List_Cons ret tl0) in - let back_'b = fun ret -> Return (List_Cons ret tl1) in - Return ((x0, x1), back_'a, back_'b) + let back'a = fun ret -> Return (List_Cons ret tl0) in + let back'b = fun ret -> Return (List_Cons ret tl1) in + Return ((x0, x1), back'a, back'b) else let* i1 = u32_sub i 1 in - let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1 - in - let back_'a1 = - fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in - let back_'b1 = - fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in - Return (p, back_'a1, back_'b1) + let* (p, back'a, back'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1 in + let back'a1 = + fun ret -> let* tl01 = back'a ret in Return (List_Cons x0 tl01) in + let back'b1 = + fun ret -> let* tl11 = back'b ret in Return (List_Cons x1 tl11) in + Return (p, back'a1, back'b1) | List_Nil -> Fail Failure end | List_Nil -> Fail Failure @@ -352,18 +351,18 @@ let rec list_nth_mut_loop_pair_merge_loop | List_Cons x1 tl1 -> if i = 0 then - let back_'a = + let back = fun ret -> let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1) in - Return ((x0, x1), back_'a) + Return ((x0, x1), back) else let* i1 = u32_sub i 1 in - let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in - let back_'a1 = + let* (p, back) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in + let back1 = fun ret -> - let* (tl01, tl11) = back_'a ret in + let* (tl01, tl11) = back ret in Return (List_Cons x0 tl01, List_Cons x1 tl11) in - Return (p, back_'a1) + Return (p, back1) | List_Nil -> Fail Failure end | List_Nil -> Fail Failure @@ -417,14 +416,14 @@ let rec list_nth_mut_shared_loop_pair_loop | List_Cons x1 tl1 -> if i = 0 then - let back_'a = fun ret -> Return (List_Cons ret tl0) in - Return ((x0, x1), back_'a) + let back = fun ret -> Return (List_Cons ret tl0) in + Return ((x0, x1), back) else let* i1 = u32_sub i 1 in - let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in - let back_'a1 = - fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in - Return (p, back_'a1) + let* (p, back) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in + let back1 = + fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in + Return (p, back1) | List_Nil -> Fail Failure end | List_Nil -> Fail Failure @@ -451,15 +450,15 @@ let rec list_nth_mut_shared_loop_pair_merge_loop | List_Cons x1 tl1 -> if i = 0 then - let back_'a = fun ret -> Return (List_Cons ret tl0) in - Return ((x0, x1), back_'a) + let back = fun ret -> Return (List_Cons ret tl0) in + Return ((x0, x1), back) else let* i1 = u32_sub i 1 in - let* (p, back_'a) = - list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1 in - let back_'a1 = - fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in - Return (p, back_'a1) + let* (p, back) = list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1 + in + let back1 = + fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in + Return (p, back1) | List_Nil -> Fail Failure end | List_Nil -> Fail Failure @@ -486,14 +485,14 @@ let rec list_nth_shared_mut_loop_pair_loop | List_Cons x1 tl1 -> if i = 0 then - let back_'b = fun ret -> Return (List_Cons ret tl1) in - Return ((x0, x1), back_'b) + let back = fun ret -> Return (List_Cons ret tl1) in + Return ((x0, x1), back) else let* i1 = u32_sub i 1 in - let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in - let back_'b1 = - fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in - Return (p, back_'b1) + let* (p, back) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in + let back1 = + fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in + Return (p, back1) | List_Nil -> Fail Failure end | List_Nil -> Fail Failure @@ -520,15 +519,15 @@ let rec list_nth_shared_mut_loop_pair_merge_loop | List_Cons x1 tl1 -> if i = 0 then - let back_'a = fun ret -> Return (List_Cons ret tl1) in - Return ((x0, x1), back_'a) + let back = fun ret -> Return (List_Cons ret tl1) in + Return ((x0, x1), back) else let* i1 = u32_sub i 1 in - let* (p, back_'a) = - list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1 in - let back_'a1 = - fun ret -> let* tl11 = back_'a ret in Return (List_Cons x1 tl11) in - Return (p, back_'a1) + let* (p, back) = list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1 + in + let back1 = + fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in + Return (p, back1) | List_Nil -> Fail Failure end | List_Nil -> Fail Failure diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index db63eb0d..1a93beaa 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -291,8 +291,8 @@ let _ = assert_norm (test_split_list = Return ()) let choose (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) = if b - then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a) - else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a) + then let back = fun ret -> Return (ret, y) in Return (x, back) + else let back = fun ret -> Return (x, ret) in Return (y, back) (** [no_nested_borrows::choose_test]: Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 *) @@ -355,15 +355,14 @@ let rec list_nth_mut begin match l with | List_Cons x tl -> if i = 0 - then - let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a) + then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back) else let* i1 = u32_sub i 1 in let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in - let back_'a = + let back = fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1) in - Return (x1, back_'a) + Return (x1, back) | List_Nil -> Fail Failure end diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst index ddc5e7a8..c2f47ad1 100644 --- a/tests/fstar/misc/Paper.fst +++ b/tests/fstar/misc/Paper.fst @@ -23,8 +23,8 @@ let _ = assert_norm (test_incr = Return ()) let choose (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) = if b - then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a) - else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a) + then let back = fun ret -> Return (ret, y) in Return (x, back) + else let back = fun ret -> Return (x, ret) in Return (y, back) (** [paper::test_choose]: Source: 'src/paper.rs', lines 23:0-23:20 *) @@ -57,15 +57,14 @@ let rec list_nth_mut begin match l with | List_Cons x tl -> if i = 0 - then - let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a) + then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back) else let* i1 = u32_sub i 1 in let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in - let back_'a = + let back = fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1) in - Return (x1, back_'a) + Return (x1, back) | List_Nil -> Fail Failure end diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst index b477802b..4203247e 100644 --- a/tests/fstar/misc/PoloniusList.fst +++ b/tests/fstar/misc/PoloniusList.fst @@ -23,10 +23,10 @@ let rec get_list_at_x then Return (List_Cons hd tl, Return) else let* (l, get_list_at_x_back) = get_list_at_x tl x in - let back_'a = + let back = fun ret -> let* tl1 = get_list_at_x_back ret in Return (List_Cons hd tl1) in - Return (l, back_'a) + Return (l, back) | List_Nil -> Return (List_Nil, Return) end diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst index fba564a5..199d49bf 100644 --- a/tests/fstar/traits/Traits.fst +++ b/tests/fstar/traits/Traits.fst @@ -503,7 +503,8 @@ let use_wrapper_len (t : Type0) (traitInst : trait_t t) : result usize = type foo_t (t u : Type0) = { x : t; y : u; } (** [core::result::Result] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *) + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 + Name pattern: core::result::Result *) type core_result_Result_t (t e : Type0) = | Core_result_Result_Ok : t -> core_result_Result_t t e | Core_result_Result_Err : e -> core_result_Result_t t e diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index ca9b48da..2fbcd6a4 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -192,12 +192,12 @@ divergent def betree.Node.lookup_first_message_for_key do let (l, lookup_first_message_for_key_back) ← betree.Node.lookup_first_message_for_key key next_msgs - let back_'a := + let back := fun ret => do let next_msgs1 ← lookup_first_message_for_key_back ret Result.ret (betree.List.Cons (i, m) next_msgs1) - Result.ret (l, back_'a) + Result.ret (l, back) | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret) /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: @@ -364,12 +364,12 @@ divergent def betree.Node.lookup_first_message_after_key do let (l, lookup_first_message_after_key_back) ← betree.Node.lookup_first_message_after_key key next_msgs - let back_'a := + let back := fun ret => do let next_msgs1 ← lookup_first_message_after_key_back ret Result.ret (betree.List.Cons (k, m) next_msgs1) - Result.ret (l, back_'a) + Result.ret (l, back) else Result.ret (betree.List.Cons (k, m) next_msgs, Result.ret) | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret) @@ -468,12 +468,12 @@ divergent def betree.Node.lookup_mut_in_bindings do let (l, lookup_mut_in_bindings_back) ← betree.Node.lookup_mut_in_bindings key tl - let back_'a := + let back := fun ret => do let tl1 ← lookup_mut_in_bindings_back ret Result.ret (betree.List.Cons (i, i1) tl1) - Result.ret (l, back_'a) + Result.ret (l, back) | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret) /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean index eaa4b6c2..0b3e4ef4 100644 --- a/tests/lean/BetreeMain/FunsExternal_Template.lean +++ b/tests/lean/BetreeMain/FunsExternal_Template.lean @@ -29,7 +29,8 @@ axiom betree_utils.store_leaf_node : U64 → betree.List (U64 × U64) → State → Result (State × Unit) /- [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/ + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 + Name pattern: core::option::{core::option::Option<@T>}::unwrap -/ axiom core.option.Option.unwrap (T : Type) : Option T → State → Result (State × T) diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 4acc69c8..6d9fef8e 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -12,10 +12,10 @@ def choose Result (T × (T → Result (T × T))) := if b - then let back_'a := fun ret => Result.ret (ret, y) - Result.ret (x, back_'a) - else let back_'a := fun ret => Result.ret (x, ret) - Result.ret (y, back_'a) + then let back := fun ret => Result.ret (ret, y) + Result.ret (x, back) + else let back := fun ret => Result.ret (x, ret) + Result.ret (y, back) /- [demo::mul2_add1]: Source: 'src/demo.rs', lines 13:0-13:31 -/ @@ -73,18 +73,18 @@ divergent def list_nth_mut | CList.CCons x tl => if i = 0#u32 then - let back_'a := fun ret => Result.ret (CList.CCons ret tl) - Result.ret (x, back_'a) + let back := fun ret => Result.ret (CList.CCons ret tl) + Result.ret (x, back) else do let i1 ← i - 1#u32 let (t, list_nth_mut_back) ← list_nth_mut T tl i1 - let back_'a := + let back := fun ret => do let tl1 ← list_nth_mut_back ret Result.ret (CList.CCons x tl1) - Result.ret (t, back_'a) + Result.ret (t, back) | CList.CNil => Result.fail .panic /- [demo::list_nth_mut1]: loop 0: @@ -97,17 +97,17 @@ divergent def list_nth_mut1_loop | CList.CCons x tl => if i = 0#u32 then - let back_'a := fun ret => Result.ret (CList.CCons ret tl) - Result.ret (x, back_'a) + let back := fun ret => Result.ret (CList.CCons ret tl) + Result.ret (x, back) else do let i1 ← i - 1#u32 - let (t, back_'a) ← list_nth_mut1_loop T tl i1 - let back_'a1 := + let (t, back) ← list_nth_mut1_loop T tl i1 + let back1 := fun ret => do - let tl1 ← back_'a ret + let tl1 ← back ret Result.ret (CList.CCons x tl1) - Result.ret (t, back_'a1) + Result.ret (t, back1) | CList.CNil => Result.fail .panic /- [demo::list_nth_mut1]: @@ -138,12 +138,12 @@ divergent def list_tail | CList.CCons t tl => do let (c, list_tail_back) ← list_tail T tl - let back_'a := + let back := fun ret => do let tl1 ← list_tail_back ret Result.ret (CList.CCons t tl1) - Result.ret (c, back_'a) + Result.ret (c, back) | CList.CNil => Result.ret (CList.CNil, Result.ret) /- Trait declaration: [demo::Counter] diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 8b645037..cfb2cb3c 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -39,8 +39,8 @@ def custom_swap := do let (st1, (x1, y1)) ← core.mem.swap T x y st - let back_'a := fun ret st2 => Result.ret (st2, (ret, y1)) - Result.ret (st1, (x1, back_'a)) + let back := fun ret st2 => Result.ret (st2, (ret, y1)) + Result.ret (st1, (x1, back)) /- [external::test_custom_swap]: Source: 'src/external.rs', lines 29:0-29:59 -/ diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index 7e237369..38151dc9 100644 --- a/tests/lean/External/FunsExternal_Template.lean +++ b/tests/lean/External/FunsExternal_Template.lean @@ -7,17 +7,20 @@ open Primitives open external /- [core::mem::swap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/ + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 + Name pattern: core::mem::swap -/ axiom core.mem.swap (T : Type) : T → T → State → Result (State × (T × T)) /- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 -/ + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 + Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new -/ axiom core.num.nonzero.NonZeroU32.new : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32)) /- [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/ + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 + Name pattern: core::option::{core::option::Option<@T>}::unwrap -/ axiom core.option.Option.unwrap (T : Type) : Option T → State → Result (State × T) diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean index 85fef236..84245531 100644 --- a/tests/lean/External/TypesExternal_Template.lean +++ b/tests/lean/External/TypesExternal_Template.lean @@ -5,7 +5,8 @@ import Base open Primitives /- [core::num::nonzero::NonZeroU32] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/ + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 + Name pattern: core::num::nonzero::NonZeroU32 -/ axiom core.num.nonzero.NonZeroU32 : Type /- The state type used in the state-error monad -/ diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 1c95f7c9..363d751a 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -79,8 +79,8 @@ divergent def HashMap.clear_loop Source: 'src/hashmap.rs', lines 80:4-80:27 -/ def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do - let back ← HashMap.clear_loop T self.slots 0#usize - Result.ret { self with num_entries := 0#usize, slots := back } + let hm ← HashMap.clear_loop T self.slots 0#usize + Result.ret { self with num_entries := 0#usize, slots := hm } /- [hashmap::{hashmap::HashMap<T>}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 -/ @@ -99,8 +99,8 @@ divergent def HashMap.insert_in_list_loop then Result.ret (false, List.Cons ckey value tl) else do - let (b, back) ← HashMap.insert_in_list_loop T key value tl - Result.ret (b, List.Cons ckey cvalue back) + let (b, tl1) ← HashMap.insert_in_list_loop T key value tl + Result.ret (b, List.Cons ckey cvalue tl1) | List.Nil => Result.ret (true, List.Cons key value List.Nil) /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: @@ -287,17 +287,17 @@ divergent def HashMap.get_mut_in_list_loop | List.Cons ckey cvalue tl => if ckey = key then - let back_'a := fun ret => Result.ret (List.Cons ckey ret tl) - Result.ret (cvalue, back_'a) + let back := fun ret => Result.ret (List.Cons ckey ret tl) + Result.ret (cvalue, back) else do - let (t, back_'a) ← HashMap.get_mut_in_list_loop T tl key - let back_'a1 := + let (t, back) ← HashMap.get_mut_in_list_loop T tl key + let back1 := fun ret => do - let tl1 ← back_'a ret + let tl1 ← back ret Result.ret (List.Cons ckey cvalue tl1) - Result.ret (t, back_'a1) + Result.ret (t, back1) | List.Nil => Result.fail .panic /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: @@ -322,13 +322,13 @@ def HashMap.get_mut alloc.vec.Vec.index_mut (List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod let (t, get_mut_in_list_back) ← HashMap.get_mut_in_list T l key - let back_'a := + let back := fun ret => do let l1 ← get_mut_in_list_back ret let v ← index_mut_back l1 Result.ret { self with slots := v } - Result.ret (t, back_'a) + Result.ret (t, back) /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0: Source: 'src/hashmap.rs', lines 265:4-291:5 -/ @@ -345,8 +345,8 @@ divergent def HashMap.remove_from_list_loop | List.Nil => Result.fail .panic else do - let (o, back) ← HashMap.remove_from_list_loop T key tl - Result.ret (o, List.Cons ckey t back) + let (o, tl1) ← HashMap.remove_from_list_loop T key tl + Result.ret (o, List.Cons ckey t tl1) | List.Nil => Result.ret (none, List.Nil) /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index 6a6934b8..6fac6940 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -83,8 +83,8 @@ divergent def hashmap.HashMap.clear_loop def hashmap.HashMap.clear (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do - let back ← hashmap.HashMap.clear_loop T self.slots 0#usize - Result.ret { self with num_entries := 0#usize, slots := back } + let hm ← hashmap.HashMap.clear_loop T self.slots 0#usize + Result.ret { self with num_entries := 0#usize, slots := hm } /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 -/ @@ -103,8 +103,8 @@ divergent def hashmap.HashMap.insert_in_list_loop then Result.ret (false, hashmap.List.Cons ckey value tl) else do - let (b, back) ← hashmap.HashMap.insert_in_list_loop T key value tl - Result.ret (b, hashmap.List.Cons ckey cvalue back) + let (b, tl1) ← hashmap.HashMap.insert_in_list_loop T key value tl + Result.ret (b, hashmap.List.Cons ckey cvalue tl1) | hashmap.List.Nil => Result.ret (true, hashmap.List.Cons key value hashmap.List.Nil) @@ -302,17 +302,17 @@ divergent def hashmap.HashMap.get_mut_in_list_loop | hashmap.List.Cons ckey cvalue tl => if ckey = key then - let back_'a := fun ret => Result.ret (hashmap.List.Cons ckey ret tl) - Result.ret (cvalue, back_'a) + let back := fun ret => Result.ret (hashmap.List.Cons ckey ret tl) + Result.ret (cvalue, back) else do - let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T tl key - let back_'a1 := + let (t, back) ← hashmap.HashMap.get_mut_in_list_loop T tl key + let back1 := fun ret => do - let tl1 ← back_'a ret + let tl1 ← back ret Result.ret (hashmap.List.Cons ckey cvalue tl1) - Result.ret (t, back_'a1) + Result.ret (t, back1) | hashmap.List.Nil => Result.fail .panic /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: @@ -338,13 +338,13 @@ def hashmap.HashMap.get_mut (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots hash_mod let (t, get_mut_in_list_back) ← hashmap.HashMap.get_mut_in_list T l key - let back_'a := + let back := fun ret => do let l1 ← get_mut_in_list_back ret let v ← index_mut_back l1 Result.ret { self with slots := v } - Result.ret (t, back_'a) + Result.ret (t, back) /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0: Source: 'src/hashmap.rs', lines 265:4-291:5 -/ @@ -364,8 +364,8 @@ divergent def hashmap.HashMap.remove_from_list_loop | hashmap.List.Nil => Result.fail .panic else do - let (o, back) ← hashmap.HashMap.remove_from_list_loop T key tl - Result.ret (o, hashmap.List.Cons ckey t back) + let (o, tl1) ← hashmap.HashMap.remove_from_list_loop T key tl + Result.ret (o, hashmap.List.Cons ckey t tl1) | hashmap.List.Nil => Result.ret (none, hashmap.List.Nil) /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 0f3d77c2..27434db8 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -295,22 +295,22 @@ divergent def list_nth_mut_loop_pair_loop | List.Cons x1 tl1 => if i = 0#u32 then - let back_'a := fun ret => Result.ret (List.Cons ret tl0) - let back_'b := fun ret => Result.ret (List.Cons ret tl1) - Result.ret ((x0, x1), back_'a, back_'b) + let back'a := fun ret => Result.ret (List.Cons ret tl0) + let back'b := fun ret => Result.ret (List.Cons ret tl1) + Result.ret ((x0, x1), back'a, back'b) else do let i1 ← i - 1#u32 - let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1 - let back_'a1 := + let (p, back'a, back'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1 + let back'a1 := fun ret => do - let tl01 ← back_'a ret + let tl01 ← back'a ret Result.ret (List.Cons x0 tl01) - let back_'b1 := + let back'b1 := fun ret => do - let tl11 ← back_'b ret + let tl11 ← back'b ret Result.ret (List.Cons x1 tl11) - Result.ret (p, back_'a1, back_'b1) + Result.ret (p, back'a1, back'b1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic @@ -356,21 +356,21 @@ divergent def list_nth_mut_loop_pair_merge_loop | List.Cons x1 tl1 => if i = 0#u32 then - let back_'a := + let back := fun ret => let (t, t1) := ret Result.ret (List.Cons t tl0, List.Cons t1 tl1) - Result.ret ((x0, x1), back_'a) + Result.ret ((x0, x1), back) else do let i1 ← i - 1#u32 - let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1 - let back_'a1 := + let (p, back) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1 + let back1 := fun ret => do - let (tl01, tl11) ← back_'a ret + let (tl01, tl11) ← back ret Result.ret (List.Cons x0 tl01, List.Cons x1 tl11) - Result.ret (p, back_'a1) + Result.ret (p, back1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic @@ -417,17 +417,17 @@ divergent def list_nth_mut_shared_loop_pair_loop | List.Cons x1 tl1 => if i = 0#u32 then - let back_'a := fun ret => Result.ret (List.Cons ret tl0) - Result.ret ((x0, x1), back_'a) + let back := fun ret => Result.ret (List.Cons ret tl0) + Result.ret ((x0, x1), back) else do let i1 ← i - 1#u32 - let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1 - let back_'a1 := + let (p, back) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1 + let back1 := fun ret => do - let tl01 ← back_'a ret + let tl01 ← back ret Result.ret (List.Cons x0 tl01) - Result.ret (p, back_'a1) + Result.ret (p, back1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic @@ -451,18 +451,17 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop | List.Cons x1 tl1 => if i = 0#u32 then - let back_'a := fun ret => Result.ret (List.Cons ret tl0) - Result.ret ((x0, x1), back_'a) + let back := fun ret => Result.ret (List.Cons ret tl0) + Result.ret ((x0, x1), back) else do let i1 ← i - 1#u32 - let (p, back_'a) ← - list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1 - let back_'a1 := + let (p, back) ← list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1 + let back1 := fun ret => do - let tl01 ← back_'a ret + let tl01 ← back ret Result.ret (List.Cons x0 tl01) - Result.ret (p, back_'a1) + Result.ret (p, back1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic @@ -486,17 +485,17 @@ divergent def list_nth_shared_mut_loop_pair_loop | List.Cons x1 tl1 => if i = 0#u32 then - let back_'b := fun ret => Result.ret (List.Cons ret tl1) - Result.ret ((x0, x1), back_'b) + let back := fun ret => Result.ret (List.Cons ret tl1) + Result.ret ((x0, x1), back) else do let i1 ← i - 1#u32 - let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1 - let back_'b1 := + let (p, back) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1 + let back1 := fun ret => do - let tl11 ← back_'b ret + let tl11 ← back ret Result.ret (List.Cons x1 tl11) - Result.ret (p, back_'b1) + Result.ret (p, back1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic @@ -520,18 +519,17 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop | List.Cons x1 tl1 => if i = 0#u32 then - let back_'a := fun ret => Result.ret (List.Cons ret tl1) - Result.ret ((x0, x1), back_'a) + let back := fun ret => Result.ret (List.Cons ret tl1) + Result.ret ((x0, x1), back) else do let i1 ← i - 1#u32 - let (p, back_'a) ← - list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1 - let back_'a1 := + let (p, back) ← list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1 + let back1 := fun ret => do - let tl11 ← back_'a ret + let tl11 ← back ret Result.ret (List.Cons x1 tl11) - Result.ret (p, back_'a1) + Result.ret (p, back1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 5f9ec0f2..b90f6aef 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -331,10 +331,10 @@ def choose Result (T × (T → Result (T × T))) := if b - then let back_'a := fun ret => Result.ret (ret, y) - Result.ret (x, back_'a) - else let back_'a := fun ret => Result.ret (x, ret) - Result.ret (y, back_'a) + then let back := fun ret => Result.ret (ret, y) + Result.ret (x, back) + else let back := fun ret => Result.ret (x, ret) + Result.ret (y, back) /- [no_nested_borrows::choose_test]: Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 -/ @@ -406,18 +406,18 @@ divergent def list_nth_mut | List.Cons x tl => if i = 0#u32 then - let back_'a := fun ret => Result.ret (List.Cons ret tl) - Result.ret (x, back_'a) + let back := fun ret => Result.ret (List.Cons ret tl) + Result.ret (x, back) else do let i1 ← i - 1#u32 let (t, list_nth_mut_back) ← list_nth_mut T tl i1 - let back_'a := + let back := fun ret => do let tl1 ← list_nth_mut_back ret Result.ret (List.Cons x tl1) - Result.ret (t, back_'a) + Result.ret (t, back) | List.Nil => Result.fail .panic /- [no_nested_borrows::list_rev_aux]: diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 924ff36c..5b00aa83 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -29,10 +29,10 @@ def choose Result (T × (T → Result (T × T))) := if b - then let back_'a := fun ret => Result.ret (ret, y) - Result.ret (x, back_'a) - else let back_'a := fun ret => Result.ret (x, ret) - Result.ret (y, back_'a) + then let back := fun ret => Result.ret (ret, y) + Result.ret (x, back) + else let back := fun ret => Result.ret (x, ret) + Result.ret (y, back) /- [paper::test_choose]: Source: 'src/paper.rs', lines 23:0-23:20 -/ @@ -68,18 +68,18 @@ divergent def list_nth_mut | List.Cons x tl => if i = 0#u32 then - let back_'a := fun ret => Result.ret (List.Cons ret tl) - Result.ret (x, back_'a) + let back := fun ret => Result.ret (List.Cons ret tl) + Result.ret (x, back) else do let i1 ← i - 1#u32 let (t, list_nth_mut_back) ← list_nth_mut T tl i1 - let back_'a := + let back := fun ret => do let tl1 ← list_nth_mut_back ret Result.ret (List.Cons x tl1) - Result.ret (t, back_'a) + Result.ret (t, back) | List.Nil => Result.fail .panic /- [paper::sum]: diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean index 59c557a0..c657237f 100644 --- a/tests/lean/PoloniusList.lean +++ b/tests/lean/PoloniusList.lean @@ -24,12 +24,12 @@ divergent def get_list_at_x else do let (l, get_list_at_x_back) ← get_list_at_x tl x - let back_'a := + let back := fun ret => do let tl1 ← get_list_at_x_back ret Result.ret (List.Cons hd tl1) - Result.ret (l, back_'a) + Result.ret (l, back) | List.Nil => Result.ret (List.Nil, Result.ret) end polonius_list diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index acddd1a9..766b109d 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -512,7 +512,8 @@ structure Foo (T U : Type) where y : U /- [core::result::Result] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 -/ + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 + Name pattern: core::result::Result -/ inductive core.result.Result (T E : Type) := | Ok : T → core.result.Result T E | Err : E → core.result.Result T E |