From 3151e373d64f9bce6146a44cd2d3cc64cac84cbf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 4 Sep 2023 00:59:39 +0200 Subject: Fix minor issues --- compiler/Driver.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index b646a53d..d88962db 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -17,7 +17,9 @@ let log = main_log let _ = (* Set up the logging - for now we use default values - TODO: use the * command-line arguments *) - (* By setting a level for the main_logger_handler, we filter everything *) + (* By setting a level for the main_logger_handler, we filter everything. + To have a good trace: one should switch between Info and Debug. + *) Easy_logging.Handlers.set_level main_logger_handler EL.Debug; main_log#set_level EL.Info; llbc_of_json_logger#set_level EL.Info; -- cgit v1.3.1 From 8b18c0da053e069b5a2d9fbf06f45eae2f05a029 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 7 Sep 2023 15:28:06 +0200 Subject: Map some globals like u32::MAX to standard definitions --- backends/lean/Base/Primitives/Scalar.lean | 42 ++++++++++++++++++++++++++ compiler/Driver.ml | 14 --------- compiler/Extract.ml | 8 ++++- compiler/ExtractAssumed.ml | 49 +++++++++++++++++++++++++++++++ compiler/ExtractBase.ml | 22 ++++++++++---- compiler/LlbcAstUtils.ml | 20 +++++++++++++ compiler/Translate.ml | 36 +++++++++++------------ compiler/dune | 1 + 8 files changed, 154 insertions(+), 38 deletions(-) create mode 100644 compiler/ExtractAssumed.ml (limited to 'compiler/Driver.ml') diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index ffc969f3..fa5a63cd 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -230,6 +230,20 @@ def Scalar.cMax (ty : ScalarTy) : Int := | .Usize => Scalar.max .U32 | _ => Scalar.max ty +theorem Scalar.min_lt_max (ty : ScalarTy) : Scalar.min ty < Scalar.max ty := by + cases ty <;> simp [Scalar.min, Scalar.max] + . simp [Isize.min, Isize.max] + have h1 := Isize.refined_min.property + have h2 := Isize.refined_max.property + cases h1 <;> cases h2 <;> simp [*] + . simp [Usize.max] + have h := Usize.refined_max.property + cases h <;> simp [*] + +theorem Scalar.min_le_max (ty : ScalarTy) : Scalar.min ty ≤ Scalar.max ty := by + have := Scalar.min_lt_max ty + int_tac + theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at * have h := Isize.refined_min.property @@ -395,6 +409,34 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re @[reducible] def U64 := Scalar .U64 @[reducible] def U128 := Scalar .U128 +-- TODO: reducible? +@[reducible] def isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) +@[reducible] def isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) +@[reducible] def i8_min : I8 := Scalar.ofInt I8.min +@[reducible] def i8_max : I8 := Scalar.ofInt I8.max +@[reducible] def i16_min : I16 := Scalar.ofInt I16.min +@[reducible] def i16_max : I16 := Scalar.ofInt I16.max +@[reducible] def i32_min : I32 := Scalar.ofInt I32.min +@[reducible] def i32_max : I32 := Scalar.ofInt I32.max +@[reducible] def i64_min : I64 := Scalar.ofInt I64.min +@[reducible] def i64_max : I64 := Scalar.ofInt I64.max +@[reducible] def i128_min : I128 := Scalar.ofInt I128.min +@[reducible] def i128_max : I128 := Scalar.ofInt I128.max + +-- TODO: reducible? +@[reducible] def usize_min : Usize := Scalar.ofInt Usize.min +@[reducible] def usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize)) +@[reducible] def u8_min : U8 := Scalar.ofInt U8.min +@[reducible] def u8_max : U8 := Scalar.ofInt U8.max +@[reducible] def u16_min : U16 := Scalar.ofInt U16.min +@[reducible] def u16_max : U16 := Scalar.ofInt U16.max +@[reducible] def u32_min : U32 := Scalar.ofInt U32.min +@[reducible] def u32_max : U32 := Scalar.ofInt U32.max +@[reducible] def u64_min : U64 := Scalar.ofInt U64.min +@[reducible] def u64_max : U64 := Scalar.ofInt U64.max +@[reducible] def u128_min : U128 := Scalar.ofInt U128.min +@[reducible] def u128_max : U128 := Scalar.ofInt U128.max + -- TODO: below: not sure this is the best way. -- Should we rather overload operations like +, -, etc.? -- Also, it is possible to automate the generation of those definitions diff --git a/compiler/Driver.ml b/compiler/Driver.ml index d88962db..0fde1d74 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -222,20 +222,6 @@ let () = in if has_loops then log#lwarning (lazy "Support for loops is experimental"); - (* If we target Lean, we request the crates to be split into several files - whenever there are opaque functions *) - if - !backend = Lean - && A.FunDeclId.Map.exists - (fun _ (d : A.fun_decl) -> d.body = None) - m.functions - && not !split_files - then ( - log#error - "For Lean, we request the -split-file option whenever using opaque \ - functions"; - fail ()); - (* We don't support mutually recursive definitions with decreases clauses in Lean *) if !backend = Lean && !extract_decreases_clauses diff --git a/compiler/Extract.ml b/compiler/Extract.ml index de6c2fc8..74540787 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -8,6 +8,7 @@ open Pure open PureUtils open TranslateCore open ExtractBase +open ExtractAssumed open StringUtils open Config module F = Format @@ -3852,8 +3853,13 @@ let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) (* Print the type *) F.pp_open_hovbox fmt 0; extract_ty ctx fmt TypeDeclId.Set.empty false ty; + (* Close the definition *) + F.pp_print_string fmt ")"; + F.pp_close_box fmt (); + (* Close the definition box *) F.pp_close_box fmt (); - (* Close the definition boxe *) F.pp_close_box fmt () + (* Add a line *) + F.pp_print_space fmt () (** Extract a global declaration. diff --git a/compiler/ExtractAssumed.ml b/compiler/ExtractAssumed.ml new file mode 100644 index 00000000..bbcedb2b --- /dev/null +++ b/compiler/ExtractAssumed.ml @@ -0,0 +1,49 @@ +(** This file declares external identifiers that we catch to map them to + definitions coming from the standard libraries in our backends. *) + +open Utils +open StringUtils +open Names + +type simple_name = string list [@@deriving show, ord] + +let name_to_simple_name (s : name) : simple_name = + (* We simply ignore the disambiguators *) + List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s + +(** Small helper which cuts a string at the occurrences of "::" *) +let string_to_simple_name (s : string) : simple_name = + (* No function to split by using string separator?? *) + let name = String.split_on_char ':' s in + List.filter (fun s -> s <> "") name + +module SimpleNameOrd = struct + type t = simple_name + + let compare = compare_simple_name + let to_string = show_simple_name + let pp_t = pp_simple_name + let show_t = show_simple_name +end + +module SimpleNameMap = Collections.MakeMap (SimpleNameOrd) + +let assumed_globals : (string * string) list = + [ + ("core::num::usize::MAX", "usize_max"); + ("core::num::u8::MAX", "u8_max"); + ("core::num::u16::MAX", "u16_max"); + ("core::num::u32::MAX", "u32_max"); + ("core::num::u64::MAX", "u64_max"); + ("core::num::u128::MAX", "u128_max"); + ("core::num::isize::MAX", "isize_max"); + ("core::num::i8::MAX", "i8_max"); + ("core::num::i16::MAX", "i16_max"); + ("core::num::i32::MAX", "i32_max"); + ("core::num::i64::MAX", "i64_max"); + ("core::num::i128::MAX", "i128_max"); + ] + +let assumed_globals_map : string SimpleNameMap.t = + SimpleNameMap.of_list + (List.map (fun (x, y) -> (string_to_simple_name x, y)) assumed_globals) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 435aa10c..9c9e08a5 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -5,6 +5,7 @@ open TranslateCore module C = Contexts module RegionVarId = T.RegionVarId module F = Format +open ExtractAssumed (** The local logger *) let log = L.pure_to_extract_log @@ -1198,12 +1199,23 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : extraction_ctx = (* TODO: update once the body id can be an option *) let is_opaque = false in - let name = ctx.fmt.global_name def.name in let decl = GlobalId def.def_id in - let body = FunId (FromLlbc (Regular def.body_id, None, None)) in - let ctx = ctx_add is_opaque decl (name ^ "_c") ctx in - let ctx = ctx_add is_opaque body (name ^ "_body") ctx in - ctx + + (* Check if the global corresponds to an assumed global that we should map + to a custom definition in our standard library (for instance, happens + with "core::num::usize::MAX") *) + let sname = name_to_simple_name def.name in + match SimpleNameMap.find_opt sname assumed_globals_map with + | Some name -> + (* Yes: register the custom binding *) + ctx_add is_opaque decl name ctx + | None -> + (* Not the case: "standard" registration *) + let name = ctx.fmt.global_name def.name in + let body = FunId (FromLlbc (Regular def.body_id, None, None)) in + let ctx = ctx_add is_opaque decl (name ^ "_c") ctx in + let ctx = ctx_add is_opaque body (name ^ "_body") ctx in + ctx let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl) (ctx : extraction_ctx) : string = diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 1111c297..8c8bbabe 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -12,3 +12,23 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : match fun_id with | Regular id -> (FunDeclId.Map.find id fun_decls).name | Assumed aid -> Assumed.get_assumed_name aid + +(** Return the opaque declarations found in the crate. + + Remark: the list of functions also contains the list of opaque global bodies. + *) +let crate_get_opaque_decls (k : crate) : T.type_decl list * fun_decl list = + let open ExtractAssumed in + let is_opaque_fun (d : fun_decl) : bool = + let sname = name_to_simple_name d.name in + d.body = None && not (SimpleNameMap.mem sname assumed_globals_map) + in + let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in + (* Note that by checking the function bodies we also the globals *) + ( List.filter is_opaque_type (T.TypeDeclId.Map.values k.types), + List.filter is_opaque_fun (FunDeclId.Map.values k.functions) ) + +(** Return true if the crate contains opaque declarations, ignoring the assumed + definitions. *) +let crate_has_opaque_decls (k : crate) : bool = + crate_get_opaque_decls k <> ([], []) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index a4041751..90066163 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -430,19 +430,9 @@ type gen_config = { } (** Returns the pair: (has opaque type decls, has opaque fun decls) *) -let module_has_opaque_decls (ctx : gen_ctx) : bool * bool = - let has_opaque_types = - Pure.TypeDeclId.Map.exists - (fun _ (d : Pure.type_decl) -> - match d.kind with Opaque -> true | _ -> false) - ctx.trans_types - in - let has_opaque_funs = - A.FunDeclId.Map.exists - (fun _ (trans : pure_fun_translation) -> Option.is_none trans.fwd.f.body) - ctx.trans_funs - in - (has_opaque_types, has_opaque_funs) +let crate_has_opaque_decls (ctx : gen_ctx) : bool * bool = + let types, funs = LlbcAstUtils.crate_get_opaque_decls ctx.crate in + (types <> [], funs <> []) (** Export a type declaration. @@ -557,11 +547,20 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) let body = trans.fwd.f in let is_opaque = Option.is_none body.Pure.body in - if + (* Check if we extract the global *) + let extract = config.extract_globals && (((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque)) - then + in + (* Check if it is an assumed global - if yes, we ignore it because we + map the definition to one in the standard library *) + let open ExtractAssumed in + let sname = name_to_simple_name global.name in + let extract = + extract && SimpleNameMap.find_opt sname assumed_globals_map = None + in + if extract then (* We don't wrap global declaration groups between calls to functions [{start, end}_global_decl_group] (which don't exist): global declaration groups are always singletons, so the [extract_global_decl] function @@ -828,7 +827,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) config.extract_opaque && config.extract_fun_decls && !Config.wrap_opaque_in_sig && - let _, opaque_funs = module_has_opaque_decls ctx in + let _, opaque_funs = crate_has_opaque_decls ctx in opaque_funs in if wrap_in_sig then ( @@ -1233,7 +1232,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (* Check if there are opaque types and functions - in which case we need * to split *) - let has_opaque_types, has_opaque_funs = module_has_opaque_decls ctx in + let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx in let has_opaque_types = has_opaque_types || !Config.use_state in (* Extract the types *) @@ -1302,7 +1301,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : in extract_file template_clauses_config ctx file_info); - (* Extract the opaque functions, if needed *) + (* Extract the opaque declarations, if needed *) let opaque_funs_module = if has_opaque_funs then ( (* In the case of Lean we generate a template file *) @@ -1330,6 +1329,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : { base_gen_config with extract_fun_decls = true; + extract_globals = true; extract_transparent = false; extract_opaque = true; interface = true; diff --git a/compiler/dune b/compiler/dune index db099c3c..2f5a0a44 100644 --- a/compiler/dune +++ b/compiler/dune @@ -22,6 +22,7 @@ Expressions ExpressionsUtils Extract + ExtractAssumed ExtractBase FunsAnalysis Identifiers -- cgit v1.3.1 From 0f0e4be7dc746e2676db33f850bbeddf239eaec8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 13 Oct 2023 00:40:37 +0200 Subject: Add sup --- backends/coq/Primitives.v | 3 ++ backends/lean/Base/IList/IList.lean | 57 +++++++++++++++++++++++++++++++- backends/lean/Base/Primitives/Array.lean | 9 +++++ compiler/Assumed.ml | 15 +++++++++ compiler/Driver.ml | 2 ++ compiler/Extract.ml | 4 ++- compiler/InterpreterStatements.ml | 2 +- compiler/PrintPure.ml | 1 + compiler/PureMicroPasses.ml | 2 +- 9 files changed, 91 insertions(+), 4 deletions(-) (limited to 'compiler/Driver.ml') diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index 8d6c9c8d..b92eb967 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/Primitives.v @@ -433,6 +433,9 @@ Qed. (* TODO: finish the definitions *) Axiom mk_array : forall (T : Type) (n : usize) (l : list T), array T n. +(* For initialization *) +Axiom array_repeat : forall {T : Type} (n : usize) (x : T), array T n. + Axiom array_index_shared : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. Axiom array_index_mut_fwd : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. Axiom array_index_mut_back : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n). diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean index 0b483e90..f10ec4e7 100644 --- a/backends/lean/Base/IList/IList.lean +++ b/backends/lean/Base/IList/IList.lean @@ -112,7 +112,19 @@ def pairwise_rel section Lemmas -variable {α : Type u} +variable {α : Type u} + +def ireplicate {α : Type u} (i : ℤ) (x : α) : List α := + if i ≤ 0 then [] + else x :: ireplicate (i - 1) x +termination_by ireplicate i x => i.toNat +decreasing_by + simp_wf + -- TODO: simplify this kind of proofs + simp at * + have : 0 ≤ i := by linarith + have : 1 ≤ i := by linarith + simp [Int.toNat_sub_of_le, *] @[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update] @[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update] @@ -129,6 +141,10 @@ variable {α : Type u} @[simp] theorem slice_nil : slice i j ([] : List α) = [] := by simp [slice] @[simp] theorem slice_zero : slice 0 0 (ls : List α) = [] := by cases ls <;> simp [slice] +@[simp] theorem ireplicate_zero : ireplicate 0 x = [] := by rw [ireplicate]; simp +@[simp] theorem ireplicate_nzero_cons (hne : 0 < i) : ireplicate i x = x :: ireplicate (i - 1) x := by + rw [ireplicate]; simp [*]; intro; linarith + @[simp] theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : slice i j ((x :: tl) : List α) = slice (i - 1) (j - 1) tl := match tl with @@ -144,6 +160,45 @@ theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : s conv at this => lhs; simp [slice, *] simp [*, slice] +@[simp] +theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : + ireplicate l x = replicate l.toNat x := + if hz: l = 0 then by + simp [*] + else by + have : 0 < l := by int_tac + have hr := ireplicate_replicate (l - 1) x (by int_tac) + simp [*] + have hl : l.toNat = .succ (l.toNat - 1) := by + cases hl: l.toNat <;> simp_all + conv => rhs; rw[hl] +termination_by ireplicate_replicate l x h => l.toNat +decreasing_by + simp_wf + -- TODO: simplify this kind of proofs + simp at * + have : 0 ≤ l := by linarith + have : 1 ≤ l := by linarith + simp [Int.toNat_sub_of_le, *] + +@[simp] +theorem ireplicate_len {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : + (ireplicate l x).len = l := + if hz: l = 0 then by + simp [*] + else by + have : 0 < l := by int_tac + have hr := ireplicate_len (l - 1) x (by int_tac) + simp [*] +termination_by ireplicate_len l x h => l.toNat +decreasing_by + simp_wf + -- TODO: simplify this kind of proofs + simp at * + have : 0 ≤ l := by linarith + have : 1 ≤ l := by linarith + simp [Int.toNat_sub_of_le, *] + theorem len_eq_length (ls : List α) : ls.len = ls.length := by induction ls . rfl diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean index 6c95fd78..49c84bee 100644 --- a/backends/lean/Base/Primitives/Array.lean +++ b/backends/lean/Base/Primitives/Array.lean @@ -51,6 +51,15 @@ def Array.index_shared (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Re | none => fail .arrayOutOfBounds | some x => ret x +-- For initialization +def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n := + ⟨ List.ireplicate n.val x, by have h := n.hmin; simp_all [Scalar.min] ⟩ + +@[pspec] +theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) : + ∃ a, Array.repeat α n x = a ∧ a.val = List.ireplicate n.val x := by + simp [Array.repeat] + /- In the theorems below: we don't always need the `∃ ..`, but we use one so that `progress` introduces an opaque variable and an equality. This helps control the context. diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index e156c335..109175af 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -298,6 +298,19 @@ module Sig = struct let array_subslice_sig (is_mut : bool) = mk_array_slice_subslice_sig true is_mut + let array_repeat_sig = + let generics = + (* *) + mk_generic_params [] [ type_param_0 ] [ cg_param_0 ] + in + let regions_hierarchy = [] (* <> *) in + let inputs = [ tvar_0 (* T *) ] in + let output = + (* [T; N] *) + mk_array_ty tvar_0 cgvar_0 + in + mk_sig generics regions_hierarchy inputs output + let slice_subslice_sig (is_mut : bool) = mk_array_slice_subslice_sig false is_mut @@ -384,6 +397,8 @@ let assumed_infos : assumed_info list = Sig.array_subslice_sig true, true, to_name [ "@ArraySubsliceMut" ] ); + (* Array Repeat *) + (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ]); (* Slice Index *) ( SliceIndexShared, Sig.slice_index_sig false, diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 0fde1d74..8a30ead9 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -24,6 +24,8 @@ let _ = main_log#set_level EL.Info; llbc_of_json_logger#set_level EL.Info; pre_passes_log#set_level EL.Info; + associated_types_log#set_level EL.Info; + contexts_log#set_level EL.Info; interpreter_log#set_level EL.Info; statements_log#set_level EL.Info; loops_match_ctxs_log#set_level EL.Info; diff --git a/compiler/Extract.ml b/compiler/Extract.ml index ce423acf..99ea14a4 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -338,6 +338,7 @@ let assumed_llbc_functions () : (ArraySubsliceShared, None, "array_subslice_shared"); (ArraySubsliceMut, None, "array_subslice_mut_fwd"); (ArraySubsliceMut, rg0, "array_subslice_mut_back"); + (ArrayRepeat, None, "array_repeat"); (SliceIndexShared, None, "slice_index_shared"); (SliceIndexMut, None, "slice_index_mut_fwd"); (SliceIndexMut, rg0, "slice_index_mut_back"); @@ -369,6 +370,7 @@ let assumed_llbc_functions () : (ArraySubsliceShared, None, "Array.subslice_shared"); (ArraySubsliceMut, None, "Array.subslice_mut"); (ArraySubsliceMut, rg0, "Array.subslice_mut_back"); + (ArrayRepeat, None, "Array.repeat"); (SliceIndexShared, None, "Slice.index_shared"); (SliceIndexMut, None, "Slice.index_mut"); (SliceIndexMut, rg0, "Slice.index_mut_back"); @@ -3212,7 +3214,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hvbox fmt ctx.indent_incr; let need_paren = inside in if need_paren then F.pp_print_string fmt "("; - (* Open the box for `Array.mk T N [` *) + (* Open the box for `Array.replicate T N [` *) F.pp_open_hovbox fmt ctx.indent_incr; (* Print the array constructor *) let cs = ctx_get_struct false (Assumed Array) ctx in diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 42073f0b..36bc3492 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -646,7 +646,7 @@ let eval_assumed_function_call_concrete (config : C.config) eval_vec_function_concrete config fid generics | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut - | SliceIndexShared | SliceIndexMut | SliceSubsliceShared + | ArrayRepeat | SliceIndexShared | SliceIndexMut | SliceSubsliceShared | SliceSubsliceMut | SliceLen -> raise (Failure "Unimplemented") in diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index d539dcf6..5fb5978b 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -610,6 +610,7 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string = | ArrayToSliceMut -> "@ArrayToSliceMut" | ArraySubsliceShared -> "@ArraySubsliceShared" | ArraySubsliceMut -> "@ArraySubsliceMut" + | ArrayRepeat -> "@ArrayRepeat" | SliceLen -> "@SliceLen" | SliceIndexShared -> "@SliceIndexShared" | SliceIndexMut -> "@SliceIndexMut" diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 2130d5c2..cedc3559 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1563,7 +1563,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = | ArraySubsliceMut | SliceIndexShared | SliceIndexMut | SliceSubsliceShared | SliceSubsliceMut | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut - | SliceLen ), + | ArrayRepeat | SliceLen ), _ ) -> super#visit_texpression env e) | _ -> super#visit_texpression env e) -- cgit v1.3.1 From 0ba1c30f735f6e1cce771800d41042e6dc15e86f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 16 Oct 2023 10:10:40 +0200 Subject: Fix a small issue --- compiler/Driver.ml | 2 -- compiler/Interpreter.ml | 64 ++++++++++++++++++++++++++++++++++++++++--------- 2 files changed, 53 insertions(+), 13 deletions(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 8a30ead9..414b042d 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -168,8 +168,6 @@ let () = decompose_monadic_let_bindings := true; decompose_nested_let_patterns := true | Lean -> - (* The Lean backend is experimental: print a warning *) - log#lwarning (lazy "The Lean backend is experimental"); (* 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"; diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 09f25ca1..24ff4808 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -84,22 +84,64 @@ let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (sg : A.fun_sig) Subst.make_const_generic_subst_from_vars sg.generics.const_generics const_generics in - let tr_subst _ = raise (Failure "Unexpected local trait clause") in - let subst = { Subst.r_subst; ty_subst; cg_subst; tr_subst; tr_self } in - let trait_refs = - List.map - (fun (c : T.trait_clause) -> + (* TODO: some clauses may use the types of other clauses, so we may have to + reorder them. + + Example: + If in Rust we write: + {[ + pub fn use_get<'a, T: Get>(x: &'a mut T) -> u32 + where + T::Item: ToU32, + { + x.get().to_u32() + } + ]} + + In LLBC we get: + {[ + fn demo::use_get<'a, T>(@1: &'a mut (T)) -> u32 + where + [@TraitClause0]: demo::Get, + [@TraitClause1]: demo::ToU32<@TraitClause0::Item>, // HERE + { + ... // Omitted + } + ]} + *) + (* We will need to update the trait refs map while we perform the instantiations *) + let mk_tr_subst + (tr_map : T.erased_region T.trait_instance_id T.TraitClauseId.Map.t) + clause_id : T.erased_region T.trait_instance_id = + match T.TraitClauseId.Map.find_opt clause_id tr_map with + | Some tr -> tr + | None -> raise (Failure "Local trait clause not found") + in + let mk_subst tr_map = + let tr_subst = mk_tr_subst tr_map in + { Subst.r_subst; ty_subst; cg_subst; tr_subst; tr_self } + in + let _, trait_refs = + List.fold_left_map + (fun tr_map (c : T.trait_clause) -> + let subst = mk_subst tr_map in let { T.trait_id = trait_decl_id; generics; _ } = c in let generics = Subst.generic_args_substitute subst generics in let trait_decl_ref = { T.trait_decl_id; decl_generics = generics } in (* Note that because we directly refer to the clause, we give it empty generics *) - { - T.trait_id = T.Clause c.clause_id; - generics = TypesUtils.mk_empty_generic_args; - trait_decl_ref; - }) - trait_clauses + let trait_id = T.Clause c.clause_id in + let trait_ref = + { + T.trait_id; + generics = TypesUtils.mk_empty_generic_args; + trait_decl_ref; + } + in + (* Update the traits map *) + let tr_map = T.TraitClauseId.Map.add c.T.clause_id trait_id tr_map in + (tr_map, trait_ref)) + T.TraitClauseId.Map.empty trait_clauses in { T.regions; types; const_generics; trait_refs } in -- cgit v1.3.1 From 4f507fa565a43b419af6ea7a641a353f62213b21 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 25 Oct 2023 11:40:47 +0200 Subject: Remove the warning for loops --- compiler/Driver.ml | 8 -------- 1 file changed, 8 deletions(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 414b042d..3b9ea4d1 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -214,14 +214,6 @@ let () = log#linfo (lazy ("Imported: " ^ filename)); log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n")); - (* Print a warning if the crate contains loops (loops are experimental for now) *) - let has_loops = - A.FunDeclId.Map.exists - (fun _ -> Aeneas.LlbcAstUtils.fun_decl_has_loops) - m.functions - in - if has_loops then log#lwarning (lazy "Support for loops is experimental"); - (* We don't support mutually recursive definitions with decreases clauses in Lean *) if !backend = Lean && !extract_decreases_clauses -- cgit v1.3.1 From 1110b3da85e93ba0755a665edd5b8c986c54cef0 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 26 Oct 2023 16:15:35 +0200 Subject: Make minor modifications and update the array test for F* --- compiler/Driver.ml | 4 +- compiler/ExtractBase.ml | 22 +- compiler/ExtractBuiltin.ml | 5 +- tests/fstar/array/Array.Clauses.Template.fst | 5 +- tests/fstar/array/Array.Funs.fst | 348 ++++++++++++++------------- tests/fstar/array/Array.Types.fst | 4 +- 6 files changed, 200 insertions(+), 188 deletions(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 3b9ea4d1..b660b5a5 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -162,7 +162,9 @@ let () = | FStar -> (* Some patterns are not supported *) decompose_monadic_let_bindings := false; - decompose_nested_let_patterns := false + decompose_nested_let_patterns := false; + (* F* can disambiguate the field names *) + record_fields_short_names := true | Coq -> (* Some patterns are not supported *) decompose_monadic_let_bindings := true; diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 8f71116c..6faa40b2 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1332,22 +1332,20 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) let rg_suff = (* TODO: make all the backends match what is done for Lean *) match rg with - | None -> ( - match !Config.backend with - | FStar | Coq | HOL4 -> "_fwd" - | Lean -> - (* In order to avoid name conflicts: - * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used) - * - otherwise, no suffix (because the backward functions will have a suffix) - *) - if num_backs = 1 && not keep_fwd then "_fwd" else "") + | None -> + if + (* In order to avoid name conflicts: + * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used) + * - otherwise, no suffix (because the backward functions will have a suffix) + *) + num_backs = 1 && not keep_fwd + then "_fwd" + else "" | Some rg -> assert (num_region_groups > 0 && num_backs > 0); if num_backs = 1 then (* Exactly one backward function *) - match !Config.backend with - | FStar | Coq | HOL4 -> if not keep_fwd then "_fwd_back" else "_back" - | Lean -> if not keep_fwd then "" else "_back" + if not keep_fwd then "" else "_back" else if (* Several region groups/backward functions: - if all the regions in the group have names, we use those names diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 2dbacce3..c6bde9c2 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -149,7 +149,10 @@ let builtin_types () : builtin_type_info list = let fields = List.map (fun (rname, name) -> - (rname, backend_choice (extract_name ^ name) name)) + ( rname, + match !backend with + | FStar | Lean -> name + | Coq | HOL4 -> extract_name ^ "_" ^ name )) fields in let constructor = mk_struct_constructor extract_name in diff --git a/tests/fstar/array/Array.Clauses.Template.fst b/tests/fstar/array/Array.Clauses.Template.fst index 8a15e230..06056d61 100644 --- a/tests/fstar/array/Array.Clauses.Template.fst +++ b/tests/fstar/array/Array.Clauses.Template.fst @@ -8,11 +8,12 @@ open Array.Types (** [array::sum]: decreases clause *) unfold -let sum_loop_decreases (s : slice u32) (sum : u32) (i : usize) : nat = admit () +let sum_loop_decreases (s : slice u32) (sum0 : u32) (i : usize) : nat = + admit () (** [array::sum2]: decreases clause *) unfold -let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum : u32) +let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum0 : u32) (i : usize) : nat = admit () diff --git a/tests/fstar/array/Array.Funs.fst b/tests/fstar/array/Array.Funs.fst index 83256398..a6808c98 100644 --- a/tests/fstar/array/Array.Funs.fst +++ b/tests/fstar/array/Array.Funs.fst @@ -7,361 +7,369 @@ include Array.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" +(** [array::incr]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +let incr (x : u32) : result u32 = + u32_add x 1 + (** [array::array_to_shared_slice_]: forward function *) -let array_to_shared_slice__fwd - (t : Type0) (s : array t 32) : result (slice t) = - array_to_slice_shared t 32 s +let array_to_shared_slice_ (t : Type0) (s : array t 32) : result (slice t) = + array_to_slice t 32 s (** [array::array_to_mut_slice_]: forward function *) -let array_to_mut_slice__fwd (t : Type0) (s : array t 32) : result (slice t) = - array_to_slice_mut_fwd t 32 s +let array_to_mut_slice_ (t : Type0) (s : array t 32) : result (slice t) = + array_to_slice t 32 s (** [array::array_to_mut_slice_]: backward function 0 *) let array_to_mut_slice__back (t : Type0) (s : array t 32) (ret : slice t) : result (array t 32) = - array_to_slice_mut_back t 32 s ret + array_from_slice t 32 s ret (** [array::array_len]: forward function *) -let array_len_fwd (t : Type0) (s : array t 32) : result usize = - let* s0 = array_to_slice_shared t 32 s in let i = slice_len t s0 in Return i +let array_len (t : Type0) (s : array t 32) : result usize = + let* s0 = array_to_slice t 32 s in let i = slice_len t s0 in Return i (** [array::shared_array_len]: forward function *) -let shared_array_len_fwd (t : Type0) (s : array t 32) : result usize = - let* s0 = array_to_slice_shared t 32 s in let i = slice_len t s0 in Return i +let shared_array_len (t : Type0) (s : array t 32) : result usize = + let* s0 = array_to_slice t 32 s in let i = slice_len t s0 in Return i (** [array::shared_slice_len]: forward function *) -let shared_slice_len_fwd (t : Type0) (s : slice t) : result usize = +let shared_slice_len (t : Type0) (s : slice t) : result usize = let i = slice_len t s in Return i (** [array::index_array_shared]: forward function *) -let index_array_shared_fwd - (t : Type0) (s : array t 32) (i : usize) : result t = - array_index_shared t 32 s i +let index_array_shared (t : Type0) (s : array t 32) (i : usize) : result t = + array_index_usize t 32 s i (** [array::index_array_u32]: forward function *) -let index_array_u32_fwd (s : array u32 32) (i : usize) : result u32 = - array_index_shared u32 32 s i - -(** [array::index_array_generic]: forward function *) -let index_array_generic_fwd - (n : usize) (s : array u32 n) (i : usize) : result u32 = - array_index_shared u32 n s i - -(** [array::index_array_generic_call]: forward function *) -let index_array_generic_call_fwd - (n : usize) (s : array u32 n) (i : usize) : result u32 = - index_array_generic_fwd n s i +let index_array_u32 (s : array u32 32) (i : usize) : result u32 = + array_index_usize u32 32 s i (** [array::index_array_copy]: forward function *) -let index_array_copy_fwd (x : array u32 32) : result u32 = - array_index_shared u32 32 x 0 +let index_array_copy (x : array u32 32) : result u32 = + array_index_usize u32 32 x 0 (** [array::index_mut_array]: forward function *) -let index_mut_array_fwd (t : Type0) (s : array t 32) (i : usize) : result t = - array_index_mut_fwd t 32 s i +let index_mut_array (t : Type0) (s : array t 32) (i : usize) : result t = + array_index_usize t 32 s i (** [array::index_mut_array]: backward function 0 *) let index_mut_array_back (t : Type0) (s : array t 32) (i : usize) (ret : t) : result (array t 32) = - array_index_mut_back t 32 s i ret + array_update_usize t 32 s i ret (** [array::index_slice]: forward function *) -let index_slice_fwd (t : Type0) (s : slice t) (i : usize) : result t = - slice_index_shared t s i +let index_slice (t : Type0) (s : slice t) (i : usize) : result t = + slice_index_usize t s i (** [array::index_mut_slice]: forward function *) -let index_mut_slice_fwd (t : Type0) (s : slice t) (i : usize) : result t = - slice_index_mut_fwd t s i +let index_mut_slice (t : Type0) (s : slice t) (i : usize) : result t = + slice_index_usize t s i (** [array::index_mut_slice]: backward function 0 *) let index_mut_slice_back (t : Type0) (s : slice t) (i : usize) (ret : t) : result (slice t) = - slice_index_mut_back t s i ret + slice_update_usize t s i ret (** [array::slice_subslice_shared_]: forward function *) -let slice_subslice_shared__fwd +let slice_subslice_shared_ (x : slice u32) (y : usize) (z : usize) : result (slice u32) = - slice_subslice_shared u32 x (Mkrange y z) + core_slice_index_Slice_index u32 (core_ops_range_Range usize) + (core_slice_index_Range_coresliceindexSliceIndexInst u32) x + { start = y; end_ = z } (** [array::slice_subslice_mut_]: forward function *) -let slice_subslice_mut__fwd +let slice_subslice_mut_ (x : slice u32) (y : usize) (z : usize) : result (slice u32) = - slice_subslice_mut_fwd u32 x (Mkrange y z) + core_slice_index_Slice_index_mut u32 (core_ops_range_Range usize) + (core_slice_index_Range_coresliceindexSliceIndexInst u32) x + { start = y; end_ = z } (** [array::slice_subslice_mut_]: backward function 0 *) let slice_subslice_mut__back (x : slice u32) (y : usize) (z : usize) (ret : slice u32) : result (slice u32) = - slice_subslice_mut_back u32 x (Mkrange y z) ret + core_slice_index_Slice_index_mut_back u32 (core_ops_range_Range usize) + (core_slice_index_Range_coresliceindexSliceIndexInst u32) x + { start = y; end_ = z } ret (** [array::array_to_slice_shared_]: forward function *) -let array_to_slice_shared__fwd (x : array u32 32) : result (slice u32) = - array_to_slice_shared u32 32 x +let array_to_slice_shared_ (x : array u32 32) : result (slice u32) = + array_to_slice u32 32 x (** [array::array_to_slice_mut_]: forward function *) -let array_to_slice_mut__fwd (x : array u32 32) : result (slice u32) = - array_to_slice_mut_fwd u32 32 x +let array_to_slice_mut_ (x : array u32 32) : result (slice u32) = + array_to_slice u32 32 x (** [array::array_to_slice_mut_]: backward function 0 *) let array_to_slice_mut__back (x : array u32 32) (ret : slice u32) : result (array u32 32) = - array_to_slice_mut_back u32 32 x ret + array_from_slice u32 32 x ret (** [array::array_subslice_shared_]: forward function *) -let array_subslice_shared__fwd +let array_subslice_shared_ (x : array u32 32) (y : usize) (z : usize) : result (slice u32) = - array_subslice_shared u32 32 x (Mkrange y z) + core_array_Array_index u32 (core_ops_range_Range usize) 32 + (core_slice_index_Slice_coreopsindexIndexInst u32 (core_ops_range_Range + usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x + { start = y; end_ = z } (** [array::array_subslice_mut_]: forward function *) -let array_subslice_mut__fwd +let array_subslice_mut_ (x : array u32 32) (y : usize) (z : usize) : result (slice u32) = - array_subslice_mut_fwd u32 32 x (Mkrange y z) + core_array_Array_index_mut u32 (core_ops_range_Range usize) 32 + (core_slice_index_Slice_coreopsindexIndexMutInst u32 (core_ops_range_Range + usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x + { start = y; end_ = z } (** [array::array_subslice_mut_]: backward function 0 *) let array_subslice_mut__back (x : array u32 32) (y : usize) (z : usize) (ret : slice u32) : result (array u32 32) = - array_subslice_mut_back u32 32 x (Mkrange y z) ret + core_array_Array_index_mut_back u32 (core_ops_range_Range usize) 32 + (core_slice_index_Slice_coreopsindexIndexMutInst u32 (core_ops_range_Range + usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x + { start = y; end_ = z } ret (** [array::index_slice_0]: forward function *) -let index_slice_0_fwd (t : Type0) (s : slice t) : result t = - slice_index_shared t s 0 +let index_slice_0 (t : Type0) (s : slice t) : result t = + slice_index_usize t s 0 (** [array::index_array_0]: forward function *) -let index_array_0_fwd (t : Type0) (s : array t 32) : result t = - array_index_shared t 32 s 0 +let index_array_0 (t : Type0) (s : array t 32) : result t = + array_index_usize t 32 s 0 (** [array::index_index_array]: forward function *) -let index_index_array_fwd +let index_index_array (s : array (array u32 32) 32) (i : usize) (j : usize) : result u32 = - let* a = array_index_shared (array u32 32) 32 s i in - array_index_shared u32 32 a j - -(** [array::const_gen_ret]: forward function *) -let const_gen_ret_fwd (n : usize) : result usize = - Return n + let* a = array_index_usize (array u32 32) 32 s i in + array_index_usize u32 32 a j (** [array::update_update_array]: forward function *) -let update_update_array_fwd +let update_update_array (s : array (array u32 32) 32) (i : usize) (j : usize) : result unit = - let* a = array_index_mut_fwd (array u32 32) 32 s i in - let* a0 = array_index_mut_back u32 32 a j 0 in - let* _ = array_index_mut_back (array u32 32) 32 s i a0 in + let* a = array_index_usize (array u32 32) 32 s i in + let* a0 = array_update_usize u32 32 a j 0 in + let* _ = array_update_usize (array u32 32) 32 s i a0 in Return () (** [array::array_local_deep_copy]: forward function *) -let array_local_deep_copy_fwd (x : array u32 32) : result unit = +let array_local_deep_copy (x : array u32 32) : result unit = Return () (** [array::take_array]: forward function *) -let take_array_fwd (a : array u32 2) : result unit = +let take_array (a : array u32 2) : result unit = Return () (** [array::take_array_borrow]: forward function *) -let take_array_borrow_fwd (a : array u32 2) : result unit = +let take_array_borrow (a : array u32 2) : result unit = Return () (** [array::take_slice]: forward function *) -let take_slice_fwd (s : slice u32) : result unit = +let take_slice (s : slice u32) : result unit = Return () (** [array::take_mut_slice]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) -let take_mut_slice_fwd_back (s : slice u32) : result (slice u32) = +let take_mut_slice (s : slice u32) : result (slice u32) = Return s (** [array::take_all]: forward function *) -let take_all_fwd : result unit = - let* _ = take_array_fwd (mk_array u32 2 [ 0; 0 ]) in - let* _ = take_array_borrow_fwd (mk_array u32 2 [ 0; 0 ]) in - let* s = array_to_slice_shared u32 2 (mk_array u32 2 [ 0; 0 ]) in - let* _ = take_slice_fwd s in - let* s0 = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in - let* s1 = take_mut_slice_fwd_back s0 in - let* _ = array_to_slice_mut_back u32 2 (mk_array u32 2 [ 0; 0 ]) s1 in +let take_all : result unit = + let* _ = take_array (mk_array u32 2 [ 0; 0 ]) in + let* _ = take_array_borrow (mk_array u32 2 [ 0; 0 ]) in + let* s = array_to_slice u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* _ = take_slice s in + let* s0 = array_to_slice u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* s1 = take_mut_slice s0 in + let* _ = array_from_slice u32 2 (mk_array u32 2 [ 0; 0 ]) s1 in Return () (** [array::index_array]: forward function *) -let index_array_fwd (x : array u32 2) : result u32 = - array_index_shared u32 2 x 0 +let index_array (x : array u32 2) : result u32 = + array_index_usize u32 2 x 0 (** [array::index_array_borrow]: forward function *) -let index_array_borrow_fwd (x : array u32 2) : result u32 = - array_index_shared u32 2 x 0 +let index_array_borrow (x : array u32 2) : result u32 = + array_index_usize u32 2 x 0 (** [array::index_slice_u32_0]: forward function *) -let index_slice_u32_0_fwd (x : slice u32) : result u32 = - slice_index_shared u32 x 0 +let index_slice_u32_0 (x : slice u32) : result u32 = + slice_index_usize u32 x 0 (** [array::index_mut_slice_u32_0]: forward function *) -let index_mut_slice_u32_0_fwd (x : slice u32) : result u32 = - slice_index_shared u32 x 0 +let index_mut_slice_u32_0 (x : slice u32) : result u32 = + slice_index_usize u32 x 0 (** [array::index_mut_slice_u32_0]: backward function 0 *) let index_mut_slice_u32_0_back (x : slice u32) : result (slice u32) = - let* _ = slice_index_shared u32 x 0 in Return x + let* _ = slice_index_usize u32 x 0 in Return x (** [array::index_all]: forward function *) -let index_all_fwd : result u32 = - let* i = index_array_fwd (mk_array u32 2 [ 0; 0 ]) in - let* i0 = index_array_fwd (mk_array u32 2 [ 0; 0 ]) in +let index_all : result u32 = + let* i = index_array (mk_array u32 2 [ 0; 0 ]) in + let* i0 = index_array (mk_array u32 2 [ 0; 0 ]) in let* i1 = u32_add i i0 in - let* i2 = index_array_borrow_fwd (mk_array u32 2 [ 0; 0 ]) in + let* i2 = index_array_borrow (mk_array u32 2 [ 0; 0 ]) in let* i3 = u32_add i1 i2 in - let* s = array_to_slice_shared u32 2 (mk_array u32 2 [ 0; 0 ]) in - let* i4 = index_slice_u32_0_fwd s in + let* s = array_to_slice u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* i4 = index_slice_u32_0 s in let* i5 = u32_add i3 i4 in - let* s0 = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in - let* i6 = index_mut_slice_u32_0_fwd s0 in + let* s0 = array_to_slice u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* i6 = index_mut_slice_u32_0 s0 in let* i7 = u32_add i5 i6 in let* s1 = index_mut_slice_u32_0_back s0 in - let* _ = array_to_slice_mut_back u32 2 (mk_array u32 2 [ 0; 0 ]) s1 in + let* _ = array_from_slice u32 2 (mk_array u32 2 [ 0; 0 ]) s1 in Return i7 (** [array::update_array]: forward function *) -let update_array_fwd (x : array u32 2) : result unit = - let* _ = array_index_mut_back u32 2 x 0 1 in Return () +let update_array (x : array u32 2) : result unit = + let* _ = array_update_usize u32 2 x 0 1 in Return () (** [array::update_array_mut_borrow]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) -let update_array_mut_borrow_fwd_back (x : array u32 2) : result (array u32 2) = - array_index_mut_back u32 2 x 0 1 +let update_array_mut_borrow (x : array u32 2) : result (array u32 2) = + array_update_usize u32 2 x 0 1 (** [array::update_mut_slice]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) -let update_mut_slice_fwd_back (x : slice u32) : result (slice u32) = - slice_index_mut_back u32 x 0 1 +let update_mut_slice (x : slice u32) : result (slice u32) = + slice_update_usize u32 x 0 1 (** [array::update_all]: forward function *) -let update_all_fwd : result unit = - let* _ = update_array_fwd (mk_array u32 2 [ 0; 0 ]) in - let* x = update_array_mut_borrow_fwd_back (mk_array u32 2 [ 0; 0 ]) in - let* s = array_to_slice_mut_fwd u32 2 x in - let* s0 = update_mut_slice_fwd_back s in - let* _ = array_to_slice_mut_back u32 2 x s0 in +let update_all : result unit = + let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in + let* x = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in + let* s = array_to_slice u32 2 x in + let* s0 = update_mut_slice s in + let* _ = array_from_slice u32 2 x s0 in Return () (** [array::range_all]: forward function *) -let range_all_fwd : result unit = +let range_all : result unit = let* s = - array_subslice_mut_fwd u32 4 (mk_array u32 4 [ 0; 0; 0; 0 ]) (Mkrange 1 3) - in - let* s0 = update_mut_slice_fwd_back s in + core_array_Array_index_mut u32 (core_ops_range_Range usize) 4 + (core_slice_index_Slice_coreopsindexIndexMutInst u32 + (core_ops_range_Range usize) + (core_slice_index_Range_coresliceindexSliceIndexInst u32)) + (mk_array u32 4 [ 0; 0; 0; 0 ]) { start = 1; end_ = 3 } in + let* s0 = update_mut_slice s in let* _ = - array_subslice_mut_back u32 4 (mk_array u32 4 [ 0; 0; 0; 0 ]) (Mkrange 1 3) - s0 in + core_array_Array_index_mut_back u32 (core_ops_range_Range usize) 4 + (core_slice_index_Slice_coreopsindexIndexMutInst u32 + (core_ops_range_Range usize) + (core_slice_index_Range_coresliceindexSliceIndexInst u32)) + (mk_array u32 4 [ 0; 0; 0; 0 ]) { start = 1; end_ = 3 } s0 in Return () (** [array::deref_array_borrow]: forward function *) -let deref_array_borrow_fwd (x : array u32 2) : result u32 = - array_index_shared u32 2 x 0 +let deref_array_borrow (x : array u32 2) : result u32 = + array_index_usize u32 2 x 0 (** [array::deref_array_mut_borrow]: forward function *) -let deref_array_mut_borrow_fwd (x : array u32 2) : result u32 = - array_index_shared u32 2 x 0 +let deref_array_mut_borrow (x : array u32 2) : result u32 = + array_index_usize u32 2 x 0 (** [array::deref_array_mut_borrow]: backward function 0 *) let deref_array_mut_borrow_back (x : array u32 2) : result (array u32 2) = - let* _ = array_index_shared u32 2 x 0 in Return x + let* _ = array_index_usize u32 2 x 0 in Return x (** [array::take_array_t]: forward function *) -let take_array_t_fwd (a : array t_t 2) : result unit = +let take_array_t (a : array ab_t 2) : result unit = Return () (** [array::non_copyable_array]: forward function *) -let non_copyable_array_fwd : result unit = - let* _ = take_array_t_fwd (mk_array t_t 2 [ TA; TB ]) in Return () +let non_copyable_array : result unit = + let* _ = take_array_t (mk_array ab_t 2 [ ABA; ABB ]) in Return () (** [array::sum]: loop 0: forward function *) -let rec sum_loop_fwd - (s : slice u32) (sum : u32) (i : usize) : - Tot (result u32) (decreases (sum_loop_decreases s sum i)) +let rec sum_loop + (s : slice u32) (sum0 : u32) (i : usize) : + Tot (result u32) (decreases (sum_loop_decreases s sum0 i)) = let i0 = slice_len u32 s in if i < i0 then - let* i1 = slice_index_shared u32 s i in - let* sum0 = u32_add sum i1 in + let* i1 = slice_index_usize u32 s i in + let* sum1 = u32_add sum0 i1 in let* i2 = usize_add i 1 in - sum_loop_fwd s sum0 i2 - else Return sum + sum_loop s sum1 i2 + else Return sum0 (** [array::sum]: forward function *) -let sum_fwd (s : slice u32) : result u32 = - sum_loop_fwd s 0 0 +let sum (s : slice u32) : result u32 = + sum_loop s 0 0 (** [array::sum2]: loop 0: forward function *) -let rec sum2_loop_fwd - (s : slice u32) (s2 : slice u32) (sum : u32) (i : usize) : - Tot (result u32) (decreases (sum2_loop_decreases s s2 sum i)) +let rec sum2_loop + (s : slice u32) (s2 : slice u32) (sum0 : u32) (i : usize) : + Tot (result u32) (decreases (sum2_loop_decreases s s2 sum0 i)) = let i0 = slice_len u32 s in if i < i0 then - let* i1 = slice_index_shared u32 s i in - let* i2 = slice_index_shared u32 s2 i in + let* i1 = slice_index_usize u32 s i in + let* i2 = slice_index_usize u32 s2 i in let* i3 = u32_add i1 i2 in - let* sum0 = u32_add sum i3 in + let* sum1 = u32_add sum0 i3 in let* i4 = usize_add i 1 in - sum2_loop_fwd s s2 sum0 i4 - else Return sum + sum2_loop s s2 sum1 i4 + else Return sum0 (** [array::sum2]: forward function *) -let sum2_fwd (s : slice u32) (s2 : slice u32) : result u32 = +let sum2 (s : slice u32) (s2 : slice u32) : result u32 = let i = slice_len u32 s in let i0 = slice_len u32 s2 in - if not (i = i0) then Fail Failure else sum2_loop_fwd s s2 0 0 + if not (i = i0) then Fail Failure else sum2_loop s s2 0 0 (** [array::f0]: forward function *) -let f0_fwd : result unit = - let* s = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 1; 2 ]) in - let* s0 = slice_index_mut_back u32 s 0 1 in - let* _ = array_to_slice_mut_back u32 2 (mk_array u32 2 [ 1; 2 ]) s0 in +let f0 : result unit = + let* s = array_to_slice u32 2 (mk_array u32 2 [ 1; 2 ]) in + let* s0 = slice_update_usize u32 s 0 1 in + let* _ = array_from_slice u32 2 (mk_array u32 2 [ 1; 2 ]) s0 in Return () (** [array::f1]: forward function *) -let f1_fwd : result unit = - let* _ = array_index_mut_back u32 2 (mk_array u32 2 [ 1; 2 ]) 0 1 in - Return () +let f1 : result unit = + let* _ = array_update_usize u32 2 (mk_array u32 2 [ 1; 2 ]) 0 1 in Return () (** [array::f2]: forward function *) -let f2_fwd (i : u32) : result unit = +let f2 (i : u32) : result unit = Return () (** [array::f4]: forward function *) -let f4_fwd (x : array u32 32) (y : usize) (z : usize) : result (slice u32) = - array_subslice_shared u32 32 x (Mkrange y z) +let f4 (x : array u32 32) (y : usize) (z : usize) : result (slice u32) = + core_array_Array_index u32 (core_ops_range_Range usize) 32 + (core_slice_index_Slice_coreopsindexIndexInst u32 (core_ops_range_Range + usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x + { start = y; end_ = z } (** [array::f3]: forward function *) -let f3_fwd : result u32 = - let* i = array_index_shared u32 2 (mk_array u32 2 [ 1; 2 ]) 0 in - let* _ = f2_fwd i in - let* s = array_to_slice_shared u32 2 (mk_array u32 2 [ 1; 2 ]) in - let* s0 = - f4_fwd - (mk_array u32 32 [ - 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; - 0; 0; 0; 0; 0; 0; 0; 0 - ]) 16 18 in - sum2_fwd s s0 +let f3 : result u32 = + let* i = array_index_usize u32 2 (mk_array u32 2 [ 1; 2 ]) 0 in + let* _ = f2 i in + let b = array_repeat u32 32 0 in + let* s = array_to_slice u32 2 (mk_array u32 2 [ 1; 2 ]) in + let* s0 = f4 b 16 18 in + sum2 s s0 (** [array::SZ] *) let sz_body : result usize = Return 32 let sz_c : usize = eval_global sz_body (** [array::f5]: forward function *) -let f5_fwd (x : array u32 32) : result u32 = - array_index_shared u32 32 x 0 +let f5 (x : array u32 32) : result u32 = + array_index_usize u32 32 x 0 (** [array::ite]: forward function *) -let ite_fwd : result unit = - let* s = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in - let* s0 = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in +let ite : result unit = + let* s = array_to_slice u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* s0 = array_to_slice u32 2 (mk_array u32 2 [ 0; 0 ]) in let* s1 = index_mut_slice_u32_0_back s0 in - let* _ = array_to_slice_mut_back u32 2 (mk_array u32 2 [ 0; 0 ]) s1 in + let* _ = array_from_slice u32 2 (mk_array u32 2 [ 0; 0 ]) s1 in let* s2 = index_mut_slice_u32_0_back s in - let* _ = array_to_slice_mut_back u32 2 (mk_array u32 2 [ 0; 0 ]) s2 in + let* _ = array_from_slice u32 2 (mk_array u32 2 [ 0; 0 ]) s2 in Return () diff --git a/tests/fstar/array/Array.Types.fst b/tests/fstar/array/Array.Types.fst index 5e8e81d8..0ec9c12f 100644 --- a/tests/fstar/array/Array.Types.fst +++ b/tests/fstar/array/Array.Types.fst @@ -5,6 +5,6 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [array::T] *) -type t_t = | TA : t_t | TB : t_t +(** [array::AB] *) +type ab_t = | ABA : ab_t | ABB : ab_t -- cgit v1.3.1 From 9df1d191cfaf929b755e9d26d55811531acd939d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 11:21:53 +0100 Subject: Fix a small issue in AssociatedTypes --- compiler/AssociatedTypes.ml | 2 +- compiler/Config.ml | 6 +++--- compiler/Driver.ml | 8 +++++++- compiler/Extract.ml | 4 ++-- compiler/ExtractBase.ml | 12 ++++++------ compiler/ExtractTypes.ml | 2 +- compiler/Logging.ml | 2 +- 7 files changed, 21 insertions(+), 15 deletions(-) (limited to 'compiler/Driver.ml') diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index e4015903..581e218c 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -451,7 +451,7 @@ and ctx_normalize_trait_instance_id : | None -> (* This is actually a local clause *) assert (trait_instance_id_is_local_clause inst_id); - (ParentClause (inst_id, decl_id, clause_id), None) + (ItemClause (inst_id, decl_id, item_name, clause_id), None) | Some impl -> (* We figure out the item clause by doing the following: {[ diff --git a/compiler/Config.ml b/compiler/Config.ml index cd0903b6..8483c879 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -333,6 +333,6 @@ let parameterize_trait_types = ref false *) let type_check_pure_code = ref false -(** Shall we fail hard if there is an issue at code-generation time? - We may not want in case outputting a code with holes helps debugging *) -let extract_fail_hard = ref false +(** Shall we fail hard if we encounter an issue, or should we attempt to go + as far as possible while leaving "holes" in the generated code? *) +let fail_hard = ref true diff --git a/compiler/Driver.ml b/compiler/Driver.ml index b660b5a5..14668632 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -41,7 +41,7 @@ let _ = pure_utils_log#set_level EL.Info; symbolic_to_pure_log#set_level EL.Info; pure_micro_passes_log#set_level EL.Info; - pure_to_extract_log#set_level EL.Info; + extract_log#set_level EL.Info; translate_log#set_level EL.Info; scc_log#set_level EL.Info; reorder_decls_log#set_level EL.Info @@ -66,6 +66,9 @@ let () = (* Read the command line arguments *) let dest_dir = ref "" in + (* Print the imported llbc *) + let print_llbc = ref false in + let spec = [ ( "-backend", @@ -118,6 +121,8 @@ let () = ( "-lean-default-lakefile", Arg.Clear lean_gen_lakefile, " Generate a default lakefile.lean (Lean only)" ); + ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC"); + ("-k", Arg.Clear fail_hard, " Do not fail hard in case of error"); ] in @@ -131,6 +136,7 @@ let () = in if !extract_template_decreases_clauses then extract_decreases_clauses := true; + if !print_llbc then main_log#set_level EL.Debug; (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *) assert (!extract_decreases_clauses || not !extract_template_decreases_clauses); diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 8ad8a18d..b8cb38bb 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -472,7 +472,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) | Error (types, err) -> extract_generic_args ctx fmt TypeDeclId.Set.empty { generics with types }; - if !Config.extract_fail_hard then raise (Failure err) + if !Config.fail_hard then raise (Failure err) else F.pp_print_string fmt "(\"ERROR: ill-formed builtin: invalid number of filtering \ @@ -1992,7 +1992,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx) trans_fun.back_id in log#serror err; - if !Config.extract_fail_hard then raise (Failure err) + if !Config.fail_hard then raise (Failure err) else (trans_fun.back_id, "%ERROR_BUILTIN_NAME_NOT_FOUND%") in let rg_with_name_list = List.map find trans_funs in diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 8ddb2ec6..55b1bca3 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -8,7 +8,7 @@ module F = Format open ExtractBuiltin (** The local logger *) -let log = L.pure_to_extract_log +let log = L.extract_log type region_group_info = { id : RegionGroupId.id; @@ -488,7 +488,7 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id) in log#serror err; (* If we fail hard on errors, raise an exception *) - if !Config.extract_fail_hard then raise (Failure err) + if !Config.fail_hard then raise (Failure err) let names_map_get_id_from_name (name : string) (nm : names_map) : id option = StringMap.find_opt name nm.name_to_id @@ -522,7 +522,7 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string) in log#serror err; (* If we fail hard on errors, raise an exception *) - if !Config.extract_fail_hard then raise (Failure err)); + if !Config.fail_hard then raise (Failure err)); (* Insert *) names_map_add_unchecked id name nm @@ -691,7 +691,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | FunId (Assumed aid) -> A.show_assumed_fun_id aid | TraitMethod (trait_ref, method_name, _) -> (* Shouldn't happen *) - if !Config.extract_fail_hard then raise (Failure "Unexpected") + if !Config.fail_hard then raise (Failure "Unexpected") else "Trait method: decl: " ^ TraitDeclId.to_string trait_ref.trait_decl_ref.trait_decl_id @@ -903,7 +903,7 @@ let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) : ^ map_to_string m in log#serror err; - if !Config.extract_fail_hard then raise (Failure err) + if !Config.fail_hard then raise (Failure err) else "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)") else let m = nm.names_map.id_to_name in @@ -915,7 +915,7 @@ let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) : ^ map_to_string m in log#serror err; - if !Config.extract_fail_hard then raise (Failure err) + if !Config.fail_hard then raise (Failure err) else "(ERROR: \"" ^ id_to_string id ^ "\")" let ctx_get (id : id) (ctx : extraction_ctx) : string = diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 7bd02381..699a0e96 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1374,7 +1374,7 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter) | Self -> (* This has a specific treatment depending on the item we're extracting (associated type, etc.). We should have caught this elsewhere. *) - if !Config.extract_fail_hard then + if !Config.fail_hard then raise (Failure "Unexpected occurrence of `Self`") else F.pp_print_string fmt "ERROR(\"Unexpected Self\")" | TraitImpl id -> diff --git a/compiler/Logging.ml b/compiler/Logging.ml index 59abbfc7..721655b8 100644 --- a/compiler/Logging.ml +++ b/compiler/Logging.ml @@ -22,7 +22,7 @@ let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure" let pure_micro_passes_log = L.get_logger "MainLogger.PureMicroPasses" (** Logger for ExtractBase *) -let pure_to_extract_log = L.get_logger "MainLogger.ExtractBase" +let extract_log = L.get_logger "MainLogger.ExtractBase" (** Logger for Interpreter *) let interpreter_log = L.get_logger "MainLogger.Interpreter" -- cgit v1.3.1 From c57dec640d4e12c3dc66969d626bbbca2eb733fd Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 11:43:47 +0100 Subject: Modify some options and update the Makefile --- Makefile | 26 +- compiler/Config.ml | 4 +- compiler/Driver.ml | 14 +- tests/fstar/misc/Loops.fst | 784 +++++++++++++++++++++++++++++++++++++++++++ tests/lean/Array.lean | 436 +++++++++++++++++++++++- tests/lean/Loops.lean | 630 +++++++++++++++++++++++++++++++++- tests/lean/Loops/Funs.lean | 625 ---------------------------------- tests/lean/Loops/Types.lean | 13 - tests/lean/Traits.lean | 411 ++++++++++++++++++++++- tests/lean/Traits/Funs.lean | 275 --------------- tests/lean/Traits/Types.lean | 144 -------- 11 files changed, 2280 insertions(+), 1082 deletions(-) create mode 100644 tests/fstar/misc/Loops.fst delete mode 100644 tests/lean/Loops/Funs.lean delete mode 100644 tests/lean/Loops/Types.lean delete mode 100644 tests/lean/Traits/Funs.lean delete mode 100644 tests/lean/Traits/Types.lean (limited to 'compiler/Driver.ml') diff --git a/Makefile b/Makefile index bdabe878..19992442 100644 --- a/Makefile +++ b/Makefile @@ -115,7 +115,7 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA # Add specific options to some tests test-no_nested_borrows test-paper: \ - OPTIONS += -test-trans-units -no-split-files -no-state + OPTIONS += -test-trans-units test-no_nested_borrows test-paper: SUBDIR := misc tfstar-no_nested_borrows tfstar-paper: tlean-no_nested_borrows: SUBDIR := @@ -123,7 +123,7 @@ tlean-paper: SUBDIR := thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows thol4-paper: SUBDIR := misc-paper -test-array: OPTIONS += -no-state +test-array: OPTIONS += test-array: SUBDIR := array tfstar-array: OPTIONS += -decreases-clauses -template-clauses tcoq-array: OPTIONS += -use-fuel @@ -131,7 +131,7 @@ tlean-array: SUBDIR := tlean-array: OPTIONS += thol4-array: OPTIONS += -test-traits: OPTIONS += -no-state +test-traits: OPTIONS += test-traits: SUBDIR := traits tfstar-traits: OPTIONS += -decreases-clauses -template-clauses tcoq-traits: OPTIONS += -use-fuel @@ -147,15 +147,15 @@ thol4-array: thol4-traits: echo "Ignoring the traits test for HOL4" -test-loops: OPTIONS += -no-state +test-loops: OPTIONS += test-loops: SUBDIR := misc -tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -tcoq-loops: OPTIONS += -use-fuel -no-split-files +tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files +tcoq-loops: OPTIONS += -use-fuel tlean-loops: SUBDIR := thol4-loops: SUBDIR := misc-loops # TODO: reactivate -test-trans-units -test-hashmap: OPTIONS += -no-state +test-hashmap: OPTIONS += -split-files test-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel @@ -164,14 +164,14 @@ tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hash thol4-hashmap: OPTIONS += # TODO: reactivate -test-trans-units -test-hashmap_main: OPTIONS += +test-hashmap_main: OPTIONS += -state -split-files test-hashmap_main: SUBDIR := hashmap_on_disk tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap_main: OPTIONS += -use-fuel tlean-hashmap_main: SUBDIR := thol4-hashmap_main: OPTIONS += -testp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state +testp-polonius_list: OPTIONS += -test-trans-units testp-polonius_list: SUBDIR := misc tfstarp-polonius_list: OPTIONS += tcoqp-polonius_list: OPTIONS += @@ -180,7 +180,7 @@ tleanp-polonius_list: OPTIONS += thol4p-polonius_list: SUBDIR := misc-polonius_list thol4p-polonius_list: OPTIONS += -test-constants: OPTIONS += -test-trans-units -no-split-files -no-state +test-constants: OPTIONS += -test-trans-units test-constants: SUBDIR := misc tfstar-constants: OPTIONS += tcoq-constants: OPTIONS += @@ -189,7 +189,7 @@ tlean-constants: OPTIONS += thol4-constants: SUBDIR := misc-constants thol4-constants: OPTIONS += -test-external: OPTIONS += -test-trans-units +test-external: OPTIONS += -test-trans-units -state -split-files test-external: SUBDIR := misc tfstar-external: OPTIONS += tcoq-external: OPTIONS += @@ -199,7 +199,7 @@ thol4-external: SUBDIR := misc-external thol4-external: OPTIONS += BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units +testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files testp-betree_main: SUBDIR:=betree tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) tcoqp-betree_main: OPTIONS += -use-fuel @@ -211,7 +211,7 @@ thol4-betree_main: OPTIONS += # This generates very ugly code, but is good to test the translation. .PHONY: ctest-testp-betree_main ctest-testp-betree_main: testp-betree_main -ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units +ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) ctest-testp-betree_main: BACKEND_SUBDIR := "fstar" ctest-testp-betree_main: SUBDIR:=betree_back_stateful diff --git a/compiler/Config.ml b/compiler/Config.ml index 8483c879..a487f9e2 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -124,7 +124,7 @@ let always_deconstruct_adts_with_matches = ref false (** Controls whether we need to use a state to model the external world (I/O, for instance). *) -let use_state = ref true +let use_state = ref false (** Controls whether we use fuel to control termination. *) @@ -160,7 +160,7 @@ let backward_no_state_update = ref false files for the types, clauses and functions, or if we group them in one file. *) -let split_files = ref true +let split_files = ref false (** Generate the library entry point, if the crate is split between different files. diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 14668632..128ae890 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -93,9 +93,9 @@ let () = Arg.Set extract_decreases_clauses, " Use decreases clauses/termination measures for the recursive \ definitions" ); - ( "-no-state", - Arg.Clear use_state, - " Do not use state-error monads, simply use error monads" ); + ( "-state", + Arg.Set use_state, + " Use a *state*-error monads, instead of an error monads" ); ( "-use-fuel", Arg.Set use_fuel, " Use a fuel parameter to control divergence" ); @@ -106,10 +106,10 @@ let () = Arg.Set extract_template_decreases_clauses, " Generate templates for the required decreases clauses/termination \ measures, in a dedicated file. Implies -decreases-clauses" ); - ( "-no-split-files", - Arg.Clear split_files, - " Do not split the definitions between different files for types, \ - functions, etc." ); + ( "-split-files", + Arg.Set split_files, + " Split the definitions between different files for types, functions, \ + etc." ); ( "-no-check-inv", Arg.Clear check_invariants, " Deactivate the invariant sanity checks performed at every evaluation \ diff --git a/tests/fstar/misc/Loops.fst b/tests/fstar/misc/Loops.fst new file mode 100644 index 00000000..823acdd4 --- /dev/null +++ b/tests/fstar/misc/Loops.fst @@ -0,0 +1,784 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [loops] *) +module Loops +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [loops::sum]: decreases clause *) +unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () + +(** [loops::sum]: loop 0: forward function *) +let rec sum_loop + (max : u32) (i : u32) (s : u32) : + Tot (result u32) (decreases (sum_loop_decreases max i s)) + = + if i < max + then let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop max i0 s0 + else u32_mul s 2 + +(** [loops::sum]: forward function *) +let sum (max : u32) : result u32 = + sum_loop max 0 0 + +(** [loops::sum_with_mut_borrows]: decreases clause *) +unfold +let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat + = + admit () + +(** [loops::sum_with_mut_borrows]: loop 0: forward function *) +let rec sum_with_mut_borrows_loop + (max : u32) (mi : u32) (ms : u32) : + Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms)) + = + if mi < max + then + let* ms0 = u32_add ms mi in + let* mi0 = u32_add mi 1 in + sum_with_mut_borrows_loop max mi0 ms0 + else u32_mul ms 2 + +(** [loops::sum_with_mut_borrows]: forward function *) +let sum_with_mut_borrows (max : u32) : result u32 = + sum_with_mut_borrows_loop max 0 0 + +(** [loops::sum_with_shared_borrows]: decreases clause *) +unfold +let sum_with_shared_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : + nat = + admit () + +(** [loops::sum_with_shared_borrows]: loop 0: forward function *) +let rec sum_with_shared_borrows_loop + (max : u32) (i : u32) (s : u32) : + Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s)) + = + if i < max + then + let* i0 = u32_add i 1 in + let* s0 = u32_add s i0 in + sum_with_shared_borrows_loop max i0 s0 + else u32_mul s 2 + +(** [loops::sum_with_shared_borrows]: forward function *) +let sum_with_shared_borrows (max : u32) : result u32 = + sum_with_shared_borrows_loop max 0 0 + +(** [loops::clear]: decreases clause *) +unfold +let clear_loop_decreases (v : alloc_vec_Vec u32) (i : usize) : nat = admit () + +(** [loops::clear]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +let rec clear_loop + (v : alloc_vec_Vec u32) (i : usize) : + Tot (result (alloc_vec_Vec u32)) (decreases (clear_loop_decreases v i)) + = + let i0 = alloc_vec_Vec_len u32 v in + if i < i0 + then + let* i1 = usize_add i 1 in + let* v0 = + alloc_vec_Vec_index_mut_back u32 usize + (core_slice_index_usize_coresliceindexSliceIndexInst u32) v i 0 in + clear_loop v0 i1 + else Return v + +(** [loops::clear]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +let clear (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) = + clear_loop v 0 + +(** [loops::List] *) +type list_t (t : Type0) = +| List_Cons : t -> list_t t -> list_t t +| List_Nil : list_t t + +(** [loops::list_mem]: decreases clause *) +unfold let list_mem_loop_decreases (x : u32) (ls : list_t u32) : nat = admit () + +(** [loops::list_mem]: loop 0: forward function *) +let rec list_mem_loop + (x : u32) (ls : list_t u32) : + Tot (result bool) (decreases (list_mem_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> if y = x then Return true else list_mem_loop x tl + | List_Nil -> Return false + end + +(** [loops::list_mem]: forward function *) +let list_mem (x : u32) (ls : list_t u32) : result bool = + list_mem_loop x ls + +(** [loops::list_nth_mut_loop]: decreases clause *) +unfold +let list_nth_mut_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : + nat = + admit () + +(** [loops::list_nth_mut_loop]: loop 0: forward function *) +let rec list_nth_mut_loop_loop + (t : Type0) (ls : list_t t) (i : u32) : + Tot (result t) (decreases (list_nth_mut_loop_loop_decreases t ls i)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return x + else let* i0 = u32_sub i 1 in list_nth_mut_loop_loop t tl i0 + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop]: forward function *) +let list_nth_mut_loop (t : Type0) (ls : list_t t) (i : u32) : result t = + list_nth_mut_loop_loop t ls i + +(** [loops::list_nth_mut_loop]: loop 0: backward function 0 *) +let rec list_nth_mut_loop_loop_back + (t : Type0) (ls : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) (decreases (list_nth_mut_loop_loop_decreases t ls i)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return (List_Cons ret tl) + else + let* i0 = u32_sub i 1 in + let* tl0 = list_nth_mut_loop_loop_back t tl i0 ret in + Return (List_Cons x tl0) + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop]: backward function 0 *) +let list_nth_mut_loop_back + (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = + list_nth_mut_loop_loop_back t ls i ret + +(** [loops::list_nth_shared_loop]: decreases clause *) +unfold +let list_nth_shared_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : + nat = + admit () + +(** [loops::list_nth_shared_loop]: loop 0: forward function *) +let rec list_nth_shared_loop_loop + (t : Type0) (ls : list_t t) (i : u32) : + Tot (result t) (decreases (list_nth_shared_loop_loop_decreases t ls i)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return x + else let* i0 = u32_sub i 1 in list_nth_shared_loop_loop t tl i0 + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_loop]: forward function *) +let list_nth_shared_loop (t : Type0) (ls : list_t t) (i : u32) : result t = + list_nth_shared_loop_loop t ls i + +(** [loops::get_elem_mut]: decreases clause *) +unfold +let get_elem_mut_loop_decreases (x : usize) (ls : list_t usize) : nat = + admit () + +(** [loops::get_elem_mut]: loop 0: forward function *) +let rec get_elem_mut_loop + (x : usize) (ls : list_t usize) : + Tot (result usize) (decreases (get_elem_mut_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> if y = x then Return y else get_elem_mut_loop x tl + | List_Nil -> Fail Failure + end + +(** [loops::get_elem_mut]: forward function *) +let get_elem_mut + (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = + let* l = + alloc_vec_Vec_index_mut (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) + slots 0 in + get_elem_mut_loop x l + +(** [loops::get_elem_mut]: loop 0: backward function 0 *) +let rec get_elem_mut_loop_back + (x : usize) (ls : list_t usize) (ret : usize) : + Tot (result (list_t usize)) (decreases (get_elem_mut_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> + if y = x + then Return (List_Cons ret tl) + else let* tl0 = get_elem_mut_loop_back x tl ret in Return (List_Cons y tl0) + | List_Nil -> Fail Failure + end + +(** [loops::get_elem_mut]: backward function 0 *) +let get_elem_mut_back + (slots : alloc_vec_Vec (list_t usize)) (x : usize) (ret : usize) : + result (alloc_vec_Vec (list_t usize)) + = + let* l = + alloc_vec_Vec_index_mut (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) + slots 0 in + let* l0 = get_elem_mut_loop_back x l ret in + alloc_vec_Vec_index_mut_back (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) slots + 0 l0 + +(** [loops::get_elem_shared]: decreases clause *) +unfold +let get_elem_shared_loop_decreases (x : usize) (ls : list_t usize) : nat = + admit () + +(** [loops::get_elem_shared]: loop 0: forward function *) +let rec get_elem_shared_loop + (x : usize) (ls : list_t usize) : + Tot (result usize) (decreases (get_elem_shared_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> if y = x then Return y else get_elem_shared_loop x tl + | List_Nil -> Fail Failure + end + +(** [loops::get_elem_shared]: forward function *) +let get_elem_shared + (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = + let* l = + alloc_vec_Vec_index (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) + slots 0 in + get_elem_shared_loop x l + +(** [loops::id_mut]: forward function *) +let id_mut (t : Type0) (ls : list_t t) : result (list_t t) = + Return ls + +(** [loops::id_mut]: backward function 0 *) +let id_mut_back + (t : Type0) (ls : list_t t) (ret : list_t t) : result (list_t t) = + Return ret + +(** [loops::id_shared]: forward function *) +let id_shared (t : Type0) (ls : list_t t) : result (list_t t) = + Return ls + +(** [loops::list_nth_mut_loop_with_id]: decreases clause *) +unfold +let list_nth_mut_loop_with_id_loop_decreases (t : Type0) (i : u32) + (ls : list_t t) : nat = + admit () + +(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *) +let rec list_nth_mut_loop_with_id_loop + (t : Type0) (i : u32) (ls : list_t t) : + Tot (result t) (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return x + else let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop t i0 tl + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_with_id]: forward function *) +let list_nth_mut_loop_with_id + (t : Type0) (ls : list_t t) (i : u32) : result t = + let* ls0 = id_mut t ls in list_nth_mut_loop_with_id_loop t i ls0 + +(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *) +let rec list_nth_mut_loop_with_id_loop_back + (t : Type0) (i : u32) (ls : list_t t) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return (List_Cons ret tl) + else + let* i0 = u32_sub i 1 in + let* tl0 = list_nth_mut_loop_with_id_loop_back t i0 tl ret in + Return (List_Cons x tl0) + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_with_id]: backward function 0 *) +let list_nth_mut_loop_with_id_back + (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = + let* ls0 = id_mut t ls in + let* l = list_nth_mut_loop_with_id_loop_back t i ls0 ret in + id_mut_back t ls l + +(** [loops::list_nth_shared_loop_with_id]: decreases clause *) +unfold +let list_nth_shared_loop_with_id_loop_decreases (t : Type0) (i : u32) + (ls : list_t t) : nat = + admit () + +(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *) +let rec list_nth_shared_loop_with_id_loop + (t : Type0) (i : u32) (ls : list_t t) : + Tot (result t) + (decreases (list_nth_shared_loop_with_id_loop_decreases t i ls)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return x + else let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop t i0 tl + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_loop_with_id]: forward function *) +let list_nth_shared_loop_with_id + (t : Type0) (ls : list_t t) (i : u32) : result t = + let* ls0 = id_shared t ls in list_nth_shared_loop_with_id_loop t i ls0 + +(** [loops::list_nth_mut_loop_pair]: decreases clause *) +unfold +let list_nth_mut_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_loop_pair]: loop 0: forward function *) +let rec list_nth_mut_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_pair]: forward function *) +let list_nth_mut_loop_pair + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_mut_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *) +let rec list_nth_mut_loop_pair_loop_back'a + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl0) + else + let* i0 = u32_sub i 1 in + let* tl00 = list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret in + Return (List_Cons x0 tl00) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_pair]: backward function 0 *) +let list_nth_mut_loop_pair_back'a + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_mut_loop_pair_loop_back'a t ls0 ls1 i ret + +(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 *) +let rec list_nth_mut_loop_pair_loop_back'b + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl1) + else + let* i0 = u32_sub i 1 in + let* tl10 = list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret in + Return (List_Cons x1 tl10) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_pair]: backward function 1 *) +let list_nth_mut_loop_pair_back'b + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret + +(** [loops::list_nth_shared_loop_pair]: decreases clause *) +unfold +let list_nth_shared_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_loop_pair]: loop 0: forward function *) +let rec list_nth_shared_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_shared_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else let* i0 = u32_sub i 1 in list_nth_shared_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_loop_pair]: forward function *) +let list_nth_shared_loop_pair + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_mut_loop_pair_merge]: decreases clause *) +unfold +let list_nth_mut_loop_pair_merge_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *) +let rec list_nth_mut_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_pair_merge]: forward function *) +let list_nth_mut_loop_pair_merge + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_mut_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *) +let rec list_nth_mut_loop_pair_merge_loop_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) : + Tot (result ((list_t t) & (list_t t))) + (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1) + else + let* i0 = u32_sub i 1 in + let* (tl00, tl10) = + list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in + Return (List_Cons x0 tl00, List_Cons x1 tl10) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *) +let list_nth_mut_loop_pair_merge_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) : + result ((list_t t) & (list_t t)) + = + list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret + +(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *) +unfold +let list_nth_shared_loop_pair_merge_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *) +let rec list_nth_shared_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in + list_nth_shared_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_loop_pair_merge]: forward function *) +let list_nth_shared_loop_pair_merge + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *) +unfold +let list_nth_mut_shared_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *) +let rec list_nth_mut_shared_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in + list_nth_mut_shared_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair]: forward function *) +let list_nth_mut_shared_loop_pair + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_mut_shared_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *) +let rec list_nth_mut_shared_loop_pair_loop_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl0) + else + let* i0 = u32_sub i 1 in + let* tl00 = list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret in + Return (List_Cons x0 tl00) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *) +let list_nth_mut_shared_loop_pair_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_mut_shared_loop_pair_loop_back t ls0 ls1 i ret + +(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *) +unfold +let list_nth_mut_shared_loop_pair_merge_loop_decreases (t : Type0) + (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *) +let rec list_nth_mut_shared_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in + list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *) +let list_nth_mut_shared_loop_pair_merge + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *) +let rec list_nth_mut_shared_loop_pair_merge_loop_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl0) + else + let* i0 = u32_sub i 1 in + let* tl00 = + list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret in + Return (List_Cons x0 tl00) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *) +let list_nth_mut_shared_loop_pair_merge_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_mut_shared_loop_pair_merge_loop_back t ls0 ls1 i ret + +(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *) +unfold +let list_nth_shared_mut_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *) +let rec list_nth_shared_mut_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in + list_nth_shared_mut_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair]: forward function *) +let list_nth_shared_mut_loop_pair + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_mut_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *) +let rec list_nth_shared_mut_loop_pair_loop_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl1) + else + let* i0 = u32_sub i 1 in + let* tl10 = list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret in + Return (List_Cons x1 tl10) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *) +let list_nth_shared_mut_loop_pair_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_shared_mut_loop_pair_loop_back t ls0 ls1 i ret + +(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *) +unfold +let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0) + (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *) +let rec list_nth_shared_mut_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in + list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *) +let list_nth_shared_mut_loop_pair_merge + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *) +let rec list_nth_shared_mut_loop_pair_merge_loop_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl1) + else + let* i0 = u32_sub i 1 in + let* tl10 = + list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in + Return (List_Cons x1 tl10) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *) +let list_nth_shared_mut_loop_pair_merge_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_shared_mut_loop_pair_merge_loop_back t ls0 ls1 i ret + diff --git a/tests/lean/Array.lean b/tests/lean/Array.lean index 277b63d9..20f02e97 100644 --- a/tests/lean/Array.lean +++ b/tests/lean/Array.lean @@ -1 +1,435 @@ -import Array.Funs +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [array] +import Base +open Primitives + +namespace array + +/- [array::AB] -/ +inductive AB := +| A : AB +| B : AB + +/- [array::incr]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def incr (x : U32) : Result U32 := + x + 1#u32 + +/- [array::array_to_shared_slice_]: forward function -/ +def array_to_shared_slice_ + (T : Type) (s : Array T 32#usize) : Result (Slice T) := + Array.to_slice T 32#usize s + +/- [array::array_to_mut_slice_]: forward function -/ +def array_to_mut_slice_ (T : Type) (s : Array T 32#usize) : Result (Slice T) := + Array.to_slice T 32#usize s + +/- [array::array_to_mut_slice_]: backward function 0 -/ +def array_to_mut_slice__back + (T : Type) (s : Array T 32#usize) (ret0 : Slice T) : + Result (Array T 32#usize) + := + Array.from_slice T 32#usize s ret0 + +/- [array::array_len]: forward function -/ +def array_len (T : Type) (s : Array T 32#usize) : Result Usize := + do + let s0 ← Array.to_slice T 32#usize s + let i := Slice.len T s0 + Result.ret i + +/- [array::shared_array_len]: forward function -/ +def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize := + do + let s0 ← Array.to_slice T 32#usize s + let i := Slice.len T s0 + Result.ret i + +/- [array::shared_slice_len]: forward function -/ +def shared_slice_len (T : Type) (s : Slice T) : Result Usize := + let i := Slice.len T s + Result.ret i + +/- [array::index_array_shared]: forward function -/ +def index_array_shared + (T : Type) (s : Array T 32#usize) (i : Usize) : Result T := + Array.index_usize T 32#usize s i + +/- [array::index_array_u32]: forward function -/ +def index_array_u32 (s : Array U32 32#usize) (i : Usize) : Result U32 := + Array.index_usize U32 32#usize s i + +/- [array::index_array_copy]: forward function -/ +def index_array_copy (x : Array U32 32#usize) : Result U32 := + Array.index_usize U32 32#usize x 0#usize + +/- [array::index_mut_array]: forward function -/ +def index_mut_array (T : Type) (s : Array T 32#usize) (i : Usize) : Result T := + Array.index_usize T 32#usize s i + +/- [array::index_mut_array]: backward function 0 -/ +def index_mut_array_back + (T : Type) (s : Array T 32#usize) (i : Usize) (ret0 : T) : + Result (Array T 32#usize) + := + Array.update_usize T 32#usize s i ret0 + +/- [array::index_slice]: forward function -/ +def index_slice (T : Type) (s : Slice T) (i : Usize) : Result T := + Slice.index_usize T s i + +/- [array::index_mut_slice]: forward function -/ +def index_mut_slice (T : Type) (s : Slice T) (i : Usize) : Result T := + Slice.index_usize T s i + +/- [array::index_mut_slice]: backward function 0 -/ +def index_mut_slice_back + (T : Type) (s : Slice T) (i : Usize) (ret0 : T) : Result (Slice T) := + Slice.update_usize T s i ret0 + +/- [array::slice_subslice_shared_]: forward function -/ +def slice_subslice_shared_ + (x : Slice U32) (y : Usize) (z : Usize) : Result (Slice U32) := + core.slice.index.Slice.index U32 (core.ops.range.Range Usize) + (core.slice.index.Range.coresliceindexSliceIndexInst U32) x + { start := y, end_ := z } + +/- [array::slice_subslice_mut_]: forward function -/ +def slice_subslice_mut_ + (x : Slice U32) (y : Usize) (z : Usize) : Result (Slice U32) := + core.slice.index.Slice.index_mut U32 (core.ops.range.Range Usize) + (core.slice.index.Range.coresliceindexSliceIndexInst U32) x + { start := y, end_ := z } + +/- [array::slice_subslice_mut_]: backward function 0 -/ +def slice_subslice_mut__back + (x : Slice U32) (y : Usize) (z : Usize) (ret0 : Slice U32) : + Result (Slice U32) + := + core.slice.index.Slice.index_mut_back U32 (core.ops.range.Range Usize) + (core.slice.index.Range.coresliceindexSliceIndexInst U32) x + { start := y, end_ := z } ret0 + +/- [array::array_to_slice_shared_]: forward function -/ +def array_to_slice_shared_ (x : Array U32 32#usize) : Result (Slice U32) := + Array.to_slice U32 32#usize x + +/- [array::array_to_slice_mut_]: forward function -/ +def array_to_slice_mut_ (x : Array U32 32#usize) : Result (Slice U32) := + Array.to_slice U32 32#usize x + +/- [array::array_to_slice_mut_]: backward function 0 -/ +def array_to_slice_mut__back + (x : Array U32 32#usize) (ret0 : Slice U32) : Result (Array U32 32#usize) := + Array.from_slice U32 32#usize x ret0 + +/- [array::array_subslice_shared_]: forward function -/ +def array_subslice_shared_ + (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize + (core.slice.index.Slice.coreopsindexIndexInst U32 (core.ops.range.Range + Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x + { start := y, end_ := z } + +/- [array::array_subslice_mut_]: forward function -/ +def array_subslice_mut_ + (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32#usize + (core.slice.index.Slice.coreopsindexIndexMutInst U32 (core.ops.range.Range + Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x + { start := y, end_ := z } + +/- [array::array_subslice_mut_]: backward function 0 -/ +def array_subslice_mut__back + (x : Array U32 32#usize) (y : Usize) (z : Usize) (ret0 : Slice U32) : + Result (Array U32 32#usize) + := + core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 32#usize + (core.slice.index.Slice.coreopsindexIndexMutInst U32 (core.ops.range.Range + Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x + { start := y, end_ := z } ret0 + +/- [array::index_slice_0]: forward function -/ +def index_slice_0 (T : Type) (s : Slice T) : Result T := + Slice.index_usize T s 0#usize + +/- [array::index_array_0]: forward function -/ +def index_array_0 (T : Type) (s : Array T 32#usize) : Result T := + Array.index_usize T 32#usize s 0#usize + +/- [array::index_index_array]: forward function -/ +def index_index_array + (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : + Result U32 + := + do + let a ← Array.index_usize (Array U32 32#usize) 32#usize s i + Array.index_usize U32 32#usize a j + +/- [array::update_update_array]: forward function -/ +def update_update_array + (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : + Result Unit + := + do + let a ← Array.index_usize (Array U32 32#usize) 32#usize s i + let a0 ← Array.update_usize U32 32#usize a j 0#u32 + let _ ← Array.update_usize (Array U32 32#usize) 32#usize s i a0 + Result.ret () + +/- [array::array_local_deep_copy]: forward function -/ +def array_local_deep_copy (x : Array U32 32#usize) : Result Unit := + Result.ret () + +/- [array::take_array]: forward function -/ +def take_array (a : Array U32 2#usize) : Result Unit := + Result.ret () + +/- [array::take_array_borrow]: forward function -/ +def take_array_borrow (a : Array U32 2#usize) : Result Unit := + Result.ret () + +/- [array::take_slice]: forward function -/ +def take_slice (s : Slice U32) : Result Unit := + Result.ret () + +/- [array::take_mut_slice]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def take_mut_slice (s : Slice U32) : Result (Slice U32) := + Result.ret s + +/- [array::take_all]: forward function -/ +def take_all : Result Unit := + do + let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_slice s + let s0 ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s1 ← take_mut_slice s0 + let _ ← + Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1 + Result.ret () + +/- [array::index_array]: forward function -/ +def index_array (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize + +/- [array::index_array_borrow]: forward function -/ +def index_array_borrow (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize + +/- [array::index_slice_u32_0]: forward function -/ +def index_slice_u32_0 (x : Slice U32) : Result U32 := + Slice.index_usize U32 x 0#usize + +/- [array::index_mut_slice_u32_0]: forward function -/ +def index_mut_slice_u32_0 (x : Slice U32) : Result U32 := + Slice.index_usize U32 x 0#usize + +/- [array::index_mut_slice_u32_0]: backward function 0 -/ +def index_mut_slice_u32_0_back (x : Slice U32) : Result (Slice U32) := + do + let _ ← Slice.index_usize U32 x 0#usize + Result.ret x + +/- [array::index_all]: forward function -/ +def index_all : Result U32 := + do + let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i0 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i1 ← i + i0 + let i2 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i3 ← i1 + i2 + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i4 ← index_slice_u32_0 s + let i5 ← i3 + i4 + let s0 ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i6 ← index_mut_slice_u32_0 s0 + let i7 ← i5 + i6 + let s1 ← index_mut_slice_u32_0_back s0 + let _ ← + Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1 + Result.ret i7 + +/- [array::update_array]: forward function -/ +def update_array (x : Array U32 2#usize) : Result Unit := + do + let _ ← Array.update_usize U32 2#usize x 0#usize 1#u32 + Result.ret () + +/- [array::update_array_mut_borrow]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def update_array_mut_borrow + (x : Array U32 2#usize) : Result (Array U32 2#usize) := + Array.update_usize U32 2#usize x 0#usize 1#u32 + +/- [array::update_mut_slice]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def update_mut_slice (x : Slice U32) : Result (Slice U32) := + Slice.update_usize U32 x 0#usize 1#u32 + +/- [array::update_all]: forward function -/ +def update_all : Result Unit := + do + let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s ← Array.to_slice U32 2#usize x + let s0 ← update_mut_slice s + let _ ← Array.from_slice U32 2#usize x s0 + Result.ret () + +/- [array::range_all]: forward function -/ +def range_all : Result Unit := + do + let s ← + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4#usize + (core.slice.index.Slice.coreopsindexIndexMutInst U32 + (core.ops.range.Range Usize) + (core.slice.index.Range.coresliceindexSliceIndexInst U32)) + (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ]) + { start := 1#usize, end_ := 3#usize } + let s0 ← update_mut_slice s + let _ ← + core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 4#usize + (core.slice.index.Slice.coreopsindexIndexMutInst U32 + (core.ops.range.Range Usize) + (core.slice.index.Range.coresliceindexSliceIndexInst U32)) + (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ]) + { start := 1#usize, end_ := 3#usize } s0 + Result.ret () + +/- [array::deref_array_borrow]: forward function -/ +def deref_array_borrow (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize + +/- [array::deref_array_mut_borrow]: forward function -/ +def deref_array_mut_borrow (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize + +/- [array::deref_array_mut_borrow]: backward function 0 -/ +def deref_array_mut_borrow_back + (x : Array U32 2#usize) : Result (Array U32 2#usize) := + do + let _ ← Array.index_usize U32 2#usize x 0#usize + Result.ret x + +/- [array::take_array_t]: forward function -/ +def take_array_t (a : Array AB 2#usize) : Result Unit := + Result.ret () + +/- [array::non_copyable_array]: forward function -/ +def non_copyable_array : Result Unit := + do + let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) + Result.ret () + +/- [array::sum]: loop 0: forward function -/ +divergent def sum_loop (s : Slice U32) (sum0 : U32) (i : Usize) : Result U32 := + let i0 := Slice.len U32 s + if i < i0 + then + do + let i1 ← Slice.index_usize U32 s i + let sum1 ← sum0 + i1 + let i2 ← i + 1#usize + sum_loop s sum1 i2 + else Result.ret sum0 + +/- [array::sum]: forward function -/ +def sum (s : Slice U32) : Result U32 := + sum_loop s 0#u32 0#usize + +/- [array::sum2]: loop 0: forward function -/ +divergent def sum2_loop + (s : Slice U32) (s2 : Slice U32) (sum0 : U32) (i : Usize) : Result U32 := + let i0 := Slice.len U32 s + if i < i0 + then + do + let i1 ← Slice.index_usize U32 s i + let i2 ← Slice.index_usize U32 s2 i + let i3 ← i1 + i2 + let sum1 ← sum0 + i3 + let i4 ← i + 1#usize + sum2_loop s s2 sum1 i4 + else Result.ret sum0 + +/- [array::sum2]: forward function -/ +def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 := + let i := Slice.len U32 s + let i0 := Slice.len U32 s2 + if not (i = i0) + then Result.fail Error.panic + else sum2_loop s s2 0#u32 0#usize + +/- [array::f0]: forward function -/ +def f0 : Result Unit := + do + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + let s0 ← Slice.update_usize U32 s 0#usize 1#u32 + let _ ← + Array.from_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) s0 + Result.ret () + +/- [array::f1]: forward function -/ +def f1 : Result Unit := + do + let _ ← + Array.update_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + 0#usize 1#u32 + Result.ret () + +/- [array::f2]: forward function -/ +def f2 (i : U32) : Result Unit := + Result.ret () + +/- [array::f4]: forward function -/ +def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize + (core.slice.index.Slice.coreopsindexIndexInst U32 (core.ops.range.Range + Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x + { start := y, end_ := z } + +/- [array::f3]: forward function -/ +def f3 : Result U32 := + do + let i ← + Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + 0#usize + let _ ← f2 i + let b := Array.repeat U32 32#usize 0#u32 + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + let s0 ← f4 b 16#usize 18#usize + sum2 s s0 + +/- [array::SZ] -/ +def sz_body : Result Usize := Result.ret 32#usize +def sz_c : Usize := eval_global sz_body (by simp) + +/- [array::f5]: forward function -/ +def f5 (x : Array U32 32#usize) : Result U32 := + Array.index_usize U32 32#usize x 0#usize + +/- [array::ite]: forward function -/ +def ite : Result Unit := + do + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s0 ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s1 ← index_mut_slice_u32_0_back s0 + let _ ← + Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1 + let s2 ← index_mut_slice_u32_0_back s + let _ ← + Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s2 + Result.ret () + +end array diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 60c73776..c6360338 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -1 +1,629 @@ -import Loops.Funs +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [loops] +import Base +open Primitives + +namespace loops + +/- [loops::sum]: loop 0: forward function -/ +divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 := + if i < max + then do + let s0 ← s + i + let i0 ← i + 1#u32 + sum_loop max i0 s0 + else s * 2#u32 + +/- [loops::sum]: forward function -/ +def sum (max : U32) : Result U32 := + sum_loop max 0#u32 0#u32 + +/- [loops::sum_with_mut_borrows]: loop 0: forward function -/ +divergent def sum_with_mut_borrows_loop + (max : U32) (mi : U32) (ms : U32) : Result U32 := + if mi < max + then + do + let ms0 ← ms + mi + let mi0 ← mi + 1#u32 + sum_with_mut_borrows_loop max mi0 ms0 + else ms * 2#u32 + +/- [loops::sum_with_mut_borrows]: forward function -/ +def sum_with_mut_borrows (max : U32) : Result U32 := + sum_with_mut_borrows_loop max 0#u32 0#u32 + +/- [loops::sum_with_shared_borrows]: loop 0: forward function -/ +divergent def sum_with_shared_borrows_loop + (max : U32) (i : U32) (s : U32) : Result U32 := + if i < max + then + do + let i0 ← i + 1#u32 + let s0 ← s + i0 + sum_with_shared_borrows_loop max i0 s0 + else s * 2#u32 + +/- [loops::sum_with_shared_borrows]: forward function -/ +def sum_with_shared_borrows (max : U32) : Result U32 := + sum_with_shared_borrows_loop max 0#u32 0#u32 + +/- [loops::clear]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +divergent def clear_loop + (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) := + let i0 := alloc.vec.Vec.len U32 v + if i < i0 + then + do + let i1 ← i + 1#usize + let v0 ← + alloc.vec.Vec.index_mut_back U32 Usize + (core.slice.index.usize.coresliceindexSliceIndexInst U32) v i 0#u32 + clear_loop v0 i1 + else Result.ret v + +/- [loops::clear]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := + clear_loop v 0#usize + +/- [loops::List] -/ +inductive List (T : Type) := +| Cons : T → List T → List T +| Nil : List T + +/- [loops::list_mem]: loop 0: forward function -/ +divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool := + match ls with + | List.Cons y tl => if y = x + then Result.ret true + else list_mem_loop x tl + | List.Nil => Result.ret false + +/- [loops::list_mem]: forward function -/ +def list_mem (x : U32) (ls : List U32) : Result Bool := + list_mem_loop x ls + +/- [loops::list_nth_mut_loop]: loop 0: forward function -/ +divergent def list_nth_mut_loop_loop + (T : Type) (ls : List T) (i : U32) : Result T := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret x + else do + let i0 ← i - 1#u32 + list_nth_mut_loop_loop T tl i0 + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop]: forward function -/ +def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T := + list_nth_mut_loop_loop T ls i + +/- [loops::list_nth_mut_loop]: loop 0: backward function 0 -/ +divergent def list_nth_mut_loop_loop_back + (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl) + else + do + let i0 ← i - 1#u32 + let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0 + Result.ret (List.Cons x tl0) + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop]: backward function 0 -/ +def list_nth_mut_loop_back + (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := + list_nth_mut_loop_loop_back T ls i ret0 + +/- [loops::list_nth_shared_loop]: loop 0: forward function -/ +divergent def list_nth_shared_loop_loop + (T : Type) (ls : List T) (i : U32) : Result T := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret x + else do + let i0 ← i - 1#u32 + list_nth_shared_loop_loop T tl i0 + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_loop]: forward function -/ +def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T := + list_nth_shared_loop_loop T ls i + +/- [loops::get_elem_mut]: loop 0: forward function -/ +divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize := + match ls with + | List.Cons y tl => if y = x + then Result.ret y + else get_elem_mut_loop x tl + | List.Nil => Result.fail Error.panic + +/- [loops::get_elem_mut]: forward function -/ +def get_elem_mut + (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := + do + let l ← + alloc.vec.Vec.index_mut (List Usize) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) + slots 0#usize + get_elem_mut_loop x l + +/- [loops::get_elem_mut]: loop 0: backward function 0 -/ +divergent def get_elem_mut_loop_back + (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) := + match ls with + | List.Cons y tl => + if y = x + then Result.ret (List.Cons ret0 tl) + else + do + let tl0 ← get_elem_mut_loop_back x tl ret0 + Result.ret (List.Cons y tl0) + | List.Nil => Result.fail Error.panic + +/- [loops::get_elem_mut]: backward function 0 -/ +def get_elem_mut_back + (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret0 : Usize) : + Result (alloc.vec.Vec (List Usize)) + := + do + let l ← + alloc.vec.Vec.index_mut (List Usize) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) + slots 0#usize + let l0 ← get_elem_mut_loop_back x l ret0 + alloc.vec.Vec.index_mut_back (List Usize) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) slots + 0#usize l0 + +/- [loops::get_elem_shared]: loop 0: forward function -/ +divergent def get_elem_shared_loop + (x : Usize) (ls : List Usize) : Result Usize := + match ls with + | List.Cons y tl => if y = x + then Result.ret y + else get_elem_shared_loop x tl + | List.Nil => Result.fail Error.panic + +/- [loops::get_elem_shared]: forward function -/ +def get_elem_shared + (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := + do + let l ← + alloc.vec.Vec.index (List Usize) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) + slots 0#usize + get_elem_shared_loop x l + +/- [loops::id_mut]: forward function -/ +def id_mut (T : Type) (ls : List T) : Result (List T) := + Result.ret ls + +/- [loops::id_mut]: backward function 0 -/ +def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) := + Result.ret ret0 + +/- [loops::id_shared]: forward function -/ +def id_shared (T : Type) (ls : List T) : Result (List T) := + Result.ret ls + +/- [loops::list_nth_mut_loop_with_id]: loop 0: forward function -/ +divergent def list_nth_mut_loop_with_id_loop + (T : Type) (i : U32) (ls : List T) : Result T := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret x + else do + let i0 ← i - 1#u32 + list_nth_mut_loop_with_id_loop T i0 tl + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_with_id]: forward function -/ +def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T := + do + let ls0 ← id_mut T ls + list_nth_mut_loop_with_id_loop T i ls0 + +/- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 -/ +divergent def list_nth_mut_loop_with_id_loop_back + (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl) + else + do + let i0 ← i - 1#u32 + let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0 + Result.ret (List.Cons x tl0) + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_with_id]: backward function 0 -/ +def list_nth_mut_loop_with_id_back + (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := + do + let ls0 ← id_mut T ls + let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret0 + id_mut_back T ls l + +/- [loops::list_nth_shared_loop_with_id]: loop 0: forward function -/ +divergent def list_nth_shared_loop_with_id_loop + (T : Type) (i : U32) (ls : List T) : Result T := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret x + else do + let i0 ← i - 1#u32 + list_nth_shared_loop_with_id_loop T i0 tl + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_loop_with_id]: forward function -/ +def list_nth_shared_loop_with_id + (T : Type) (ls : List T) (i : U32) : Result T := + do + let ls0 ← id_shared T ls + list_nth_shared_loop_with_id_loop T i ls0 + +/- [loops::list_nth_mut_loop_pair]: loop 0: forward function -/ +divergent def list_nth_mut_loop_pair_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else do + let i0 ← i - 1#u32 + list_nth_mut_loop_pair_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_pair]: forward function -/ +def list_nth_mut_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_mut_loop_pair_loop T ls0 ls1 i + +/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 -/ +divergent def list_nth_mut_loop_pair_loop_back'a + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl0) + else + do + let i0 ← i - 1#u32 + let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0 + Result.ret (List.Cons x0 tl00) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_pair]: backward function 0 -/ +def list_nth_mut_loop_pair_back'a + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0 + +/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 -/ +divergent def list_nth_mut_loop_pair_loop_back'b + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl1) + else + do + let i0 ← i - 1#u32 + let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0 + Result.ret (List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_pair]: backward function 1 -/ +def list_nth_mut_loop_pair_back'b + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0 + +/- [loops::list_nth_shared_loop_pair]: loop 0: forward function -/ +divergent def list_nth_shared_loop_pair_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else do + let i0 ← i - 1#u32 + list_nth_shared_loop_pair_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_loop_pair]: forward function -/ +def list_nth_shared_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_shared_loop_pair_loop T ls0 ls1 i + +/- [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function -/ +divergent def list_nth_mut_loop_pair_merge_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_pair_merge]: forward function -/ +def list_nth_mut_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_mut_loop_pair_merge_loop T ls0 ls1 i + +/- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 -/ +divergent def list_nth_mut_loop_pair_merge_loop_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : + Result ((List T) × (List T)) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then let (t, t0) := ret0 + Result.ret (List.Cons t tl0, List.Cons t0 tl1) + else + do + let i0 ← i - 1#u32 + let (tl00, tl10) ← + list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 + Result.ret (List.Cons x0 tl00, List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_pair_merge]: backward function 0 -/ +def list_nth_mut_loop_pair_merge_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : + Result ((List T) × (List T)) + := + list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 + +/- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function -/ +divergent def list_nth_shared_loop_pair_merge_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_loop_pair_merge]: forward function -/ +def list_nth_shared_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_shared_loop_pair_merge_loop T ls0 ls1 i + +/- [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function -/ +divergent def list_nth_mut_shared_loop_pair_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_shared_loop_pair]: forward function -/ +def list_nth_mut_shared_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_mut_shared_loop_pair_loop T ls0 ls1 i + +/- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 -/ +divergent def list_nth_mut_shared_loop_pair_loop_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl0) + else + do + let i0 ← i - 1#u32 + let tl00 ← + list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0 + Result.ret (List.Cons x0 tl00) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_shared_loop_pair]: backward function 0 -/ +def list_nth_mut_shared_loop_pair_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0 + +/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function -/ +divergent def list_nth_mut_shared_loop_pair_merge_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_shared_loop_pair_merge]: forward function -/ +def list_nth_mut_shared_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i + +/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 -/ +divergent def list_nth_mut_shared_loop_pair_merge_loop_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl0) + else + do + let i0 ← i - 1#u32 + let tl00 ← + list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 + Result.ret (List.Cons x0 tl00) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 -/ +def list_nth_mut_shared_loop_pair_merge_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0 + +/- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function -/ +divergent def list_nth_shared_mut_loop_pair_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_mut_loop_pair]: forward function -/ +def list_nth_shared_mut_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_shared_mut_loop_pair_loop T ls0 ls1 i + +/- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 -/ +divergent def list_nth_shared_mut_loop_pair_loop_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl1) + else + do + let i0 ← i - 1#u32 + let tl10 ← + list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0 + Result.ret (List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_mut_loop_pair]: backward function 1 -/ +def list_nth_shared_mut_loop_pair_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0 + +/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function -/ +divergent def list_nth_shared_mut_loop_pair_merge_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_mut_loop_pair_merge]: forward function -/ +def list_nth_shared_mut_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i + +/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 -/ +divergent def list_nth_shared_mut_loop_pair_merge_loop_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl1) + else + do + let i0 ← i - 1#u32 + let tl10 ← + list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 + Result.ret (List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 -/ +def list_nth_shared_mut_loop_pair_merge_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 + +end loops diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean deleted file mode 100644 index f9c7569e..00000000 --- a/tests/lean/Loops/Funs.lean +++ /dev/null @@ -1,625 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [loops]: function definitions -import Base -import Loops.Types -open Primitives - -namespace loops - -/- [loops::sum]: loop 0: forward function -/ -divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 := - if i < max - then do - let s0 ← s + i - let i0 ← i + 1#u32 - sum_loop max i0 s0 - else s * 2#u32 - -/- [loops::sum]: forward function -/ -def sum (max : U32) : Result U32 := - sum_loop max 0#u32 0#u32 - -/- [loops::sum_with_mut_borrows]: loop 0: forward function -/ -divergent def sum_with_mut_borrows_loop - (max : U32) (mi : U32) (ms : U32) : Result U32 := - if mi < max - then - do - let ms0 ← ms + mi - let mi0 ← mi + 1#u32 - sum_with_mut_borrows_loop max mi0 ms0 - else ms * 2#u32 - -/- [loops::sum_with_mut_borrows]: forward function -/ -def sum_with_mut_borrows (max : U32) : Result U32 := - sum_with_mut_borrows_loop max 0#u32 0#u32 - -/- [loops::sum_with_shared_borrows]: loop 0: forward function -/ -divergent def sum_with_shared_borrows_loop - (max : U32) (i : U32) (s : U32) : Result U32 := - if i < max - then - do - let i0 ← i + 1#u32 - let s0 ← s + i0 - sum_with_shared_borrows_loop max i0 s0 - else s * 2#u32 - -/- [loops::sum_with_shared_borrows]: forward function -/ -def sum_with_shared_borrows (max : U32) : Result U32 := - sum_with_shared_borrows_loop max 0#u32 0#u32 - -/- [loops::clear]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) -/ -divergent def clear_loop - (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) := - let i0 := alloc.vec.Vec.len U32 v - if i < i0 - then - do - let i1 ← i + 1#usize - let v0 ← - alloc.vec.Vec.index_mut_back U32 Usize - (core.slice.index.usize.coresliceindexSliceIndexInst U32) v i 0#u32 - clear_loop v0 i1 - else Result.ret v - -/- [loops::clear]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) -/ -def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := - clear_loop v 0#usize - -/- [loops::list_mem]: loop 0: forward function -/ -divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool := - match ls with - | List.Cons y tl => if y = x - then Result.ret true - else list_mem_loop x tl - | List.Nil => Result.ret false - -/- [loops::list_mem]: forward function -/ -def list_mem (x : U32) (ls : List U32) : Result Bool := - list_mem_loop x ls - -/- [loops::list_nth_mut_loop]: loop 0: forward function -/ -divergent def list_nth_mut_loop_loop - (T : Type) (ls : List T) (i : U32) : Result T := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_mut_loop_loop T tl i0 - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop]: forward function -/ -def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T := - list_nth_mut_loop_loop T ls i - -/- [loops::list_nth_mut_loop]: loop 0: backward function 0 -/ -divergent def list_nth_mut_loop_loop_back - (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl) - else - do - let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0 - Result.ret (List.Cons x tl0) - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop]: backward function 0 -/ -def list_nth_mut_loop_back - (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := - list_nth_mut_loop_loop_back T ls i ret0 - -/- [loops::list_nth_shared_loop]: loop 0: forward function -/ -divergent def list_nth_shared_loop_loop - (T : Type) (ls : List T) (i : U32) : Result T := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_shared_loop_loop T tl i0 - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_loop]: forward function -/ -def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T := - list_nth_shared_loop_loop T ls i - -/- [loops::get_elem_mut]: loop 0: forward function -/ -divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize := - match ls with - | List.Cons y tl => if y = x - then Result.ret y - else get_elem_mut_loop x tl - | List.Nil => Result.fail Error.panic - -/- [loops::get_elem_mut]: forward function -/ -def get_elem_mut - (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := - do - let l ← - alloc.vec.Vec.index_mut (List Usize) Usize - (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) - slots 0#usize - get_elem_mut_loop x l - -/- [loops::get_elem_mut]: loop 0: backward function 0 -/ -divergent def get_elem_mut_loop_back - (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) := - match ls with - | List.Cons y tl => - if y = x - then Result.ret (List.Cons ret0 tl) - else - do - let tl0 ← get_elem_mut_loop_back x tl ret0 - Result.ret (List.Cons y tl0) - | List.Nil => Result.fail Error.panic - -/- [loops::get_elem_mut]: backward function 0 -/ -def get_elem_mut_back - (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret0 : Usize) : - Result (alloc.vec.Vec (List Usize)) - := - do - let l ← - alloc.vec.Vec.index_mut (List Usize) Usize - (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) - slots 0#usize - let l0 ← get_elem_mut_loop_back x l ret0 - alloc.vec.Vec.index_mut_back (List Usize) Usize - (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) slots - 0#usize l0 - -/- [loops::get_elem_shared]: loop 0: forward function -/ -divergent def get_elem_shared_loop - (x : Usize) (ls : List Usize) : Result Usize := - match ls with - | List.Cons y tl => if y = x - then Result.ret y - else get_elem_shared_loop x tl - | List.Nil => Result.fail Error.panic - -/- [loops::get_elem_shared]: forward function -/ -def get_elem_shared - (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := - do - let l ← - alloc.vec.Vec.index (List Usize) Usize - (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) - slots 0#usize - get_elem_shared_loop x l - -/- [loops::id_mut]: forward function -/ -def id_mut (T : Type) (ls : List T) : Result (List T) := - Result.ret ls - -/- [loops::id_mut]: backward function 0 -/ -def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) := - Result.ret ret0 - -/- [loops::id_shared]: forward function -/ -def id_shared (T : Type) (ls : List T) : Result (List T) := - Result.ret ls - -/- [loops::list_nth_mut_loop_with_id]: loop 0: forward function -/ -divergent def list_nth_mut_loop_with_id_loop - (T : Type) (i : U32) (ls : List T) : Result T := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_mut_loop_with_id_loop T i0 tl - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_with_id]: forward function -/ -def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T := - do - let ls0 ← id_mut T ls - list_nth_mut_loop_with_id_loop T i ls0 - -/- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 -/ -divergent def list_nth_mut_loop_with_id_loop_back - (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl) - else - do - let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0 - Result.ret (List.Cons x tl0) - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_with_id]: backward function 0 -/ -def list_nth_mut_loop_with_id_back - (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := - do - let ls0 ← id_mut T ls - let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret0 - id_mut_back T ls l - -/- [loops::list_nth_shared_loop_with_id]: loop 0: forward function -/ -divergent def list_nth_shared_loop_with_id_loop - (T : Type) (i : U32) (ls : List T) : Result T := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_shared_loop_with_id_loop T i0 tl - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_loop_with_id]: forward function -/ -def list_nth_shared_loop_with_id - (T : Type) (ls : List T) (i : U32) : Result T := - do - let ls0 ← id_shared T ls - list_nth_shared_loop_with_id_loop T i ls0 - -/- [loops::list_nth_mut_loop_pair]: loop 0: forward function -/ -divergent def list_nth_mut_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else do - let i0 ← i - 1#u32 - list_nth_mut_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_pair]: forward function -/ -def list_nth_mut_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 -/ -divergent def list_nth_mut_loop_pair_loop_back'a - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl0) - else - do - let i0 ← i - 1#u32 - let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0 - Result.ret (List.Cons x0 tl00) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_pair]: backward function 0 -/ -def list_nth_mut_loop_pair_back'a - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0 - -/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 -/ -divergent def list_nth_mut_loop_pair_loop_back'b - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl1) - else - do - let i0 ← i - 1#u32 - let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0 - Result.ret (List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_pair]: backward function 1 -/ -def list_nth_mut_loop_pair_back'b - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0 - -/- [loops::list_nth_shared_loop_pair]: loop 0: forward function -/ -divergent def list_nth_shared_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else do - let i0 ← i - 1#u32 - list_nth_shared_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_loop_pair]: forward function -/ -def list_nth_shared_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_shared_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function -/ -divergent def list_nth_mut_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_pair_merge]: forward function -/ -def list_nth_mut_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 -/ -divergent def list_nth_mut_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : - Result ((List T) × (List T)) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then let (t, t0) := ret0 - Result.ret (List.Cons t tl0, List.Cons t0 tl1) - else - do - let i0 ← i - 1#u32 - let (tl00, tl10) ← - list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (List.Cons x0 tl00, List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_pair_merge]: backward function 0 -/ -def list_nth_mut_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : - Result ((List T) × (List T)) - := - list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 - -/- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function -/ -divergent def list_nth_shared_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_loop_pair_merge]: forward function -/ -def list_nth_shared_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_shared_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function -/ -divergent def list_nth_mut_shared_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_shared_loop_pair]: forward function -/ -def list_nth_mut_shared_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_shared_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 -/ -divergent def list_nth_mut_shared_loop_pair_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl0) - else - do - let i0 ← i - 1#u32 - let tl00 ← - list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0 - Result.ret (List.Cons x0 tl00) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_shared_loop_pair]: backward function 0 -/ -def list_nth_mut_shared_loop_pair_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0 - -/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function -/ -divergent def list_nth_mut_shared_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_shared_loop_pair_merge]: forward function -/ -def list_nth_mut_shared_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 -/ -divergent def list_nth_mut_shared_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl0) - else - do - let i0 ← i - 1#u32 - let tl00 ← - list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (List.Cons x0 tl00) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 -/ -def list_nth_mut_shared_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0 - -/- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function -/ -divergent def list_nth_shared_mut_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_mut_loop_pair]: forward function -/ -def list_nth_shared_mut_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_shared_mut_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 -/ -divergent def list_nth_shared_mut_loop_pair_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl1) - else - do - let i0 ← i - 1#u32 - let tl10 ← - list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0 - Result.ret (List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_mut_loop_pair]: backward function 1 -/ -def list_nth_shared_mut_loop_pair_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0 - -/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function -/ -divergent def list_nth_shared_mut_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_mut_loop_pair_merge]: forward function -/ -def list_nth_shared_mut_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 -/ -divergent def list_nth_shared_mut_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl1) - else - do - let i0 ← i - 1#u32 - let tl10 ← - list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 -/ -def list_nth_shared_mut_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 - -end loops diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean deleted file mode 100644 index 018af901..00000000 --- a/tests/lean/Loops/Types.lean +++ /dev/null @@ -1,13 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [loops]: type definitions -import Base -open Primitives - -namespace loops - -/- [loops::List] -/ -inductive List (T : Type) := -| Cons : T → List T → List T -| Nil : List T - -end loops diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 5e812e95..94ae0bb0 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -1 +1,410 @@ -import Traits.Funs +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [traits] +import Base +open Primitives + +namespace traits + +/- Trait declaration: [traits::BoolTrait] -/ +structure BoolTrait (Self : Type) where + get_bool : Self → Result Bool + +/- [traits::Bool::{0}::get_bool]: forward function -/ +def Bool.get_bool (self : Bool) : Result Bool := + Result.ret self + +/- Trait implementation: [traits::Bool::{0}] -/ +def Bool.BoolTraitInst : BoolTrait Bool := { + get_bool := Bool.get_bool +} + +/- [traits::BoolTrait::ret_true]: forward function -/ +def BoolTrait.ret_true + {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool := + Result.ret true + +/- [traits::test_bool_trait_bool]: forward function -/ +def test_bool_trait_bool (x : Bool) : Result Bool := + do + let b ← Bool.get_bool x + if b + then BoolTrait.ret_true Bool.BoolTraitInst x + else Result.ret false + +/- [traits::Option::{1}::get_bool]: forward function -/ +def Option.get_bool (T : Type) (self : Option T) : Result Bool := + match self with + | none => Result.ret false + | some t => Result.ret true + +/- Trait implementation: [traits::Option::{1}] -/ +def Option.BoolTraitInst (T : Type) : BoolTrait (Option T) := { + get_bool := Option.get_bool T +} + +/- [traits::test_bool_trait_option]: forward function -/ +def test_bool_trait_option (T : Type) (x : Option T) : Result Bool := + do + let b ← Option.get_bool T x + if b + then BoolTrait.ret_true (Option.BoolTraitInst T) x + else Result.ret false + +/- [traits::test_bool_trait]: forward function -/ +def test_bool_trait (T : Type) (inst : BoolTrait T) (x : T) : Result Bool := + inst.get_bool x + +/- Trait declaration: [traits::ToU64] -/ +structure ToU64 (Self : Type) where + to_u64 : Self → Result U64 + +/- [traits::u64::{2}::to_u64]: forward function -/ +def u64.to_u64 (self : U64) : Result U64 := + Result.ret self + +/- Trait implementation: [traits::u64::{2}] -/ +def u64.ToU64Inst : ToU64 U64 := { + to_u64 := u64.to_u64 +} + +/- [traits::Tuple2::{3}::to_u64]: forward function -/ +def Tuple2.to_u64 (A : Type) (inst : ToU64 A) (self : (A × A)) : Result U64 := + do + let (t, t0) := self + let i ← inst.to_u64 t + let i0 ← inst.to_u64 t0 + i + i0 + +/- Trait implementation: [traits::Tuple2::{3}] -/ +def Tuple2.ToU64Inst (A : Type) (inst : ToU64 A) : ToU64 (A × A) := { + to_u64 := Tuple2.to_u64 A inst +} + +/- [traits::f]: forward function -/ +def f (T : Type) (inst : ToU64 T) (x : (T × T)) : Result U64 := + Tuple2.to_u64 T inst x + +/- [traits::g]: forward function -/ +def g (T : Type) (inst : ToU64 (T × T)) (x : (T × T)) : Result U64 := + inst.to_u64 x + +/- [traits::h0]: forward function -/ +def h0 (x : U64) : Result U64 := + u64.to_u64 x + +/- [traits::Wrapper] -/ +structure Wrapper (T : Type) where + x : T + +/- [traits::Wrapper::{4}::to_u64]: forward function -/ +def Wrapper.to_u64 + (T : Type) (inst : ToU64 T) (self : Wrapper T) : Result U64 := + inst.to_u64 self.x + +/- Trait implementation: [traits::Wrapper::{4}] -/ +def Wrapper.ToU64Inst (T : Type) (inst : ToU64 T) : ToU64 (Wrapper T) := { + to_u64 := Wrapper.to_u64 T inst +} + +/- [traits::h1]: forward function -/ +def h1 (x : Wrapper U64) : Result U64 := + Wrapper.to_u64 U64 u64.ToU64Inst x + +/- [traits::h2]: forward function -/ +def h2 (T : Type) (inst : ToU64 T) (x : Wrapper T) : Result U64 := + Wrapper.to_u64 T inst x + +/- Trait declaration: [traits::ToType] -/ +structure ToType (Self T : Type) where + to_type : Self → Result T + +/- [traits::u64::{5}::to_type]: forward function -/ +def u64.to_type (self : U64) : Result Bool := + Result.ret (self > 0#u64) + +/- Trait implementation: [traits::u64::{5}] -/ +def u64.ToTypeInst : ToType U64 Bool := { + to_type := u64.to_type +} + +/- Trait declaration: [traits::OfType] -/ +structure OfType (Self : Type) where + of_type : forall (T : Type) (inst : ToType T Self), T → Result Self + +/- [traits::h3]: forward function -/ +def h3 + (T1 T2 : Type) (inst : OfType T1) (inst0 : ToType T2 T1) (y : T2) : + Result T1 + := + inst.of_type T2 inst0 y + +/- Trait declaration: [traits::OfTypeBis] -/ +structure OfTypeBis (Self T : Type) where + parent_clause_0 : ToType T Self + of_type : T → Result Self + +/- [traits::h4]: forward function -/ +def h4 + (T1 T2 : Type) (inst : OfTypeBis T1 T2) (inst0 : ToType T2 T1) (y : T2) : + Result T1 + := + inst.of_type y + +/- [traits::TestType] -/ +structure TestType (T : Type) where + _0 : T + +/- [traits::TestType::{6}::test::TestType1] -/ +structure TestType.test.TestType1 where + _0 : U64 + +/- Trait declaration: [traits::TestType::{6}::test::TestTrait] -/ +structure TestType.test.TestTrait (Self : Type) where + test : Self → Result Bool + +/- [traits::TestType::{6}::test::TestType1::{0}::test]: forward function -/ +def TestType.test.TestType1.test + (self : TestType.test.TestType1) : Result Bool := + Result.ret (self._0 > 1#u64) + +/- Trait implementation: [traits::TestType::{6}::test::TestType1::{0}] -/ +def TestType.test.TestType1.TestTypetestTestTraitInst : TestType.test.TestTrait + TestType.test.TestType1 := { + test := TestType.test.TestType1.test +} + +/- [traits::TestType::{6}::test]: forward function -/ +def TestType.test + (T : Type) (inst : ToU64 T) (self : TestType T) (x : T) : Result Bool := + do + let x0 ← inst.to_u64 x + if x0 > 0#u64 + then TestType.test.TestType1.test { _0 := 0#u64 } + else Result.ret false + +/- [traits::BoolWrapper] -/ +structure BoolWrapper where + _0 : Bool + +/- [traits::BoolWrapper::{7}::to_type]: forward function -/ +def BoolWrapper.to_type + (T : Type) (inst : ToType Bool T) (self : BoolWrapper) : Result T := + inst.to_type self._0 + +/- Trait implementation: [traits::BoolWrapper::{7}] -/ +def BoolWrapper.ToTypeInst (T : Type) (inst : ToType Bool T) : ToType + BoolWrapper T := { + to_type := BoolWrapper.to_type T inst +} + +/- [traits::WithConstTy::LEN2] -/ +def with_const_ty_len2_body : Result Usize := Result.ret 32#usize +def with_const_ty_len2_c : Usize := + eval_global with_const_ty_len2_body (by simp) + +/- Trait declaration: [traits::WithConstTy] -/ +structure WithConstTy (Self : Type) (LEN : Usize) where + LEN1 : Usize + LEN2 : Usize + V : Type + W : Type + W_clause_0 : ToU64 W + f : W → Array U8 LEN → Result W + +/- [traits::Bool::{8}::LEN1] -/ +def bool_len1_body : Result Usize := Result.ret 12#usize +def bool_len1_c : Usize := eval_global bool_len1_body (by simp) + +/- [traits::Bool::{8}::f]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def Bool.f (i : U64) (a : Array U8 32#usize) : Result U64 := + Result.ret i + +/- Trait implementation: [traits::Bool::{8}] -/ +def Bool.WithConstTyInst : WithConstTy Bool 32#usize := { + LEN1 := bool_len1_c + LEN2 := with_const_ty_len2_c + V := U8 + W := U64 + W_clause_0 := u64.ToU64Inst + f := Bool.f +} + +/- [traits::use_with_const_ty1]: forward function -/ +def use_with_const_ty1 + (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) : Result Usize := + let i := inst.LEN1 + Result.ret i + +/- [traits::use_with_const_ty2]: forward function -/ +def use_with_const_ty2 + (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (w : inst.W) : + Result Unit + := + Result.ret () + +/- [traits::use_with_const_ty3]: forward function -/ +def use_with_const_ty3 + (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (x : inst.W) : + Result U64 + := + inst.W_clause_0.to_u64 x + +/- [traits::test_where1]: forward function -/ +def test_where1 (T : Type) (_x : T) : Result Unit := + Result.ret () + +/- [traits::test_where2]: forward function -/ +def test_where2 + (T : Type) (inst : WithConstTy T 32#usize) (_x : U32) : Result Unit := + Result.ret () + +/- [alloc::string::String] -/ +axiom alloc.string.String : Type + +/- Trait declaration: [traits::ParentTrait0] -/ +structure ParentTrait0 (Self : Type) where + W : Type + get_name : Self → Result alloc.string.String + get_w : Self → Result W + +/- Trait declaration: [traits::ParentTrait1] -/ +structure ParentTrait1 (Self : Type) where + +/- Trait declaration: [traits::ChildTrait] -/ +structure ChildTrait (Self : Type) where + parent_clause_0 : ParentTrait0 Self + parent_clause_1 : ParentTrait1 Self + +/- [traits::test_child_trait1]: forward function -/ +def test_child_trait1 + (T : Type) (inst : ChildTrait T) (x : T) : Result alloc.string.String := + inst.parent_clause_0.get_name x + +/- [traits::test_child_trait2]: forward function -/ +def test_child_trait2 + (T : Type) (inst : ChildTrait T) (x : T) : Result inst.parent_clause_0.W := + inst.parent_clause_0.get_w x + +/- [traits::order1]: forward function -/ +def order1 + (T U : Type) (inst : ParentTrait0 T) (inst0 : ParentTrait0 U) : + Result Unit + := + Result.ret () + +/- Trait declaration: [traits::ChildTrait1] -/ +structure ChildTrait1 (Self : Type) where + parent_clause_0 : ParentTrait1 Self + +/- Trait implementation: [traits::usize::{9}] -/ +def usize.ParentTrait1Inst : ParentTrait1 Usize := { +} + +/- Trait implementation: [traits::usize::{10}] -/ +def usize.ChildTrait1Inst : ChildTrait1 Usize := { + parent_clause_0 := usize.ParentTrait1Inst +} + +/- Trait declaration: [traits::Iterator] -/ +structure Iterator (Self : Type) where + Item : Type + +/- Trait declaration: [traits::IntoIterator] -/ +structure IntoIterator (Self : Type) where + Item : Type + IntoIter : Type + IntoIter_clause_0 : Iterator IntoIter + into_iter : Self → Result IntoIter + +/- Trait declaration: [traits::FromResidual] -/ +structure FromResidual (Self T : Type) where + +/- Trait declaration: [traits::Try] -/ +structure Try (Self : Type) where + parent_clause_0 : FromResidual Self Residual + Residual : Type + +/- Trait declaration: [traits::CFnOnce] -/ +structure CFnOnce (Self Args : Type) where + Output : Type + call_once : Self → Args → Result Output + +/- Trait declaration: [traits::CFnMut] -/ +structure CFnMut (Self Args : Type) where + parent_clause_0 : CFnOnce Self Args + call_mut : Self → Args → Result parent_clause_0.Output + call_mut_back : Self → Args → parent_clause_0.Output → Result Self + +/- Trait declaration: [traits::CFn] -/ +structure CFn (Self Args : Type) where + parent_clause_0 : CFnMut Self Args + call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output + +/- Trait declaration: [core::ops::function::FnOnce] -/ +structure core.ops.function.FnOnce (Self Args : Type) where + Output : Type + call_once : Self → Args → Result Output + +/- Trait declaration: [core::ops::function::FnMut] -/ +structure core.ops.function.FnMut (Self Args : Type) where + parent_clause_0 : core.ops.function.FnOnce Self Args + call_mut : Self → Args → Result parent_clause_0.Output + call_mut_back : Self → Args → parent_clause_0.Output → Result Self + +/- Trait declaration: [core::ops::function::Fn] -/ +structure core.ops.function.Fn (Self Args : Type) where + parent_clause_0 : core.ops.function.FnMut Self Args + call : Self → Args → Result parent_clause_0.parent_clause_0.Output + +/- [traits::map_option]: forward function -/ +def map_option + (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) : + Result (Option T) + := + match x with + | none => Result.ret none + | some x0 => do + let t ← inst.call f0 x0 + Result.ret (some t) + +/- Trait declaration: [traits::WithTarget] -/ +structure WithTarget (Self : Type) where + Target : Type + +/- Trait declaration: [traits::ParentTrait2] -/ +structure ParentTrait2 (Self : Type) where + U : Type + U_clause_0 : WithTarget U + +/- Trait declaration: [traits::ChildTrait2] -/ +structure ChildTrait2 (Self : Type) where + parent_clause_0 : ParentTrait2 Self + convert : parent_clause_0.U → Result parent_clause_0.U_clause_0.Target + +/- Trait implementation: [traits::u32::{11}] -/ +def u32.WithTargetInst : WithTarget U32 := { + Target := U32 +} + +/- Trait implementation: [traits::u32::{12}] -/ +def u32.ParentTrait2Inst : ParentTrait2 U32 := { + U := U32 + U_clause_0 := u32.WithTargetInst +} + +/- [traits::u32::{13}::convert]: forward function -/ +def u32.convert (x : U32) : Result U32 := + Result.ret x + +/- Trait implementation: [traits::u32::{13}] -/ +def u32.ChildTrait2Inst : ChildTrait2 U32 := { + parent_clause_0 := u32.ParentTrait2Inst + convert := u32.convert +} + +/- [traits::incr_u32]: forward function -/ +def incr_u32 (x : U32) : Result U32 := + x + 1#u32 + +end traits diff --git a/tests/lean/Traits/Funs.lean b/tests/lean/Traits/Funs.lean deleted file mode 100644 index 8d423280..00000000 --- a/tests/lean/Traits/Funs.lean +++ /dev/null @@ -1,275 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [traits]: function definitions -import Base -import Traits.Types -open Primitives - -namespace traits - -/- [traits::Bool::{0}::get_bool]: forward function -/ -def Bool.get_bool (self : Bool) : Result Bool := - Result.ret self - -/- Trait implementation: [traits::Bool::{0}] -/ -def Bool.BoolTraitInst : BoolTrait Bool := { - get_bool := Bool.get_bool -} - -/- [traits::BoolTrait::ret_true]: forward function -/ -def BoolTrait.ret_true - {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool := - Result.ret true - -/- [traits::test_bool_trait_bool]: forward function -/ -def test_bool_trait_bool (x : Bool) : Result Bool := - do - let b ← Bool.get_bool x - if b - then BoolTrait.ret_true Bool.BoolTraitInst x - else Result.ret false - -/- [traits::Option::{1}::get_bool]: forward function -/ -def Option.get_bool (T : Type) (self : Option T) : Result Bool := - match self with - | none => Result.ret false - | some t => Result.ret true - -/- Trait implementation: [traits::Option::{1}] -/ -def Option.BoolTraitInst (T : Type) : BoolTrait (Option T) := { - get_bool := Option.get_bool T -} - -/- [traits::test_bool_trait_option]: forward function -/ -def test_bool_trait_option (T : Type) (x : Option T) : Result Bool := - do - let b ← Option.get_bool T x - if b - then BoolTrait.ret_true (Option.BoolTraitInst T) x - else Result.ret false - -/- [traits::test_bool_trait]: forward function -/ -def test_bool_trait (T : Type) (inst : BoolTrait T) (x : T) : Result Bool := - inst.get_bool x - -/- [traits::u64::{2}::to_u64]: forward function -/ -def u64.to_u64 (self : U64) : Result U64 := - Result.ret self - -/- Trait implementation: [traits::u64::{2}] -/ -def u64.ToU64Inst : ToU64 U64 := { - to_u64 := u64.to_u64 -} - -/- [traits::Tuple2::{3}::to_u64]: forward function -/ -def Tuple2.to_u64 (A : Type) (inst : ToU64 A) (self : (A × A)) : Result U64 := - do - let (t, t0) := self - let i ← inst.to_u64 t - let i0 ← inst.to_u64 t0 - i + i0 - -/- Trait implementation: [traits::Tuple2::{3}] -/ -def Tuple2.ToU64Inst (A : Type) (inst : ToU64 A) : ToU64 (A × A) := { - to_u64 := Tuple2.to_u64 A inst -} - -/- [traits::f]: forward function -/ -def f (T : Type) (inst : ToU64 T) (x : (T × T)) : Result U64 := - Tuple2.to_u64 T inst x - -/- [traits::g]: forward function -/ -def g (T : Type) (inst : ToU64 (T × T)) (x : (T × T)) : Result U64 := - inst.to_u64 x - -/- [traits::h0]: forward function -/ -def h0 (x : U64) : Result U64 := - u64.to_u64 x - -/- [traits::Wrapper::{4}::to_u64]: forward function -/ -def Wrapper.to_u64 - (T : Type) (inst : ToU64 T) (self : Wrapper T) : Result U64 := - inst.to_u64 self.x - -/- Trait implementation: [traits::Wrapper::{4}] -/ -def Wrapper.ToU64Inst (T : Type) (inst : ToU64 T) : ToU64 (Wrapper T) := { - to_u64 := Wrapper.to_u64 T inst -} - -/- [traits::h1]: forward function -/ -def h1 (x : Wrapper U64) : Result U64 := - Wrapper.to_u64 U64 u64.ToU64Inst x - -/- [traits::h2]: forward function -/ -def h2 (T : Type) (inst : ToU64 T) (x : Wrapper T) : Result U64 := - Wrapper.to_u64 T inst x - -/- [traits::u64::{5}::to_type]: forward function -/ -def u64.to_type (self : U64) : Result Bool := - Result.ret (self > 0#u64) - -/- Trait implementation: [traits::u64::{5}] -/ -def u64.ToTypeInst : ToType U64 Bool := { - to_type := u64.to_type -} - -/- [traits::h3]: forward function -/ -def h3 - (T1 T2 : Type) (inst : OfType T1) (inst0 : ToType T2 T1) (y : T2) : - Result T1 - := - inst.of_type T2 inst0 y - -/- [traits::h4]: forward function -/ -def h4 - (T1 T2 : Type) (inst : OfTypeBis T1 T2) (inst0 : ToType T2 T1) (y : T2) : - Result T1 - := - inst.of_type y - -/- [traits::TestType::{6}::test::TestType1::{0}::test]: forward function -/ -def TestType.test.TestType1.test - (self : TestType.test.TestType1) : Result Bool := - Result.ret (self._0 > 1#u64) - -/- Trait implementation: [traits::TestType::{6}::test::TestType1::{0}] -/ -def TestType.test.TestType1.TestTypetestTestTraitInst : TestType.test.TestTrait - TestType.test.TestType1 := { - test := TestType.test.TestType1.test -} - -/- [traits::TestType::{6}::test]: forward function -/ -def TestType.test - (T : Type) (inst : ToU64 T) (self : TestType T) (x : T) : Result Bool := - do - let x0 ← inst.to_u64 x - if x0 > 0#u64 - then TestType.test.TestType1.test { _0 := 0#u64 } - else Result.ret false - -/- [traits::BoolWrapper::{7}::to_type]: forward function -/ -def BoolWrapper.to_type - (T : Type) (inst : ToType Bool T) (self : BoolWrapper) : Result T := - inst.to_type self._0 - -/- Trait implementation: [traits::BoolWrapper::{7}] -/ -def BoolWrapper.ToTypeInst (T : Type) (inst : ToType Bool T) : ToType - BoolWrapper T := { - to_type := BoolWrapper.to_type T inst -} - -/- [traits::WithConstTy::LEN2] -/ -def with_const_ty_len2_body : Result Usize := Result.ret 32#usize -def with_const_ty_len2_c : Usize := - eval_global with_const_ty_len2_body (by simp) - -/- [traits::Bool::{8}::LEN1] -/ -def bool_len1_body : Result Usize := Result.ret 12#usize -def bool_len1_c : Usize := eval_global bool_len1_body (by simp) - -/- [traits::Bool::{8}::f]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) -/ -def Bool.f (i : U64) (a : Array U8 32#usize) : Result U64 := - Result.ret i - -/- Trait implementation: [traits::Bool::{8}] -/ -def Bool.WithConstTyInst : WithConstTy Bool 32#usize := { - LEN1 := bool_len1_c - LEN2 := with_const_ty_len2_c - V := U8 - W := U64 - W_clause_0 := u64.ToU64Inst - f := Bool.f -} - -/- [traits::use_with_const_ty1]: forward function -/ -def use_with_const_ty1 - (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) : Result Usize := - let i := inst.LEN1 - Result.ret i - -/- [traits::use_with_const_ty2]: forward function -/ -def use_with_const_ty2 - (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (w : inst.W) : - Result Unit - := - Result.ret () - -/- [traits::use_with_const_ty3]: forward function -/ -def use_with_const_ty3 - (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (x : inst.W) : - Result U64 - := - inst.W_clause_0.to_u64 x - -/- [traits::test_where1]: forward function -/ -def test_where1 (T : Type) (_x : T) : Result Unit := - Result.ret () - -/- [traits::test_where2]: forward function -/ -def test_where2 - (T : Type) (inst : WithConstTy T 32#usize) (_x : U32) : Result Unit := - Result.ret () - -/- [traits::test_child_trait1]: forward function -/ -def test_child_trait1 - (T : Type) (inst : ChildTrait T) (x : T) : Result alloc.string.String := - inst.parent_clause_0.get_name x - -/- [traits::test_child_trait2]: forward function -/ -def test_child_trait2 - (T : Type) (inst : ChildTrait T) (x : T) : Result inst.parent_clause_0.W := - inst.parent_clause_0.get_w x - -/- [traits::order1]: forward function -/ -def order1 - (T U : Type) (inst : ParentTrait0 T) (inst0 : ParentTrait0 U) : - Result Unit - := - Result.ret () - -/- Trait implementation: [traits::usize::{9}] -/ -def usize.ParentTrait1Inst : ParentTrait1 Usize := { -} - -/- Trait implementation: [traits::usize::{10}] -/ -def usize.ChildTrait1Inst : ChildTrait1 Usize := { - parent_clause_0 := usize.ParentTrait1Inst -} - -/- [traits::map_option]: forward function -/ -def map_option - (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) : - Result (Option T) - := - match x with - | none => Result.ret none - | some x0 => do - let t ← inst.call f0 x0 - Result.ret (some t) - -/- Trait implementation: [traits::u32::{11}] -/ -def u32.WithTargetInst : WithTarget U32 := { - Target := U32 -} - -/- Trait implementation: [traits::u32::{12}] -/ -def u32.ParentTrait2Inst : ParentTrait2 U32 := { - U := U32 - U_clause_0 := u32.WithTargetInst -} - -/- [traits::u32::{13}::convert]: forward function -/ -def u32.convert (x : U32) : Result U32 := - Result.ret x - -/- Trait implementation: [traits::u32::{13}] -/ -def u32.ChildTrait2Inst : ChildTrait2 U32 := { - parent_clause_0 := u32.ParentTrait2Inst - convert := u32.convert -} - -/- [traits::incr_u32]: forward function -/ -def incr_u32 (x : U32) : Result U32 := - x + 1#u32 - -end traits diff --git a/tests/lean/Traits/Types.lean b/tests/lean/Traits/Types.lean deleted file mode 100644 index 4c5dd874..00000000 --- a/tests/lean/Traits/Types.lean +++ /dev/null @@ -1,144 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [traits]: type definitions -import Base -open Primitives - -namespace traits - -/- Trait declaration: [traits::BoolTrait] -/ -structure BoolTrait (Self : Type) where - get_bool : Self → Result Bool - -/- Trait declaration: [traits::ToU64] -/ -structure ToU64 (Self : Type) where - to_u64 : Self → Result U64 - -/- [traits::Wrapper] -/ -structure Wrapper (T : Type) where - x : T - -/- Trait declaration: [traits::ToType] -/ -structure ToType (Self T : Type) where - to_type : Self → Result T - -/- Trait declaration: [traits::OfType] -/ -structure OfType (Self : Type) where - of_type : forall (T : Type) (inst : ToType T Self), T → Result Self - -/- Trait declaration: [traits::OfTypeBis] -/ -structure OfTypeBis (Self T : Type) where - parent_clause_0 : ToType T Self - of_type : T → Result Self - -/- [traits::TestType] -/ -structure TestType (T : Type) where - _0 : T - -/- [traits::TestType::{6}::test::TestType1] -/ -structure TestType.test.TestType1 where - _0 : U64 - -/- Trait declaration: [traits::TestType::{6}::test::TestTrait] -/ -structure TestType.test.TestTrait (Self : Type) where - test : Self → Result Bool - -/- [traits::BoolWrapper] -/ -structure BoolWrapper where - _0 : Bool - -/- Trait declaration: [traits::WithConstTy] -/ -structure WithConstTy (Self : Type) (LEN : Usize) where - LEN1 : Usize - LEN2 : Usize - V : Type - W : Type - W_clause_0 : ToU64 W - f : W → Array U8 LEN → Result W - -/- [alloc::string::String] -/ -axiom alloc.string.String : Type - -/- Trait declaration: [traits::ParentTrait0] -/ -structure ParentTrait0 (Self : Type) where - W : Type - get_name : Self → Result alloc.string.String - get_w : Self → Result W - -/- Trait declaration: [traits::ParentTrait1] -/ -structure ParentTrait1 (Self : Type) where - -/- Trait declaration: [traits::ChildTrait] -/ -structure ChildTrait (Self : Type) where - parent_clause_0 : ParentTrait0 Self - parent_clause_1 : ParentTrait1 Self - -/- Trait declaration: [traits::ChildTrait1] -/ -structure ChildTrait1 (Self : Type) where - parent_clause_0 : ParentTrait1 Self - -/- Trait declaration: [traits::Iterator] -/ -structure Iterator (Self : Type) where - Item : Type - -/- Trait declaration: [traits::IntoIterator] -/ -structure IntoIterator (Self : Type) where - Item : Type - IntoIter : Type - IntoIter_clause_0 : Iterator IntoIter - into_iter : Self → Result IntoIter - -/- Trait declaration: [traits::FromResidual] -/ -structure FromResidual (Self T : Type) where - -/- Trait declaration: [traits::Try] -/ -structure Try (Self : Type) where - parent_clause_0 : FromResidual Self Residual - Residual : Type - -/- Trait declaration: [traits::CFnOnce] -/ -structure CFnOnce (Self Args : Type) where - Output : Type - call_once : Self → Args → Result Output - -/- Trait declaration: [traits::CFnMut] -/ -structure CFnMut (Self Args : Type) where - parent_clause_0 : CFnOnce Self Args - call_mut : Self → Args → Result parent_clause_0.Output - call_mut_back : Self → Args → parent_clause_0.Output → Result Self - -/- Trait declaration: [traits::CFn] -/ -structure CFn (Self Args : Type) where - parent_clause_0 : CFnMut Self Args - call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output - -/- Trait declaration: [core::ops::function::FnOnce] -/ -structure core.ops.function.FnOnce (Self Args : Type) where - Output : Type - call_once : Self → Args → Result Output - -/- Trait declaration: [core::ops::function::FnMut] -/ -structure core.ops.function.FnMut (Self Args : Type) where - parent_clause_0 : core.ops.function.FnOnce Self Args - call_mut : Self → Args → Result parent_clause_0.Output - call_mut_back : Self → Args → parent_clause_0.Output → Result Self - -/- Trait declaration: [core::ops::function::Fn] -/ -structure core.ops.function.Fn (Self Args : Type) where - parent_clause_0 : core.ops.function.FnMut Self Args - call : Self → Args → Result parent_clause_0.parent_clause_0.Output - -/- Trait declaration: [traits::WithTarget] -/ -structure WithTarget (Self : Type) where - Target : Type - -/- Trait declaration: [traits::ParentTrait2] -/ -structure ParentTrait2 (Self : Type) where - U : Type - U_clause_0 : WithTarget U - -/- Trait declaration: [traits::ChildTrait2] -/ -structure ChildTrait2 (Self : Type) where - parent_clause_0 : ParentTrait2 Self - convert : parent_clause_0.U → Result parent_clause_0.U_clause_0.Target - -end traits -- cgit v1.3.1