summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backends/coq/Primitives.v3
-rw-r--r--backends/lean/Base/IList/IList.lean57
-rw-r--r--backends/lean/Base/Primitives/Array.lean9
-rw-r--r--compiler/Assumed.ml15
-rw-r--r--compiler/Driver.ml2
-rw-r--r--compiler/Extract.ml4
-rw-r--r--compiler/InterpreterStatements.ml2
-rw-r--r--compiler/PrintPure.ml1
-rw-r--r--compiler/PureMicroPasses.ml2
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)