From 50af296306bfee9f0b127dde8abe5fb0ec1b0acb Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 1 Aug 2023 11:16:06 +0200 Subject: Start adding support for const generics --- compiler/Assumed.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index e751d0ba..2fbb9044 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -53,6 +53,8 @@ module Sig = struct (** Type parameter [T] of id 0 *) let type_param_0 : T.type_var = { T.index = tvar_id_0; name = "T" } + let empty_const_generic_params : T.const_generic_var list = [] + let mk_ref_ty (r : T.RegionVarId.id T.region) (ty : T.sty) (is_mut : bool) : T.sty = let ref_kind = if is_mut then T.Mut else T.Shared in @@ -73,6 +75,7 @@ module Sig = struct num_early_bound_regions = 0; regions_hierarchy; type_params; + const_generic_params = empty_const_generic_params; inputs; output; } @@ -84,6 +87,7 @@ module Sig = struct num_early_bound_regions = 0; regions_hierarchy = []; type_params = [ type_param_0 ] (* *); + const_generic_params = empty_const_generic_params; inputs = [ tvar_0 (* T *) ]; output = mk_box_ty tvar_0 (* Box *); } @@ -95,6 +99,7 @@ module Sig = struct num_early_bound_regions = 0; regions_hierarchy = []; type_params = [ type_param_0 ] (* *); + const_generic_params = empty_const_generic_params; inputs = [ mk_box_ty tvar_0 (* Box *) ]; output = mk_unit_ty (* () *); } @@ -112,6 +117,7 @@ module Sig = struct num_early_bound_regions = 0; regions_hierarchy; type_params = [ type_param_0 ] (* *); + const_generic_params = empty_const_generic_params; inputs = [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box *) ]; output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *); @@ -135,6 +141,7 @@ module Sig = struct num_early_bound_regions = 0; regions_hierarchy; type_params; + const_generic_params = empty_const_generic_params; inputs; output; } @@ -157,6 +164,7 @@ module Sig = struct num_early_bound_regions = 0; regions_hierarchy; type_params; + const_generic_params = empty_const_generic_params; inputs; output; } @@ -180,6 +188,7 @@ module Sig = struct num_early_bound_regions = 0; regions_hierarchy; type_params; + const_generic_params = empty_const_generic_params; inputs; output; } @@ -199,6 +208,7 @@ module Sig = struct num_early_bound_regions = 0; regions_hierarchy; type_params; + const_generic_params = empty_const_generic_params; inputs; output; } @@ -223,6 +233,7 @@ module Sig = struct num_early_bound_regions = 0; regions_hierarchy; type_params; + const_generic_params = empty_const_generic_params; inputs; output; } -- cgit v1.3.1 From f6b4aade7b4a60ed589440af042b44c65c9fcb92 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 2 Aug 2023 17:43:13 +0200 Subject: Add the function signatures in Assumed.ml --- compiler/Assumed.ml | 143 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 143 insertions(+) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 2fbb9044..e0a2efea 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -42,6 +42,8 @@ module Sig = struct let rg_id_0 = T.RegionGroupId.of_int 0 let tvar_id_0 = T.TypeVarId.of_int 0 let tvar_0 : T.sty = T.TypeVar tvar_id_0 + let cgvar_id_0 = T.ConstGenericVarId.of_int 0 + let cgvar_0 : T.const_generic = T.ConstGenericVar cgvar_id_0 (** Region 'a of id 0 *) let region_param_0 : T.region_var = { T.index = rvar_id_0; name = Some "'a" } @@ -53,6 +55,12 @@ module Sig = struct (** Type parameter [T] of id 0 *) let type_param_0 : T.type_var = { T.index = tvar_id_0; name = "T" } + let usize_ty : T.sty = T.Literal (Integer Usize) + + (** Const generic parameter [const N : usize] of id 0 *) + let cg_param_0 : T.const_generic_var = + { T.index = cgvar_id_0; name = "N"; ty = Integer Usize } + let empty_const_generic_params : T.const_generic_var list = [] let mk_ref_ty (r : T.RegionVarId.id T.region) (ty : T.sty) (is_mut : bool) : @@ -60,6 +68,12 @@ module Sig = struct let ref_kind = if is_mut then T.Mut else T.Shared in mk_ref_ty r ty ref_kind + let mk_array_ty (ty : T.sty) (cg : T.const_generic) : T.sty = + Adt (Assumed Array, [], [ ty ], [ cg ]) + + let mk_slice_ty (ty : T.sty) : T.sty = Adt (Assumed Slice, [], [ ty ], []) + let range_ty : T.sty = Adt (Assumed Range, [], [ usize_ty ], []) + (** [fn(&'a mut T, T) -> T] *) let mem_replace_sig : A.fun_sig = (* The signature fields *) @@ -243,6 +257,96 @@ module Sig = struct (** [fn(&'a mut Vec, usize) -> &'a mut T] *) let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true + + (** Array/slice functions *) + + (** Small helper. + + Return the type: + {[ + fn<'a, T>(&'a input_ty, index_ty) -> &'a output_ty + ]} + + Remarks: + The [input_ty] and [output_ty] are parameterized by a type variable id. + The [mut_borrow] boolean controls whether we use a shared or a mutable + borrow. + *) + let mk_array_slice_borrow_sig (cgs : T.const_generic_var list) + (input_ty : T.TypeVarId.id -> T.sty) (index_ty : T.sty option) + (output_ty : T.TypeVarId.id -> T.sty) (is_mut : bool) : A.fun_sig = + (* The signature fields *) + let region_params = [ region_param_0 ] in + let regions_hierarchy = [ region_group_0 ] (* <'a> *) in + let type_params = [ type_param_0 ] (* *) in + let inputs = + [ + mk_ref_ty rvar_0 + (input_ty type_param_0.index) + is_mut (* &'a (mut) input_ty *); + ] + in + let inputs = + List.append inputs (match index_ty with None -> [] | Some ty -> [ ty ]) + in + let output = + mk_ref_ty rvar_0 + (output_ty type_param_0.index) + is_mut (* &'a (mut) output_ty *) + in + { + region_params; + num_early_bound_regions = 0; + regions_hierarchy; + type_params; + const_generic_params = cgs; + inputs; + output; + } + + let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig = + (* Array *) + let input_ty id = + if is_array then mk_array_ty (T.TypeVar id) cgvar_0 + else mk_slice_ty (T.TypeVar id) + in + (* usize *) + let index_ty = usize_ty in + (* T *) + let output_ty id = T.TypeVar id in + let cgs = if is_array then [ cg_param_0 ] else [] in + mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut + + let array_index_sig (is_mut : bool) = mk_array_slice_index_sig true is_mut + let slice_index_sig (is_mut : bool) = mk_array_slice_index_sig false is_mut + + let array_to_slice_sig (is_mut : bool) : A.fun_sig = + (* Array *) + let input_ty id = mk_array_ty (T.TypeVar id) cgvar_0 in + (* Slice *) + let output_ty id = mk_slice_ty (T.TypeVar id) in + let cgs = [ cg_param_0 ] in + mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut + + let mk_array_slice_subslice_sig (is_array : bool) (is_mut : bool) : A.fun_sig + = + (* Array *) + let input_ty id = + if is_array then mk_array_ty (T.TypeVar id) cgvar_0 + else mk_slice_ty (T.TypeVar id) + in + (* Range *) + let index_ty = range_ty in + (* Slice *) + let output_ty id = mk_slice_ty (T.TypeVar id) in + let cgs = if is_array then [ cg_param_0 ] else [] in + mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut + + let array_subslice_sig (is_mut : bool) = + mk_array_slice_subslice_sig true is_mut + + let slice_subslice_sig (is_mut : bool) = + mk_array_slice_subslice_sig false is_mut end type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name @@ -289,6 +393,45 @@ let assumed_infos : assumed_info list = Sig.vec_index_mut_sig, true, to_name (index_pre @ [ "IndexMut"; "index_mut" ]) ); + (* Array Index *) + ( ArraySharedIndex, + Sig.array_index_sig false, + true, + to_name [ "@ArraySharedIndex" ] ); + (ArrayMutIndex, Sig.array_index_sig true, true, to_name [ "@ArrayMutIndex" ]); + (* Array to slice*) + ( ArrayToSharedSlice, + Sig.array_to_slice_sig false, + false, + to_name [ "@ArrayToSharedSlice" ] ); + ( ArrayToMutSlice, + Sig.array_to_slice_sig true, + false, + to_name [ "@ArrayToMutSlice" ] ); + (* Array Subslice *) + ( ArraySharedSubslice, + Sig.array_subslice_sig false, + true, + to_name [ "@ArraySharedSubslice" ] ); + ( ArrayMutSubslice, + Sig.array_subslice_sig true, + true, + to_name [ "@ArrayMutSubslice" ] ); + (* Slice Index *) + ( SliceSharedIndex, + Sig.slice_index_sig false, + true, + to_name [ "@SliceSharedIndex" ] ); + (SliceMutIndex, Sig.slice_index_sig true, true, to_name [ "@SliceMutIndex" ]); + (* Slice Subslice *) + ( SliceSharedSubslice, + Sig.slice_subslice_sig false, + true, + to_name [ "@SliceSharedSubslice" ] ); + ( SliceMutSubslice, + Sig.slice_subslice_sig true, + true, + to_name [ "@SliceMutSubslice" ] ); ] let get_assumed_info (id : A.assumed_fun_id) : assumed_info = -- cgit v1.3.1 From 79225e6ca645ca3902b3b761966dc869306cedbd Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 4 Aug 2023 19:57:48 +0200 Subject: Add SliceLen as a primitive function and make minor adjustments --- backends/lean/Base/Primitives/Array.lean | 80 +++++++++++++++----------------- compiler/Assumed.ml | 33 +++++++++++-- compiler/Extract.ml | 58 ++++++++++++----------- compiler/InterpreterStatements.ml | 2 +- compiler/PrintPure.ml | 1 + compiler/PureMicroPasses.ml | 3 +- 6 files changed, 100 insertions(+), 77 deletions(-) (limited to 'compiler/Assumed.ml') diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean index d19e9144..2d4a567b 100644 --- a/backends/lean/Base/Primitives/Array.lean +++ b/backends/lean/Base/Primitives/Array.lean @@ -14,7 +14,7 @@ namespace Primitives open Result Error -abbrev Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val } +def Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val } instance (a : Type u) (n : Usize) : Arith.HasIntProp (Array a n) where prop_ty := λ v => v.val.len = n.val @@ -33,19 +33,10 @@ abbrev Array.v {α : Type u} {n : Usize} (v : Array α n) : List α := v.val example {α: Type u} {n : Usize} (v : Array α n) : v.length ≤ Scalar.max ScalarTy.Usize := by scalar_tac -def Array.mk (α : Type u) (n : Usize) (init : List α) (hl : init.len = n.val := by decide) : +def Array.make (α : Type u) (n : Usize) (init : List α) (hl : init.len = n.val := by decide) : Array α n := ⟨ init, by simp [← List.len_eq_length]; apply hl ⟩ -example : Array Int (Usize.ofInt 2) := Array.mk Int (Usize.ofInt 2) [0, 1] - --- Remark: not used yet, but could be used if explicit calls to Len are used in Rust --- TODO: very annoying that the α and the n are explicit parameters -def Array.len (α : Type u) (n : Usize) (v : Array α n) : Usize := - Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac) - -@[simp] -theorem Array.len_val {α : Type u} {n : Usize} (v : Array α n) : (Array.len α n v).val = v.length := - by rfl +example : Array Int (Usize.ofInt 2) := Array.make Int (Usize.ofInt 2) [0, 1] @[simp] abbrev Array.index {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Int) : α := @@ -81,7 +72,7 @@ def Array.index_shared_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) else .fail arrayOutOfBounds -def Array.index_mut (α : Type u) (v: Array α n) (i: Usize) : Result α := +def Array.index_mut (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α := match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds | some x => ret x @@ -89,13 +80,13 @@ def Array.index_mut (α : Type u) (v: Array α n) (i: Usize) : Result α := @[pspec] theorem Array.index_mut_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize) (hbound : i.val < v.length) : - ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by + ∃ x, v.index_mut α n i = ret x ∧ x = v.val.index i.val := by simp only [index_mut] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) simp [*] -def Array.index_mut_back (α : Type u) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) := +def Array.index_mut_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) := match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds | some _ => @@ -104,7 +95,7 @@ def Array.index_mut_back (α : Type u) (v: Array α n) (i: Usize) (x: α) : Resu @[pspec] theorem Array.index_mut_back_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α) (hbound : i.val < v.length) : - ∃ nv, v.index_mut_back α i x = ret nv ∧ + ∃ nv, v.index_mut_back α n i x = ret nv ∧ nv.val = v.val.update i.val x := by simp only [index_mut_back] @@ -209,6 +200,11 @@ theorem Slice.index_mut_back_spec {α : Type u} (v: Slice α) (i: Usize) (x : α . simp_all /- Array to slice/subslices -/ + +/- We could make this function not use the `Result` type. By making it monadic, we + push the user to use the `Array.to_slice_spec` spec theorem below (through the + `progress` tactic), meaning `Array.to_slice` should be considered as opaque. + All what the spec theorem reveals is that the "representative" lists are the same. -/ def Array.to_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) := ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩ @@ -233,7 +229,7 @@ theorem Array.to_mut_slice_back_spec {α : Type u} {n : Usize} (a : Array α n) ∃ na, to_mut_slice_back α n a ns = ret na ∧ na.val = ns.val := by simp [to_mut_slice_back, *] -def Array.shared_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) := +def Array.subslice_shared (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) := -- TODO: not completely sure here if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then ret ⟨ a.val.slice r.start.val r.end_.val, @@ -245,29 +241,29 @@ def Array.shared_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range fail panic @[pspec] -theorem Array.shared_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) +theorem Array.subslice_shared_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) : - ∃ s, shared_subslice α n a r = ret s ∧ + ∃ s, subslice_shared α n a r = ret s ∧ s.val = a.val.slice r.start.val r.end_.val ∧ (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i)) := by - simp [shared_subslice, *] + simp [subslice_shared, *] intro i _ _ have := List.index_slice r.start.val r.end_.val i a.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac) simp [*] -def Array.mut_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) := - Array.shared_subslice α n a r +def Array.subslice_mut (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) := + Array.subslice_shared α n a r @[pspec] -theorem Array.mut_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) +theorem Array.subslice_mut_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) : - ∃ s, mut_subslice α n a r = ret s ∧ + ∃ s, subslice_mut α n a r = ret s ∧ s.val = a.slice r.start.val r.end_.val ∧ (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i)) - := shared_subslice_spec a r h0 h1 + := subslice_shared_spec a r h0 h1 -def Array.mut_subslice_back (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) := +def Array.subslice_mut_back (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) := -- TODO: not completely sure here if h: r.start.val < r.end_.val ∧ r.end_.val ≤ a.length ∧ s.val.len = r.end_.val - r.start.val then let s_beg := a.val.itake r.start.val @@ -292,13 +288,13 @@ def Array.mut_subslice_back (α : Type u) (n : Usize) (a : Array α n) (r : Rang -- We should introduce special symbols for the monadic arithmetic operations -- (the use will never write those symbols directly). @[pspec] -theorem Array.mut_subslice_back_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α) +theorem Array.subslice_mut_back_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α) (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) : - ∃ na, mut_subslice_back α n a r s = ret na ∧ + ∃ na, subslice_mut_back α n a r s = ret na ∧ (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧ (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = s.index (i - r.start.val)) ∧ (∀ i, r.end_.val ≤ i → i < n.val → na.index i = a.index i) := by - simp [mut_subslice_back, *] + simp [subslice_mut_back, *] have h := List.replace_slice_index r.start.val r.end_.val a.val s.val (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac) simp [List.replace_slice] at h @@ -315,7 +311,7 @@ theorem Array.mut_subslice_back_spec {α : Type u} {n : Usize} [Inhabited α] (a have := h2 i (by int_tac) (by int_tac) simp [*] -def Slice.shared_subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) := +def Slice.subslice_shared (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) := -- TODO: not completely sure here if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then ret ⟨ s.val.slice r.start.val r.end_.val, @@ -327,32 +323,32 @@ def Slice.shared_subslice (α : Type u) (s : Slice α) (r : Range Usize) : Resul fail panic @[pspec] -theorem Slice.shared_subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize) +theorem Slice.subslice_shared_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize) (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) : - ∃ ns, shared_subslice α s r = ret ns ∧ + ∃ ns, subslice_shared α s r = ret ns ∧ ns.val = s.slice r.start.val r.end_.val ∧ (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i)) := by - simp [shared_subslice, *] + simp [subslice_shared, *] intro i _ _ have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac) simp [*] -def Slice.mut_subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) := - Slice.shared_subslice α s r +def Slice.subslice_mut (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) := + Slice.subslice_shared α s r @[pspec] -theorem Slice.mut_subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize) +theorem Slice.subslice_mut_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize) (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) : - ∃ ns, mut_subslice α s r = ret ns ∧ + ∃ ns, subslice_mut α s r = ret ns ∧ ns.val = s.slice r.start.val r.end_.val ∧ (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i)) - := shared_subslice_spec s r h0 h1 + := subslice_shared_spec s r h0 h1 attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse) -def Slice.mut_subslice_back (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) := +def Slice.subslice_mut_back (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) := -- TODO: not completely sure here if h: r.start.val < r.end_.val ∧ r.end_.val ≤ s.length ∧ ss.val.len = r.end_.val - r.start.val then let s_beg := s.val.itake r.start.val @@ -372,13 +368,13 @@ def Slice.mut_subslice_back (α : Type u) (s : Slice α) (r : Range Usize) (ss : fail panic @[pspec] -theorem Slice.mut_subslice_back_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α) +theorem Slice.subslice_mut_back_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α) (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) : - ∃ na, mut_subslice_back α a r ss = ret na ∧ + ∃ na, subslice_mut_back α a r ss = ret na ∧ (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧ (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = ss.index (i - r.start.val)) ∧ (∀ i, r.end_.val ≤ i → i < a.length → na.index i = a.index i) := by - simp [mut_subslice_back, *] + simp [subslice_mut_back, *] have h := List.replace_slice_index r.start.val r.end_.val a.val ss.val (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac) simp [List.replace_slice, *] at h diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index e0a2efea..572b0a24 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -347,20 +347,42 @@ module Sig = struct let slice_subslice_sig (is_mut : bool) = mk_array_slice_subslice_sig false is_mut + + (** Helper: + [fn(&'a [T]) -> usize] + *) + let slice_len_sig : A.fun_sig = + (* The signature fields *) + let region_params = [ region_param_0 ] in + let regions_hierarchy = [ region_group_0 ] (* <'a> *) in + let type_params = [ type_param_0 ] (* *) in + let inputs = + [ mk_ref_ty rvar_0 (mk_slice_ty tvar_0) false (* &'a [T] *) ] + in + let output = mk_usize_ty (* usize *) in + { + region_params; + num_early_bound_regions = 0; + regions_hierarchy; + type_params; + const_generic_params = empty_const_generic_params; + inputs; + output; + } end type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name (** The list of assumed functions and all their information: - their signature - - a boolean indicating whether the function can fail or not + - a boolean indicating whether the function can fail or not (if true: can fail) - their name Rk.: following what is written above, we don't include [Box::free]. - + Remark about the vector functions: for [Vec::len] to be correct and return a [usize], we have to make sure that vectors are bounded by the max usize. - Followingly, [Vec::push] is monadic. + As a consequence, [Vec::push] is monadic. *) let assumed_infos : assumed_info list = let deref_pre = [ "core"; "ops"; "deref" ] in @@ -402,11 +424,11 @@ let assumed_infos : assumed_info list = (* Array to slice*) ( ArrayToSharedSlice, Sig.array_to_slice_sig false, - false, + true, to_name [ "@ArrayToSharedSlice" ] ); ( ArrayToMutSlice, Sig.array_to_slice_sig true, - false, + true, to_name [ "@ArrayToMutSlice" ] ); (* Array Subslice *) ( ArraySharedSubslice, @@ -432,6 +454,7 @@ let assumed_infos : assumed_info list = Sig.slice_subslice_sig true, true, to_name [ "@SliceMutSubslice" ] ); + (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]); ] let get_assumed_info (id : A.assumed_fun_id) : assumed_info = diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 1de7d68b..84d11895 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -261,7 +261,7 @@ let assumed_adts () : (assumed_ty * string) list = let assumed_struct_constructors () : (assumed_ty * string) list = match !backend with - | Lean -> [ (Range, "Range.mk"); (Array, "Array.mk") ] + | Lean -> [ (Range, "Range.mk"); (Array, "Array.make") ] | Coq -> [ (Range, "range.mk"); (Array, "array.mk") ] | FStar -> [ (Range, "mkrange"); (Array, "mkarray") ] | HOL4 -> [ (Range, "mk_range"); (Array, "mk_array") ] @@ -329,21 +329,22 @@ let assumed_llbc_functions () : (VecIndex, rg0, "vec_index_back") (* shouldn't be used *); (VecIndexMut, None, "vec_index_mut_fwd"); (VecIndexMut, rg0, "vec_index_mut_back"); - (ArraySharedIndex, None, "array_index"); - (ArrayMutIndex, None, "array_mut_index_fwd"); - (ArrayMutIndex, rg0, "array_mut_index_back"); + (ArraySharedIndex, None, "array_index_shared"); + (ArrayMutIndex, None, "array_index_mut_fwd"); + (ArrayMutIndex, rg0, "array_index_mut_back"); (ArrayToSharedSlice, None, "array_to_slice"); (ArrayToMutSlice, None, "array_to_mut_slice_fwd"); (ArrayToMutSlice, rg0, "array_to_mut_slice_back"); - (ArraySharedSubslice, None, "array_subslice"); - (ArrayMutSubslice, None, "array_mut_subslice_fwd"); - (ArrayMutSubslice, rg0, "array_mut_subslice_back"); - (SliceSharedIndex, None, "slice_index"); - (SliceMutIndex, None, "slice_mut_index_fwd"); - (SliceMutIndex, rg0, "slice_mut_index_back"); - (SliceSharedSubslice, None, "slice_subslice"); - (SliceMutSubslice, None, "slice_mut_subslice_fwd"); - (SliceMutSubslice, rg0, "slice_mut_subslice_back"); + (ArraySharedSubslice, None, "array_subslice_shared"); + (ArrayMutSubslice, None, "array_subslice_mut_fwd"); + (ArrayMutSubslice, rg0, "array_subslice_mut_back"); + (SliceSharedIndex, None, "slice_index_shared"); + (SliceMutIndex, None, "slice_index_mut_fwd"); + (SliceMutIndex, rg0, "slice_index_mut_back"); + (SliceSharedSubslice, None, "slice_subslice_mut"); + (SliceMutSubslice, None, "slice_subslice_mut_fwd"); + (SliceMutSubslice, rg0, "slice_subslice_mut_back"); + (SliceLen, None, "slice_len_fwd"); ] | Lean -> [ @@ -355,27 +356,28 @@ let assumed_llbc_functions () : (VecInsert, None, "Vec.insert_fwd") (* Shouldn't be used *); (VecInsert, rg0, "Vec.insert"); (VecLen, None, "Vec.len"); - (VecIndex, None, "Vec.index"); - (VecIndex, rg0, "Vec.index_back") (* shouldn't be used *); + (VecIndex, None, "Vec.index_shared"); + (VecIndex, rg0, "Vec.index_shared_back") (* shouldn't be used *); (VecIndexMut, None, "Vec.index_mut"); (VecIndexMut, rg0, "Vec.index_mut_back"); - (* TODO: it would be good to only use Array.index (no Array.mut_index) + (* TODO: it would be good to only use Array.index (no Array.index_mut) (same for subslice, etc.) *) - (ArraySharedIndex, None, "Array.index"); - (ArrayMutIndex, None, "Array.mut_index"); - (ArrayMutIndex, rg0, "Array.mut_index_back"); + (ArraySharedIndex, None, "Array.index_shared"); + (ArrayMutIndex, None, "Array.index_mut"); + (ArrayMutIndex, rg0, "Array.index_mut_back"); (ArrayToSharedSlice, None, "Array.to_slice"); (ArrayToMutSlice, None, "Array.to_mut_slice"); (ArrayToMutSlice, rg0, "Array.to_mut_slice_back"); - (ArraySharedSubslice, None, "Array.subslice"); - (ArrayMutSubslice, None, "Array.mut_subslice"); - (ArrayMutSubslice, rg0, "Array.mut_subslice_back"); - (SliceSharedIndex, None, "Slice.index"); - (SliceMutIndex, None, "Slice.mut_index"); - (SliceMutIndex, rg0, "Slice.mut_index_back"); - (SliceSharedSubslice, None, "Slice.subslice"); - (SliceMutSubslice, None, "Slice.mut_subslice"); - (SliceMutSubslice, rg0, "Slice.mut_subslice_back"); + (ArraySharedSubslice, None, "Array.subslice_shared"); + (ArrayMutSubslice, None, "Array.subslice_mut"); + (ArrayMutSubslice, rg0, "Array.subslice_mut_back"); + (SliceSharedIndex, None, "Slice.index_shared"); + (SliceMutIndex, None, "Slice.index_mut"); + (SliceMutIndex, rg0, "Slice.index_mut_back"); + (SliceSharedSubslice, None, "Slice.subslice_shared"); + (SliceMutSubslice, None, "Slice.subslice_mut"); + (SliceMutSubslice, rg0, "Slice.subslice_mut_back"); + (SliceLen, None, "Slice.len"); ] let assumed_pure_functions () : (pure_assumed_fun_id * string) list = diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 207acef6..157cca38 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -647,7 +647,7 @@ let eval_non_local_function_call_concrete (config : C.config) | ArraySharedIndex | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice | ArraySharedSubslice | ArrayMutSubslice | SliceSharedIndex | SliceMutIndex | SliceSharedSubslice - | SliceMutSubslice -> + | SliceMutSubslice | SliceLen -> raise (Failure "Unimplemented") in diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 43b11aa5..ad7ab05f 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -512,6 +512,7 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string = | ArrayToMutSlice -> "@ArrayToMutSlice" | ArraySharedSubslice -> "@ArraySharedSubslice" | ArrayMutSubslice -> "@ArrayMutSubslice" + | SliceLen -> "@SliceLen" | SliceSharedIndex -> "@SliceSharedIndex" | SliceMutIndex -> "@SliceMutIndex" | SliceSharedSubslice -> "@SliceSharedSubslice" diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 58a5f9e2..52eeee26 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1567,7 +1567,8 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = | VecIndex | VecIndexMut | ArraySharedSubslice | ArrayMutSubslice | SliceSharedIndex | SliceMutIndex | SliceSharedSubslice | SliceMutSubslice | ArraySharedIndex - | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice ), + | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice + | SliceLen ), _ ) -> super#visit_texpression env e) | _ -> super#visit_texpression env e) -- cgit v1.3.1 From 987dc5c25a1d5cee19f4bba2416cbfa83e6ab6de Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 7 Aug 2023 08:59:27 +0200 Subject: Change some fun id names to use "Mut"/"Shared" as a suffix --- compiler/Assumed.ml | 36 +++++++++++------------ compiler/Extract.ml | 60 +++++++++++++++++++-------------------- compiler/InterpreterStatements.ml | 8 +++--- compiler/PrintPure.ml | 20 ++++++------- compiler/PureMicroPasses.ml | 8 +++--- 5 files changed, 66 insertions(+), 66 deletions(-) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 572b0a24..11cd5666 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -416,44 +416,44 @@ let assumed_infos : assumed_info list = true, to_name (index_pre @ [ "IndexMut"; "index_mut" ]) ); (* Array Index *) - ( ArraySharedIndex, + ( ArrayIndexShared, Sig.array_index_sig false, true, - to_name [ "@ArraySharedIndex" ] ); - (ArrayMutIndex, Sig.array_index_sig true, true, to_name [ "@ArrayMutIndex" ]); + to_name [ "@ArrayIndexShared" ] ); + (ArrayIndexMut, Sig.array_index_sig true, true, to_name [ "@ArrayIndexMut" ]); (* Array to slice*) - ( ArrayToSharedSlice, + ( ArrayToSliceShared, Sig.array_to_slice_sig false, true, - to_name [ "@ArrayToSharedSlice" ] ); - ( ArrayToMutSlice, + to_name [ "@ArrayToSliceShared" ] ); + ( ArrayToSliceMut, Sig.array_to_slice_sig true, true, - to_name [ "@ArrayToMutSlice" ] ); + to_name [ "@ArrayToSliceMut" ] ); (* Array Subslice *) - ( ArraySharedSubslice, + ( ArraySubsliceShared, Sig.array_subslice_sig false, true, - to_name [ "@ArraySharedSubslice" ] ); - ( ArrayMutSubslice, + to_name [ "@ArraySubsliceShared" ] ); + ( ArraySubsliceMut, Sig.array_subslice_sig true, true, - to_name [ "@ArrayMutSubslice" ] ); + to_name [ "@ArraySubsliceMut" ] ); (* Slice Index *) - ( SliceSharedIndex, + ( SliceIndexShared, Sig.slice_index_sig false, true, - to_name [ "@SliceSharedIndex" ] ); - (SliceMutIndex, Sig.slice_index_sig true, true, to_name [ "@SliceMutIndex" ]); + to_name [ "@SliceIndexShared" ] ); + (SliceIndexMut, Sig.slice_index_sig true, true, to_name [ "@SliceIndexMut" ]); (* Slice Subslice *) - ( SliceSharedSubslice, + ( SliceSubsliceShared, Sig.slice_subslice_sig false, true, - to_name [ "@SliceSharedSubslice" ] ); - ( SliceMutSubslice, + to_name [ "@SliceSubsliceShared" ] ); + ( SliceSubsliceMut, Sig.slice_subslice_sig true, true, - to_name [ "@SliceMutSubslice" ] ); + to_name [ "@SliceSubsliceMut" ] ); (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]); ] diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 297c182a..c4238d83 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -329,21 +329,21 @@ let assumed_llbc_functions () : (VecIndex, rg0, "vec_index_back") (* shouldn't be used *); (VecIndexMut, None, "vec_index_mut_fwd"); (VecIndexMut, rg0, "vec_index_mut_back"); - (ArraySharedIndex, None, "array_index_shared"); - (ArrayMutIndex, None, "array_index_mut_fwd"); - (ArrayMutIndex, rg0, "array_index_mut_back"); - (ArrayToSharedSlice, None, "array_to_slice_shared"); - (ArrayToMutSlice, None, "array_to_slice_mut_fwd"); - (ArrayToMutSlice, rg0, "array_to_slice_mut_back"); - (ArraySharedSubslice, None, "array_subslice_shared"); - (ArrayMutSubslice, None, "array_subslice_mut_fwd"); - (ArrayMutSubslice, rg0, "array_subslice_mut_back"); - (SliceSharedIndex, None, "slice_index_shared"); - (SliceMutIndex, None, "slice_index_mut_fwd"); - (SliceMutIndex, rg0, "slice_index_mut_back"); - (SliceSharedSubslice, None, "slice_subslice_shared"); - (SliceMutSubslice, None, "slice_subslice_mut_fwd"); - (SliceMutSubslice, rg0, "slice_subslice_mut_back"); + (ArrayIndexShared, None, "array_index_shared"); + (ArrayIndexMut, None, "array_index_mut_fwd"); + (ArrayIndexMut, rg0, "array_index_mut_back"); + (ArrayToSliceShared, None, "array_to_slice_shared"); + (ArrayToSliceMut, None, "array_to_slice_mut_fwd"); + (ArrayToSliceMut, rg0, "array_to_slice_mut_back"); + (ArraySubsliceShared, None, "array_subslice_shared"); + (ArraySubsliceMut, None, "array_subslice_mut_fwd"); + (ArraySubsliceMut, rg0, "array_subslice_mut_back"); + (SliceIndexShared, None, "slice_index_shared"); + (SliceIndexMut, None, "slice_index_mut_fwd"); + (SliceIndexMut, rg0, "slice_index_mut_back"); + (SliceSubsliceShared, None, "slice_subslice_shared"); + (SliceSubsliceMut, None, "slice_subslice_mut_fwd"); + (SliceSubsliceMut, rg0, "slice_subslice_mut_back"); (SliceLen, None, "slice_len"); ] | Lean -> @@ -360,21 +360,21 @@ let assumed_llbc_functions () : (VecIndex, rg0, "Vec.index_shared_back") (* shouldn't be used *); (VecIndexMut, None, "Vec.index_mut"); (VecIndexMut, rg0, "Vec.index_mut_back"); - (ArraySharedIndex, None, "Array.index_shared"); - (ArrayMutIndex, None, "Array.index_mut"); - (ArrayMutIndex, rg0, "Array.index_mut_back"); - (ArrayToSharedSlice, None, "Array.to_slice_shared"); - (ArrayToMutSlice, None, "Array.to_slice_mut"); - (ArrayToMutSlice, rg0, "Array.to_slice_mut_back"); - (ArraySharedSubslice, None, "Array.subslice_shared"); - (ArrayMutSubslice, None, "Array.subslice_mut"); - (ArrayMutSubslice, rg0, "Array.subslice_mut_back"); - (SliceSharedIndex, None, "Slice.index_shared"); - (SliceMutIndex, None, "Slice.index_mut"); - (SliceMutIndex, rg0, "Slice.index_mut_back"); - (SliceSharedSubslice, None, "Slice.subslice_shared"); - (SliceMutSubslice, None, "Slice.subslice_mut"); - (SliceMutSubslice, rg0, "Slice.subslice_mut_back"); + (ArrayIndexShared, None, "Array.index_shared"); + (ArrayIndexMut, None, "Array.index_mut"); + (ArrayIndexMut, rg0, "Array.index_mut_back"); + (ArrayToSliceShared, None, "Array.to_slice_shared"); + (ArrayToSliceMut, None, "Array.to_slice_mut"); + (ArrayToSliceMut, rg0, "Array.to_slice_mut_back"); + (ArraySubsliceShared, None, "Array.subslice_shared"); + (ArraySubsliceMut, None, "Array.subslice_mut"); + (ArraySubsliceMut, rg0, "Array.subslice_mut_back"); + (SliceIndexShared, None, "Slice.index_shared"); + (SliceIndexMut, None, "Slice.index_mut"); + (SliceIndexMut, rg0, "Slice.index_mut_back"); + (SliceSubsliceShared, None, "Slice.subslice_shared"); + (SliceSubsliceMut, None, "Slice.subslice_mut"); + (SliceSubsliceMut, rg0, "Slice.subslice_mut_back"); (SliceLen, None, "Slice.len"); ] diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 157cca38..045c4484 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -644,10 +644,10 @@ let eval_non_local_function_call_concrete (config : C.config) | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut -> eval_vec_function_concrete config fid region_params type_params cg_params - | ArraySharedIndex | ArrayMutIndex | ArrayToSharedSlice - | ArrayToMutSlice | ArraySharedSubslice | ArrayMutSubslice - | SliceSharedIndex | SliceMutIndex | SliceSharedSubslice - | SliceMutSubslice | SliceLen -> + | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared + | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut + | SliceIndexShared | SliceIndexMut | SliceSubsliceShared + | SliceSubsliceMut | SliceLen -> raise (Failure "Unimplemented") in diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index ad7ab05f..cfb63ec2 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -506,17 +506,17 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string = | A.VecLen -> "alloc::vec::Vec::len" | A.VecIndex -> "core::ops::index::Index::index" | A.VecIndexMut -> "core::ops::index::IndexMut::index_mut" - | ArraySharedIndex -> "@ArraySharedIndex" - | ArrayMutIndex -> "@ArrayMutIndex" - | ArrayToSharedSlice -> "@ArrayToSharedSlice" - | ArrayToMutSlice -> "@ArrayToMutSlice" - | ArraySharedSubslice -> "@ArraySharedSubslice" - | ArrayMutSubslice -> "@ArrayMutSubslice" + | ArrayIndexShared -> "@ArrayIndexShared" + | ArrayIndexMut -> "@ArrayIndexMut" + | ArrayToSliceShared -> "@ArrayToSliceShared" + | ArrayToSliceMut -> "@ArrayToSliceMut" + | ArraySubsliceShared -> "@ArraySubsliceShared" + | ArraySubsliceMut -> "@ArraySubsliceMut" | SliceLen -> "@SliceLen" - | SliceSharedIndex -> "@SliceSharedIndex" - | SliceMutIndex -> "@SliceMutIndex" - | SliceSharedSubslice -> "@SliceSharedSubslice" - | SliceMutSubslice -> "@SliceMutSubslice" + | SliceIndexShared -> "@SliceIndexShared" + | SliceIndexMut -> "@SliceIndexMut" + | SliceSubsliceShared -> "@SliceSubsliceShared" + | SliceSubsliceMut -> "@SliceSubsliceMut" let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string = match fid with diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 52eeee26..b6025df4 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1564,10 +1564,10 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = assert (args = []); mk_unit_rvalue | ( ( A.Replace | VecNew | VecPush | VecInsert | VecLen - | VecIndex | VecIndexMut | ArraySharedSubslice - | ArrayMutSubslice | SliceSharedIndex | SliceMutIndex - | SliceSharedSubslice | SliceMutSubslice | ArraySharedIndex - | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice + | VecIndex | VecIndexMut | ArraySubsliceShared + | ArraySubsliceMut | SliceIndexShared | SliceIndexMut + | SliceSubsliceShared | SliceSubsliceMut | ArrayIndexShared + | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | SliceLen ), _ ) -> super#visit_texpression env e) -- cgit v1.3.1