diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Primitives/ArraySlice.lean | 128 | ||||
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 32 |
2 files changed, 88 insertions, 72 deletions
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index 2a080ca6..cfc9a6b2 100644 --- a/backends/lean/Base/Primitives/ArraySlice.lean +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -341,110 +341,110 @@ theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) ( structure core.slice.index.private_slice_index.Sealed (Self : Type) where /- Trait declaration: [core::slice::index::SliceIndex] -/ -structure core.slice.index.SliceIndex (Self T0 : Type) where +structure core.slice.index.SliceIndex (Self T : Type) where sealedInst : core.slice.index.private_slice_index.Sealed Self Output : Type - get : Self → T0 → Result (Option Output) - get_mut : Self → T0 → Result (Option Output) - get_mut_back : Self → T0 → Option Output → Result T0 - get_unchecked : Self → ConstRawPtr T0 → Result (ConstRawPtr Output) - get_unchecked_mut : Self → MutRawPtr T0 → Result (MutRawPtr Output) - index : Self → T0 → Result Output - index_mut : Self → T0 → Result Output - index_mut_back : Self → T0 → Output → Result T0 + get : Self → T → Result (Option Output) + get_mut : Self → T → Result (Option Output) + get_mut_back : Self → T → Option Output → Result T + get_unchecked : Self → ConstRawPtr T → Result (ConstRawPtr Output) + get_unchecked_mut : Self → MutRawPtr T → Result (MutRawPtr Output) + index : Self → T → Result Output + index_mut : Self → T → Result Output + index_mut_back : Self → T → Output → Result T /- [core::slice::index::[T]::index]: forward function -/ def core.slice.index.Slice.index - (T0 I : Type) (inst : core.slice.index.SliceIndex I (Slice T0)) - (slice : Slice T0) (i : I) : Result inst.Output := do + (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) + (slice : Slice T) (i : I) : Result inst.Output := do let x ← inst.get i slice match x with | none => fail panic | some x => ret x /- [core::slice::index::Range:::get]: forward function -/ -def core.slice.index.Range.get (T0 : Type) (i : Range Usize) (slice : Slice T0) : - Result (Option (Slice T0)) := +def core.slice.index.Range.get (T : Type) (i : Range Usize) (slice : Slice T) : + Result (Option (Slice T)) := sorry -- TODO /- [core::slice::index::Range::get_mut]: forward function -/ def core.slice.index.Range.get_mut - (T0 : Type) : Range Usize → Slice T0 → Result (Option (Slice T0)) := + (T : Type) : Range Usize → Slice T → Result (Option (Slice T)) := sorry -- TODO /- [core::slice::index::Range::get_mut]: backward function 0 -/ def core.slice.index.Range.get_mut_back - (T0 : Type) : - Range Usize → Slice T0 → Option (Slice T0) → Result (Slice T0) := + (T : Type) : + Range Usize → Slice T → Option (Slice T) → Result (Slice T) := sorry -- TODO /- [core::slice::index::Range::get_unchecked]: forward function -/ def core.slice.index.Range.get_unchecked - (T0 : Type) : - Range Usize → ConstRawPtr (Slice T0) → Result (ConstRawPtr (Slice T0)) := + (T : Type) : + Range Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr (Slice T)) := -- Don't know what the model should be - for now we always fail to make -- sure code which uses it fails fun _ _ => fail panic /- [core::slice::index::Range::get_unchecked_mut]: forward function -/ def core.slice.index.Range.get_unchecked_mut - (T0 : Type) : - Range Usize → MutRawPtr (Slice T0) → Result (MutRawPtr (Slice T0)) := + (T : Type) : + Range Usize → MutRawPtr (Slice T) → Result (MutRawPtr (Slice T)) := -- Don't know what the model should be - for now we always fail to make -- sure code which uses it fails fun _ _ => fail panic /- [core::slice::index::Range::index]: forward function -/ def core.slice.index.Range.index - (T0 : Type) : Range Usize → Slice T0 → Result (Slice T0) := + (T : Type) : Range Usize → Slice T → Result (Slice T) := sorry -- TODO /- [core::slice::index::Range::index_mut]: forward function -/ def core.slice.index.Range.index_mut - (T0 : Type) : Range Usize → Slice T0 → Result (Slice T0) := + (T : Type) : Range Usize → Slice T → Result (Slice T) := sorry -- TODO /- [core::slice::index::Range::index_mut]: backward function 0 -/ def core.slice.index.Range.index_mut_back - (T0 : Type) : Range Usize → Slice T0 → Slice T0 → Result (Slice T0) := + (T : Type) : Range Usize → Slice T → Slice T → Result (Slice T) := sorry -- TODO /- [core::slice::index::[T]::index_mut]: forward function -/ def core.slice.index.Slice.index_mut - (T0 I : Type) (inst : core.slice.index.SliceIndex I (Slice T0)) : - Slice T0 → I → Result inst.Output := + (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) : + Slice T → I → Result inst.Output := sorry -- TODO /- [core::slice::index::[T]::index_mut]: backward function 0 -/ def core.slice.index.Slice.index_mut_back - (T0 I : Type) (inst : core.slice.index.SliceIndex I (Slice T0)) : - Slice T0 → I → inst.Output → Result (Slice T0) := + (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) : + Slice T → I → inst.Output → Result (Slice T) := sorry -- TODO /- [core::array::[T; N]::index]: forward function -/ def core.array.Array.index - (T0 I : Type) (N : Usize) (inst : core.ops.index.Index (Slice T0) I) : - Array T0 N → I → Result inst.Output := + (T I : Type) (N : Usize) (inst : core.ops.index.Index (Slice T) I) + (a : Array T N) (i : I) : Result inst.Output := sorry -- TODO /- [core::array::[T; N]::index_mut]: forward function -/ def core.array.Array.index_mut - (T0 I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T0) I) : - Array T0 N → I → Result inst.indexInst.Output := + (T I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T) I) + (a : Array T N) (i : I) : Result inst.indexInst.Output := sorry -- TODO /- [core::array::[T; N]::index_mut]: backward function 0 -/ def core.array.Array.index_mut_back - (T0 I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T0) I) : - Array T0 N → I → inst.indexInst.Output → Result (Array T0 N) := + (T I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T) I) + (a : Array T N) (i : I) (x : inst.indexInst.Output) : Result (Array T N) := sorry -- TODO /- Trait implementation: [core::slice::index::[T]] -/ -def core.slice.index.Slice.coreopsindexIndexInst (T0 I : Type) - (inst : core.slice.index.SliceIndex I (Slice T0)) : - core.ops.index.Index (Slice T0) I := { +def core.slice.index.Slice.coreopsindexIndexInst (T I : Type) + (inst : core.slice.index.SliceIndex I (Slice T)) : + core.ops.index.Index (Slice T) I := { Output := inst.Output - index := core.slice.index.Slice.index T0 I inst + index := core.slice.index.Slice.index T I inst } /- Trait implementation: [core::slice::index::private_slice_index::Range] -/ @@ -452,45 +452,45 @@ def core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_index : core.slice.index.private_slice_index.Sealed (Range Usize) := {} /- Trait implementation: [core::slice::index::Range] -/ -def core.slice.index.Range.coresliceindexSliceIndexInst (T0 : Type) : - core.slice.index.SliceIndex (Range Usize) (Slice T0) := { +def core.slice.index.Range.coresliceindexSliceIndexInst (T : Type) : + core.slice.index.SliceIndex (Range Usize) (Slice T) := { sealedInst := core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst - Output := Slice T0 - get := core.slice.index.Range.get T0 - get_mut := core.slice.index.Range.get_mut T0 - get_mut_back := core.slice.index.Range.get_mut_back T0 - get_unchecked := core.slice.index.Range.get_unchecked T0 - get_unchecked_mut := core.slice.index.Range.get_unchecked_mut T0 - index := core.slice.index.Range.index T0 - index_mut := core.slice.index.Range.index_mut T0 - index_mut_back := core.slice.index.Range.index_mut_back T0 + Output := Slice T + get := core.slice.index.Range.get T + get_mut := core.slice.index.Range.get_mut T + get_mut_back := core.slice.index.Range.get_mut_back T + get_unchecked := core.slice.index.Range.get_unchecked T + get_unchecked_mut := core.slice.index.Range.get_unchecked_mut T + index := core.slice.index.Range.index T + index_mut := core.slice.index.Range.index_mut T + index_mut_back := core.slice.index.Range.index_mut_back T } /- Trait implementation: [core::slice::index::[T]] -/ -def core.slice.index.Slice.coreopsindexIndexMutInst (T0 I : Type) - (inst : core.slice.index.SliceIndex I (Slice T0)) : - core.ops.index.IndexMut (Slice T0) I := { - indexInst := core.slice.index.Slice.coreopsindexIndexInst T0 I inst - index_mut := core.slice.index.Slice.index_mut T0 I inst - index_mut_back := core.slice.index.Slice.index_mut_back T0 I inst +def core.slice.index.Slice.coreopsindexIndexMutInst (T I : Type) + (inst : core.slice.index.SliceIndex I (Slice T)) : + core.ops.index.IndexMut (Slice T) I := { + indexInst := core.slice.index.Slice.coreopsindexIndexInst T I inst + index_mut := core.slice.index.Slice.index_mut T I inst + index_mut_back := core.slice.index.Slice.index_mut_back T I inst } /- Trait implementation: [core::array::[T; N]] -/ -def core.array.Array.coreopsindexIndexInst (T0 I : Type) (N : Usize) - (inst : core.ops.index.Index (Slice T0) I) : - core.ops.index.Index (Array T0 N) I := { +def core.array.Array.coreopsindexIndexInst (T I : Type) (N : Usize) + (inst : core.ops.index.Index (Slice T) I) : + core.ops.index.Index (Array T N) I := { Output := inst.Output - index := core.array.Array.index T0 I N inst + index := core.array.Array.index T I N inst } /- Trait implementation: [core::array::[T; N]] -/ -def core.array.Array.coreopsindexIndexMutInst (T0 I : Type) (N : Usize) - (inst : core.ops.index.IndexMut (Slice T0) I) : - core.ops.index.IndexMut (Array T0 N) I := { - indexInst := core.array.Array.coreopsindexIndexInst T0 I N inst.indexInst - index_mut := core.array.Array.index_mut T0 I N inst - index_mut_back := core.array.Array.index_mut_back T0 I N inst +def core.array.Array.coreopsindexIndexMutInst (T I : Type) (N : Usize) + (inst : core.ops.index.IndexMut (Slice T) I) : + core.ops.index.IndexMut (Array T N) I := { + indexInst := core.array.Array.coreopsindexIndexInst T I N inst.indexInst + index_mut := core.array.Array.index_mut T I N inst + index_mut_back := core.array.Array.index_mut_back T I N inst } /- [core::slice::index::usize::get]: forward function -/ diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 8fcdea56..afa0dd6f 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -528,12 +528,18 @@ module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd) let builtin_trait_impls_info () : ((string list * string list) * (bool list option * string)) list = - let fmt (type_name : string list) (trait_name : string list) - ?(filter : bool list option = None) () : + let fmt (type_name : string list) + ?(extract_type_name : string list option = None) + (trait_name : string list) ?(filter : bool list option = None) () : (string list * string list) * (bool list option * string) = let name = let trait_name = String.concat "" trait_name ^ "Inst" in let sep = backend_choice "_" "." in + let type_name = + match extract_type_name with + | Some type_name -> type_name + | None -> type_name + in String.concat sep type_name ^ sep ^ trait_name in ((type_name, trait_name), (filter, name)) @@ -547,8 +553,15 @@ let builtin_trait_impls_info () : (* core::ops::index::Index<[T], I> *) fmt [ "core"; "slice"; "index"; "[T]" ] + ~extract_type_name:(Some [ "core"; "slice"; "index"; "Slice" ]) [ "core"; "ops"; "index"; "Index" ] (); + (* core::ops::index::IndexMut<[T], I> *) + fmt + [ "core"; "slice"; "index"; "[T]" ] + ~extract_type_name:(Some [ "core"; "slice"; "index"; "Slice" ]) + [ "core"; "ops"; "index"; "IndexMut" ] + (); (* core::slice::index::private_slice_index::Sealed<Range<usize>> *) fmt [ "core"; "slice"; "index"; "private_slice_index"; "Range" ] @@ -559,15 +572,18 @@ let builtin_trait_impls_info () : [ "core"; "slice"; "index"; "Range" ] [ "core"; "slice"; "index"; "SliceIndex" ] (); - (* core::ops::index::IndexMut<[T], I> *) + (* core::ops::index::Index<[T; N], I> *) fmt - [ "core"; "slice"; "index"; "[T]" ] - [ "core"; "ops"; "index"; "IndexMut" ] + [ "core"; "array"; "[T; N]" ] + ~extract_type_name:(Some [ "core"; "array"; "Array" ]) + [ "core"; "ops"; "index"; "Index" ] (); - (* core::ops::index::Index<[T; N], I> *) - fmt [ "core"; "array"; "[T; N]" ] [ "core"; "ops"; "index"; "Index" ] (); (* core::ops::index::IndexMut<[T; N], I> *) - fmt [ "core"; "array"; "[T; N]" ] [ "core"; "ops"; "index"; "IndexMut" ] (); + fmt + [ "core"; "array"; "[T; N]" ] + ~extract_type_name:(Some [ "core"; "array"; "Array" ]) + [ "core"; "ops"; "index"; "IndexMut" ] + (); (* core::slice::index::private_slice_index::Sealed<usize> *) fmt [ "core"; "slice"; "index"; "private_slice_index"; "usize" ] |