diff options
| -rw-r--r-- | backends/coq/Primitives.v | 3 | ||||
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 57 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Array.lean | 9 | ||||
| -rw-r--r-- | compiler/Assumed.ml | 15 | ||||
| -rw-r--r-- | compiler/Driver.ml | 2 | ||||
| -rw-r--r-- | compiler/Extract.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 2 | ||||
| -rw-r--r-- | compiler/PrintPure.ml | 1 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 2 |
9 files changed, 91 insertions, 4 deletions
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 = + (* <T, N> *) + 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) |