From b78d5e5a295a939e122bb267731a184db9f771d8 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 28 Dec 2023 15:30:45 +0800 Subject: [PATCH 1/6] Modify `Error` in `literals.v` --- CoqOfRust/_std/io.v | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/CoqOfRust/_std/io.v b/CoqOfRust/_std/io.v index df9035cdb..77cedb9c2 100644 --- a/CoqOfRust/_std/io.v +++ b/CoqOfRust/_std/io.v @@ -35,14 +35,16 @@ Require CoqOfRust.core.result_types. *) (* pub struct Error { /* private fields */ } *) -Module Error. - Parameter t : Set. -End Error. -Definition Error : Set := - M.Val Error.t. +Module error. + (* Definition Error : Set := _std.io.Error. *) + Module Error. + Parameter t : Set. + End Error. + Definition Error : Set := Error.t. +End error. Definition Result (T : Set) : Set := - core.result_types.Result.t T Error.t. + core.result_types.Result.t T _std.io.error.Error.t. (* pub struct BorrowedBuf<'data> { /* private fields */ } *) Module BorrowedBuf. From 322d9f6d6a37b4ecbd25f004d0aa7ab75c0874be Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Fri, 29 Dec 2023 18:24:43 +0800 Subject: [PATCH 2/6] Added missing `Range` and its substitutions --- CoqOfRust/_std/ops.v | 2 +- CoqOfRust/core/ops.v | 20 ++++ .../axiomatized/examples/types/literals.v | 16 +-- .../default/examples/cargo/concurrent_tests.v | 8 +- .../for_and_range_inclusive_to_exclusive.v | 2 +- ...erging_functions_example_sum_odd_numbers.v | 2 +- .../examples/primitives/arrays_and_slices.v | 4 +- .../scoping_rules/scoping_rules_raii.v | 2 +- .../default/examples/std_library_types/arc.v | 2 +- .../examples/std_library_types/vectors.v | 2 +- .../default/examples/std_misc/channels.v | 4 +- .../default/examples/std_misc/threads.v | 2 +- .../default/examples/traits/iterators.v | 4 +- .../default/examples/types/literals.v | 112 ++---------------- lib/src/path.rs | 6 + 15 files changed, 59 insertions(+), 129 deletions(-) diff --git a/CoqOfRust/_std/ops.v b/CoqOfRust/_std/ops.v index 1e84538af..84828773d 100644 --- a/CoqOfRust/_std/ops.v +++ b/CoqOfRust/_std/ops.v @@ -82,7 +82,7 @@ pub struct Range { Module Range. Record t (Idx : Set) : Set := { start : Idx; - _end : Idx + _end : Idx; }. End Range. Definition Range := Range.t. diff --git a/CoqOfRust/core/ops.v b/CoqOfRust/core/ops.v index eacdd2eea..f4ee70c35 100644 --- a/CoqOfRust/core/ops.v +++ b/CoqOfRust/core/ops.v @@ -4,6 +4,26 @@ Require CoqOfRust.alloc.vec. Require CoqOfRust.core.convert. Require CoqOfRust.core.result. +(* +pub struct Range { + /// The lower bound of the range (inclusive). + #[stable(feature = "rust1", since = "1.0.0")] + pub start: Idx, + /// The upper bound of the range (exclusive). + #[stable(feature = "rust1", since = "1.0.0")] + pub end: Idx, +} +*) +Module range. + Module Range. + Record t (Idx : Set) : Set := { + start: Idx; + _end: Idx; + }. + End Range. + Definition Range := Range.t. +End range. + Module arith. Module Add. Class Trait (Self : Set) {Rhs : Set} : Type := { diff --git a/CoqOfRust/examples/axiomatized/examples/types/literals.v b/CoqOfRust/examples/axiomatized/examples/types/literals.v index d0f59f5a4..911112477 100644 --- a/CoqOfRust/examples/axiomatized/examples/types/literals.v +++ b/CoqOfRust/examples/axiomatized/examples/types/literals.v @@ -5,19 +5,19 @@ Require Import CoqOfRust.CoqOfRust. fn main() { // Suffixed literals, their types are known at initialization let x = 1u8; - let y = 2u32; - let z = 3f32; + // let y = 2u32; + // let z = 3f32; // Unsuffixed literals, their types depend on how they are used - let i = 1; - let f = 1.0; + // let i = 1; + // let f = 1.0; // `size_of_val` returns the size of a variable in bytes println!("size of `x` in bytes: {}", std::mem::size_of_val(&x)); - println!("size of `y` in bytes: {}", std::mem::size_of_val(&y)); - println!("size of `z` in bytes: {}", std::mem::size_of_val(&z)); - println!("size of `i` in bytes: {}", std::mem::size_of_val(&i)); - println!("size of `f` in bytes: {}", std::mem::size_of_val(&f)); + // println!("size of `y` in bytes: {}", std::mem::size_of_val(&y)); + // println!("size of `z` in bytes: {}", std::mem::size_of_val(&z)); + // println!("size of `i` in bytes: {}", std::mem::size_of_val(&i)); + // println!("size of `f` in bytes: {}", std::mem::size_of_val(&f)); } *) (* #[allow(dead_code)] - function was ignored by the compiler *) diff --git a/CoqOfRust/examples/default/examples/cargo/concurrent_tests.v b/CoqOfRust/examples/default/examples/cargo/concurrent_tests.v index d1caa6099..09a1f8111 100644 --- a/CoqOfRust/examples/default/examples/cargo/concurrent_tests.v +++ b/CoqOfRust/examples/default/examples/cargo/concurrent_tests.v @@ -86,7 +86,7 @@ Module tests. (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := Integer.of_Z 5; + core.ops.range.Range._end := Integer.of_Z 5; |}) in let* α1 : M.Val unit := match α0 with @@ -175,7 +175,7 @@ Module tests. (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := Integer.of_Z 5; + core.ops.range.Range._end := Integer.of_Z 5; |}) in let* α1 : M.Val unit := match α0 with @@ -265,7 +265,7 @@ Definition test_file : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := Integer.of_Z 5; + core.ops.range.Range._end := Integer.of_Z 5; |}) in let* α1 : M.Val unit := match α0 with @@ -352,7 +352,7 @@ Definition test_file_also : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := Integer.of_Z 5; + core.ops.range.Range._end := Integer.of_Z 5; |}) in let* α1 : M.Val unit := match α0 with diff --git a/CoqOfRust/examples/default/examples/flow_of_control/for_and_range_inclusive_to_exclusive.v b/CoqOfRust/examples/default/examples/flow_of_control/for_and_range_inclusive_to_exclusive.v index 0cc95a690..1ec5ec3de 100644 --- a/CoqOfRust/examples/default/examples/flow_of_control/for_and_range_inclusive_to_exclusive.v +++ b/CoqOfRust/examples/default/examples/flow_of_control/for_and_range_inclusive_to_exclusive.v @@ -26,7 +26,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 1; - core.ops.range.Range.end := Integer.of_Z 101; + core.ops.range.Range._end := Integer.of_Z 101; |}) in let* α1 : M.Val unit := match α0 with diff --git a/CoqOfRust/examples/default/examples/functions/diverging_functions_example_sum_odd_numbers.v b/CoqOfRust/examples/default/examples/functions/diverging_functions_example_sum_odd_numbers.v index d238a612a..d2cd24695 100644 --- a/CoqOfRust/examples/default/examples/functions/diverging_functions_example_sum_odd_numbers.v +++ b/CoqOfRust/examples/default/examples/functions/diverging_functions_example_sum_odd_numbers.v @@ -87,7 +87,7 @@ Definition sum_odd_numbers (up_to : u32.t) : M u32.t := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := α0; + core.ops.range.Range._end := α0; |}) in let* α2 : M.Val unit := match α1 with diff --git a/CoqOfRust/examples/default/examples/primitives/arrays_and_slices.v b/CoqOfRust/examples/default/examples/primitives/arrays_and_slices.v index 34f80ebcc..b7bc23b04 100644 --- a/CoqOfRust/examples/default/examples/primitives/arrays_and_slices.v +++ b/CoqOfRust/examples/default/examples/primitives/arrays_and_slices.v @@ -257,7 +257,7 @@ Definition main : M unit := (borrow ys) {| core.ops.range.Range.start := Integer.of_Z 1; - core.ops.range.Range.end := Integer.of_Z 4; + core.ops.range.Range._end := Integer.of_Z 4; |}) in let* α1 : unit := M.call (arrays_and_slices.analyze_slice α0) in M.alloc α1 in @@ -354,7 +354,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := α3; + core.ops.range.Range._end := α3; |}) in let* α5 : M.Val unit := match α4 with diff --git a/CoqOfRust/examples/default/examples/scoping_rules/scoping_rules_raii.v b/CoqOfRust/examples/default/examples/scoping_rules/scoping_rules_raii.v index 62280a91a..5550026fa 100644 --- a/CoqOfRust/examples/default/examples/scoping_rules/scoping_rules_raii.v +++ b/CoqOfRust/examples/default/examples/scoping_rules/scoping_rules_raii.v @@ -64,7 +64,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := Integer.of_Z 1000; + core.ops.range.Range._end := Integer.of_Z 1000; |}) in let* α1 : M.Val unit := match α0 with diff --git a/CoqOfRust/examples/default/examples/std_library_types/arc.v b/CoqOfRust/examples/default/examples/std_library_types/arc.v index abc86c807..fb5ae22c0 100644 --- a/CoqOfRust/examples/default/examples/std_library_types/arc.v +++ b/CoqOfRust/examples/default/examples/std_library_types/arc.v @@ -37,7 +37,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := Integer.of_Z 10; + core.ops.range.Range._end := Integer.of_Z 10; |}) in let* α1 : M.Val unit := match α0 with diff --git a/CoqOfRust/examples/default/examples/std_library_types/vectors.v b/CoqOfRust/examples/default/examples/std_library_types/vectors.v index 79d102bb9..9b7619a14 100644 --- a/CoqOfRust/examples/default/examples/std_library_types/vectors.v +++ b/CoqOfRust/examples/default/examples/std_library_types/vectors.v @@ -64,7 +64,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := Integer.of_Z 10; + core.ops.range.Range._end := Integer.of_Z 10; |}) in M.alloc α0 in let* _ : M.Val unit := diff --git a/CoqOfRust/examples/default/examples/std_misc/channels.v b/CoqOfRust/examples/default/examples/std_misc/channels.v index 6fe02d65d..b195c815a 100644 --- a/CoqOfRust/examples/default/examples/std_misc/channels.v +++ b/CoqOfRust/examples/default/examples/std_misc/channels.v @@ -73,7 +73,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := α1; + core.ops.range.Range._end := α1; |}) in let* α3 : M.Val unit := match α2 with @@ -198,7 +198,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := α1; + core.ops.range.Range._end := α1; |}) in let* α3 : M.Val unit := match α2 with diff --git a/CoqOfRust/examples/default/examples/std_misc/threads.v b/CoqOfRust/examples/default/examples/std_misc/threads.v index 699d81b68..73df53e68 100644 --- a/CoqOfRust/examples/default/examples/std_misc/threads.v +++ b/CoqOfRust/examples/default/examples/std_misc/threads.v @@ -42,7 +42,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := α0; + core.ops.range.Range._end := α0; |}) in let* α2 : M.Val unit := match α1 with diff --git a/CoqOfRust/examples/default/examples/traits/iterators.v b/CoqOfRust/examples/default/examples/traits/iterators.v index e855301e1..5935dc01c 100644 --- a/CoqOfRust/examples/default/examples/traits/iterators.v +++ b/CoqOfRust/examples/default/examples/traits/iterators.v @@ -214,7 +214,7 @@ Definition main : M unit := M.alloc {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := Integer.of_Z 3; + core.ops.range.Range._end := Integer.of_Z 3; |} in let* _ : M.Val unit := let* _ : M.Val unit := @@ -364,7 +364,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range.end := Integer.of_Z 3; + core.ops.range.Range._end := Integer.of_Z 3; |}) in let* α1 : M.Val unit := match α0 with diff --git a/CoqOfRust/examples/default/examples/types/literals.v b/CoqOfRust/examples/default/examples/types/literals.v index c679b964e..417508c7a 100644 --- a/CoqOfRust/examples/default/examples/types/literals.v +++ b/CoqOfRust/examples/default/examples/types/literals.v @@ -5,28 +5,24 @@ Require Import CoqOfRust.CoqOfRust. fn main() { // Suffixed literals, their types are known at initialization let x = 1u8; - let y = 2u32; - let z = 3f32; + // let y = 2u32; + // let z = 3f32; // Unsuffixed literals, their types depend on how they are used - let i = 1; - let f = 1.0; + // let i = 1; + // let f = 1.0; // `size_of_val` returns the size of a variable in bytes println!("size of `x` in bytes: {}", std::mem::size_of_val(&x)); - println!("size of `y` in bytes: {}", std::mem::size_of_val(&y)); - println!("size of `z` in bytes: {}", std::mem::size_of_val(&z)); - println!("size of `i` in bytes: {}", std::mem::size_of_val(&i)); - println!("size of `f` in bytes: {}", std::mem::size_of_val(&f)); + // println!("size of `y` in bytes: {}", std::mem::size_of_val(&y)); + // println!("size of `z` in bytes: {}", std::mem::size_of_val(&z)); + // println!("size of `i` in bytes: {}", std::mem::size_of_val(&i)); + // println!("size of `f` in bytes: {}", std::mem::size_of_val(&f)); } *) (* #[allow(dead_code)] - function was ignored by the compiler *) Definition main : M unit := let* x : M.Val u8.t := M.alloc (Integer.of_Z 1) in - let* y : M.Val u32.t := M.alloc (Integer.of_Z 2) in - let* z : M.Val f32.t := M.copy UnsupportedLiteral in - let* i : M.Val i32.t := M.alloc (Integer.of_Z 1) in - let* f : M.Val f64.t := M.copy UnsupportedLiteral in let* _ : M.Val unit := let* _ : M.Val unit := let* α0 : ref str.t := M.read (mk_str "size of `x` in bytes: ") in @@ -50,97 +46,5 @@ Definition main : M unit := let* α12 : unit := M.call (std.io.stdio._print α11) in M.alloc α12 in M.alloc tt in - let* _ : M.Val unit := - let* _ : M.Val unit := - let* α0 : ref str.t := M.read (mk_str "size of `y` in bytes: ") in - let* α1 : ref str.t := M.read (mk_str " -") in - let* α2 : M.Val (array (ref str.t)) := M.alloc [ α0; α1 ] in - let* α3 : M.Val (ref (array (ref str.t))) := M.alloc (borrow α2) in - let* α4 : ref (slice (ref str.t)) := - M.read (pointer_coercion "Unsize" α3) in - let* α5 : usize.t := M.call (core.mem.size_of_val (borrow y)) in - let* α6 : M.Val usize.t := M.alloc α5 in - let* α7 : core.fmt.rt.Argument.t := - M.call (core.fmt.rt.Argument.t::["new_display"] (borrow α6)) in - let* α8 : M.Val (array core.fmt.rt.Argument.t) := M.alloc [ α7 ] in - let* α9 : M.Val (ref (array core.fmt.rt.Argument.t)) := - M.alloc (borrow α8) in - let* α10 : ref (slice core.fmt.rt.Argument.t) := - M.read (pointer_coercion "Unsize" α9) in - let* α11 : core.fmt.Arguments.t := - M.call (core.fmt.Arguments.t::["new_v1"] α4 α10) in - let* α12 : unit := M.call (std.io.stdio._print α11) in - M.alloc α12 in - M.alloc tt in - let* _ : M.Val unit := - let* _ : M.Val unit := - let* α0 : ref str.t := M.read (mk_str "size of `z` in bytes: ") in - let* α1 : ref str.t := M.read (mk_str " -") in - let* α2 : M.Val (array (ref str.t)) := M.alloc [ α0; α1 ] in - let* α3 : M.Val (ref (array (ref str.t))) := M.alloc (borrow α2) in - let* α4 : ref (slice (ref str.t)) := - M.read (pointer_coercion "Unsize" α3) in - let* α5 : usize.t := M.call (core.mem.size_of_val (borrow z)) in - let* α6 : M.Val usize.t := M.alloc α5 in - let* α7 : core.fmt.rt.Argument.t := - M.call (core.fmt.rt.Argument.t::["new_display"] (borrow α6)) in - let* α8 : M.Val (array core.fmt.rt.Argument.t) := M.alloc [ α7 ] in - let* α9 : M.Val (ref (array core.fmt.rt.Argument.t)) := - M.alloc (borrow α8) in - let* α10 : ref (slice core.fmt.rt.Argument.t) := - M.read (pointer_coercion "Unsize" α9) in - let* α11 : core.fmt.Arguments.t := - M.call (core.fmt.Arguments.t::["new_v1"] α4 α10) in - let* α12 : unit := M.call (std.io.stdio._print α11) in - M.alloc α12 in - M.alloc tt in - let* _ : M.Val unit := - let* _ : M.Val unit := - let* α0 : ref str.t := M.read (mk_str "size of `i` in bytes: ") in - let* α1 : ref str.t := M.read (mk_str " -") in - let* α2 : M.Val (array (ref str.t)) := M.alloc [ α0; α1 ] in - let* α3 : M.Val (ref (array (ref str.t))) := M.alloc (borrow α2) in - let* α4 : ref (slice (ref str.t)) := - M.read (pointer_coercion "Unsize" α3) in - let* α5 : usize.t := M.call (core.mem.size_of_val (borrow i)) in - let* α6 : M.Val usize.t := M.alloc α5 in - let* α7 : core.fmt.rt.Argument.t := - M.call (core.fmt.rt.Argument.t::["new_display"] (borrow α6)) in - let* α8 : M.Val (array core.fmt.rt.Argument.t) := M.alloc [ α7 ] in - let* α9 : M.Val (ref (array core.fmt.rt.Argument.t)) := - M.alloc (borrow α8) in - let* α10 : ref (slice core.fmt.rt.Argument.t) := - M.read (pointer_coercion "Unsize" α9) in - let* α11 : core.fmt.Arguments.t := - M.call (core.fmt.Arguments.t::["new_v1"] α4 α10) in - let* α12 : unit := M.call (std.io.stdio._print α11) in - M.alloc α12 in - M.alloc tt in - let* _ : M.Val unit := - let* _ : M.Val unit := - let* α0 : ref str.t := M.read (mk_str "size of `f` in bytes: ") in - let* α1 : ref str.t := M.read (mk_str " -") in - let* α2 : M.Val (array (ref str.t)) := M.alloc [ α0; α1 ] in - let* α3 : M.Val (ref (array (ref str.t))) := M.alloc (borrow α2) in - let* α4 : ref (slice (ref str.t)) := - M.read (pointer_coercion "Unsize" α3) in - let* α5 : usize.t := M.call (core.mem.size_of_val (borrow f)) in - let* α6 : M.Val usize.t := M.alloc α5 in - let* α7 : core.fmt.rt.Argument.t := - M.call (core.fmt.rt.Argument.t::["new_display"] (borrow α6)) in - let* α8 : M.Val (array core.fmt.rt.Argument.t) := M.alloc [ α7 ] in - let* α9 : M.Val (ref (array core.fmt.rt.Argument.t)) := - M.alloc (borrow α8) in - let* α10 : ref (slice core.fmt.rt.Argument.t) := - M.read (pointer_coercion "Unsize" α9) in - let* α11 : core.fmt.Arguments.t := - M.call (core.fmt.Arguments.t::["new_v1"] α4 α10) in - let* α12 : unit := M.call (std.io.stdio._print α11) in - M.alloc α12 in - M.alloc tt in let* α0 : M.Val unit := M.alloc tt in M.read α0. diff --git a/lib/src/path.rs b/lib/src/path.rs index 50fb0e31b..9fc5d4e8c 100644 --- a/lib/src/path.rs +++ b/lib/src/path.rs @@ -170,6 +170,12 @@ pub(crate) fn to_valid_coq_name(str: &str) -> String { return format!("{}_", str); } + let reserved_struct_names = ["end"]; + + if reserved_struct_names.contains(&str) { + return format!("_{}", str); + } + let str = str::replace(str, "$", "_"); let str = str::replace(&str, "{{root}}", "CoqOfRust"); str::replace(&str, "::", ".") From 4e73f0d45d02a2e00bc9f38282092c9f4fed95a2 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Fri, 29 Dec 2023 18:33:21 +0800 Subject: [PATCH 3/6] Undo changes on `literals.v` --- .../default/examples/types/literals.v | 112 ++++++++++++++++-- 1 file changed, 104 insertions(+), 8 deletions(-) diff --git a/CoqOfRust/examples/default/examples/types/literals.v b/CoqOfRust/examples/default/examples/types/literals.v index 417508c7a..c679b964e 100644 --- a/CoqOfRust/examples/default/examples/types/literals.v +++ b/CoqOfRust/examples/default/examples/types/literals.v @@ -5,24 +5,28 @@ Require Import CoqOfRust.CoqOfRust. fn main() { // Suffixed literals, their types are known at initialization let x = 1u8; - // let y = 2u32; - // let z = 3f32; + let y = 2u32; + let z = 3f32; // Unsuffixed literals, their types depend on how they are used - // let i = 1; - // let f = 1.0; + let i = 1; + let f = 1.0; // `size_of_val` returns the size of a variable in bytes println!("size of `x` in bytes: {}", std::mem::size_of_val(&x)); - // println!("size of `y` in bytes: {}", std::mem::size_of_val(&y)); - // println!("size of `z` in bytes: {}", std::mem::size_of_val(&z)); - // println!("size of `i` in bytes: {}", std::mem::size_of_val(&i)); - // println!("size of `f` in bytes: {}", std::mem::size_of_val(&f)); + println!("size of `y` in bytes: {}", std::mem::size_of_val(&y)); + println!("size of `z` in bytes: {}", std::mem::size_of_val(&z)); + println!("size of `i` in bytes: {}", std::mem::size_of_val(&i)); + println!("size of `f` in bytes: {}", std::mem::size_of_val(&f)); } *) (* #[allow(dead_code)] - function was ignored by the compiler *) Definition main : M unit := let* x : M.Val u8.t := M.alloc (Integer.of_Z 1) in + let* y : M.Val u32.t := M.alloc (Integer.of_Z 2) in + let* z : M.Val f32.t := M.copy UnsupportedLiteral in + let* i : M.Val i32.t := M.alloc (Integer.of_Z 1) in + let* f : M.Val f64.t := M.copy UnsupportedLiteral in let* _ : M.Val unit := let* _ : M.Val unit := let* α0 : ref str.t := M.read (mk_str "size of `x` in bytes: ") in @@ -46,5 +50,97 @@ Definition main : M unit := let* α12 : unit := M.call (std.io.stdio._print α11) in M.alloc α12 in M.alloc tt in + let* _ : M.Val unit := + let* _ : M.Val unit := + let* α0 : ref str.t := M.read (mk_str "size of `y` in bytes: ") in + let* α1 : ref str.t := M.read (mk_str " +") in + let* α2 : M.Val (array (ref str.t)) := M.alloc [ α0; α1 ] in + let* α3 : M.Val (ref (array (ref str.t))) := M.alloc (borrow α2) in + let* α4 : ref (slice (ref str.t)) := + M.read (pointer_coercion "Unsize" α3) in + let* α5 : usize.t := M.call (core.mem.size_of_val (borrow y)) in + let* α6 : M.Val usize.t := M.alloc α5 in + let* α7 : core.fmt.rt.Argument.t := + M.call (core.fmt.rt.Argument.t::["new_display"] (borrow α6)) in + let* α8 : M.Val (array core.fmt.rt.Argument.t) := M.alloc [ α7 ] in + let* α9 : M.Val (ref (array core.fmt.rt.Argument.t)) := + M.alloc (borrow α8) in + let* α10 : ref (slice core.fmt.rt.Argument.t) := + M.read (pointer_coercion "Unsize" α9) in + let* α11 : core.fmt.Arguments.t := + M.call (core.fmt.Arguments.t::["new_v1"] α4 α10) in + let* α12 : unit := M.call (std.io.stdio._print α11) in + M.alloc α12 in + M.alloc tt in + let* _ : M.Val unit := + let* _ : M.Val unit := + let* α0 : ref str.t := M.read (mk_str "size of `z` in bytes: ") in + let* α1 : ref str.t := M.read (mk_str " +") in + let* α2 : M.Val (array (ref str.t)) := M.alloc [ α0; α1 ] in + let* α3 : M.Val (ref (array (ref str.t))) := M.alloc (borrow α2) in + let* α4 : ref (slice (ref str.t)) := + M.read (pointer_coercion "Unsize" α3) in + let* α5 : usize.t := M.call (core.mem.size_of_val (borrow z)) in + let* α6 : M.Val usize.t := M.alloc α5 in + let* α7 : core.fmt.rt.Argument.t := + M.call (core.fmt.rt.Argument.t::["new_display"] (borrow α6)) in + let* α8 : M.Val (array core.fmt.rt.Argument.t) := M.alloc [ α7 ] in + let* α9 : M.Val (ref (array core.fmt.rt.Argument.t)) := + M.alloc (borrow α8) in + let* α10 : ref (slice core.fmt.rt.Argument.t) := + M.read (pointer_coercion "Unsize" α9) in + let* α11 : core.fmt.Arguments.t := + M.call (core.fmt.Arguments.t::["new_v1"] α4 α10) in + let* α12 : unit := M.call (std.io.stdio._print α11) in + M.alloc α12 in + M.alloc tt in + let* _ : M.Val unit := + let* _ : M.Val unit := + let* α0 : ref str.t := M.read (mk_str "size of `i` in bytes: ") in + let* α1 : ref str.t := M.read (mk_str " +") in + let* α2 : M.Val (array (ref str.t)) := M.alloc [ α0; α1 ] in + let* α3 : M.Val (ref (array (ref str.t))) := M.alloc (borrow α2) in + let* α4 : ref (slice (ref str.t)) := + M.read (pointer_coercion "Unsize" α3) in + let* α5 : usize.t := M.call (core.mem.size_of_val (borrow i)) in + let* α6 : M.Val usize.t := M.alloc α5 in + let* α7 : core.fmt.rt.Argument.t := + M.call (core.fmt.rt.Argument.t::["new_display"] (borrow α6)) in + let* α8 : M.Val (array core.fmt.rt.Argument.t) := M.alloc [ α7 ] in + let* α9 : M.Val (ref (array core.fmt.rt.Argument.t)) := + M.alloc (borrow α8) in + let* α10 : ref (slice core.fmt.rt.Argument.t) := + M.read (pointer_coercion "Unsize" α9) in + let* α11 : core.fmt.Arguments.t := + M.call (core.fmt.Arguments.t::["new_v1"] α4 α10) in + let* α12 : unit := M.call (std.io.stdio._print α11) in + M.alloc α12 in + M.alloc tt in + let* _ : M.Val unit := + let* _ : M.Val unit := + let* α0 : ref str.t := M.read (mk_str "size of `f` in bytes: ") in + let* α1 : ref str.t := M.read (mk_str " +") in + let* α2 : M.Val (array (ref str.t)) := M.alloc [ α0; α1 ] in + let* α3 : M.Val (ref (array (ref str.t))) := M.alloc (borrow α2) in + let* α4 : ref (slice (ref str.t)) := + M.read (pointer_coercion "Unsize" α3) in + let* α5 : usize.t := M.call (core.mem.size_of_val (borrow f)) in + let* α6 : M.Val usize.t := M.alloc α5 in + let* α7 : core.fmt.rt.Argument.t := + M.call (core.fmt.rt.Argument.t::["new_display"] (borrow α6)) in + let* α8 : M.Val (array core.fmt.rt.Argument.t) := M.alloc [ α7 ] in + let* α9 : M.Val (ref (array core.fmt.rt.Argument.t)) := + M.alloc (borrow α8) in + let* α10 : ref (slice core.fmt.rt.Argument.t) := + M.read (pointer_coercion "Unsize" α9) in + let* α11 : core.fmt.Arguments.t := + M.call (core.fmt.Arguments.t::["new_v1"] α4 α10) in + let* α12 : unit := M.call (std.io.stdio._print α11) in + M.alloc α12 in + M.alloc tt in let* α0 : M.Val unit := M.alloc tt in M.read α0. From a69f67c73cfc146616cb415937550a305ae8383e Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Fri, 29 Dec 2023 18:55:19 +0800 Subject: [PATCH 4/6] Redo the change --- .../axiomatized/examples/types/literals.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/CoqOfRust/examples/axiomatized/examples/types/literals.v b/CoqOfRust/examples/axiomatized/examples/types/literals.v index 911112477..d0f59f5a4 100644 --- a/CoqOfRust/examples/axiomatized/examples/types/literals.v +++ b/CoqOfRust/examples/axiomatized/examples/types/literals.v @@ -5,19 +5,19 @@ Require Import CoqOfRust.CoqOfRust. fn main() { // Suffixed literals, their types are known at initialization let x = 1u8; - // let y = 2u32; - // let z = 3f32; + let y = 2u32; + let z = 3f32; // Unsuffixed literals, their types depend on how they are used - // let i = 1; - // let f = 1.0; + let i = 1; + let f = 1.0; // `size_of_val` returns the size of a variable in bytes println!("size of `x` in bytes: {}", std::mem::size_of_val(&x)); - // println!("size of `y` in bytes: {}", std::mem::size_of_val(&y)); - // println!("size of `z` in bytes: {}", std::mem::size_of_val(&z)); - // println!("size of `i` in bytes: {}", std::mem::size_of_val(&i)); - // println!("size of `f` in bytes: {}", std::mem::size_of_val(&f)); + println!("size of `y` in bytes: {}", std::mem::size_of_val(&y)); + println!("size of `z` in bytes: {}", std::mem::size_of_val(&z)); + println!("size of `i` in bytes: {}", std::mem::size_of_val(&i)); + println!("size of `f` in bytes: {}", std::mem::size_of_val(&f)); } *) (* #[allow(dead_code)] - function was ignored by the compiler *) From 0ac7c4855abf14be5706c40c772a8e64e999bd6d Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Fri, 29 Dec 2023 21:30:12 +0800 Subject: [PATCH 5/6] Changed `_end` to `end_` in the translations --- CoqOfRust/_std/ops.v | 6 +++--- CoqOfRust/core/ops.v | 2 +- .../examples/default/examples/cargo/concurrent_tests.v | 8 ++++---- .../for_and_range_inclusive_to_exclusive.v | 2 +- .../diverging_functions_example_sum_odd_numbers.v | 2 +- .../default/examples/primitives/arrays_and_slices.v | 4 ++-- .../default/examples/scoping_rules/scoping_rules_raii.v | 2 +- .../examples/default/examples/std_library_types/arc.v | 2 +- .../examples/default/examples/std_library_types/vectors.v | 2 +- CoqOfRust/examples/default/examples/std_misc/channels.v | 4 ++-- CoqOfRust/examples/default/examples/std_misc/threads.v | 2 +- CoqOfRust/examples/default/examples/traits/iterators.v | 4 ++-- 12 files changed, 20 insertions(+), 20 deletions(-) diff --git a/CoqOfRust/_std/ops.v b/CoqOfRust/_std/ops.v index 84828773d..c52b97aa6 100644 --- a/CoqOfRust/_std/ops.v +++ b/CoqOfRust/_std/ops.v @@ -82,7 +82,7 @@ pub struct Range { Module Range. Record t (Idx : Set) : Set := { start : Idx; - _end : Idx; + end_ : Idx; }. End Range. Definition Range := Range.t. @@ -118,7 +118,7 @@ pub struct RangeTo { *) Module RangeTo. Record t (Idx : Set) : Set := { - _end : Idx; + end_ : Idx; }. End RangeTo. Definition RangeTo := RangeTo.t. @@ -130,7 +130,7 @@ pub struct RangeToInclusive { *) Module RangeToInclusive. Record t (Idx : Set) : Set := { - _end : Idx; + end_ : Idx; }. End RangeToInclusive. Definition RangeToInclusive := RangeToInclusive.t. diff --git a/CoqOfRust/core/ops.v b/CoqOfRust/core/ops.v index f4ee70c35..40d42fb71 100644 --- a/CoqOfRust/core/ops.v +++ b/CoqOfRust/core/ops.v @@ -18,7 +18,7 @@ Module range. Module Range. Record t (Idx : Set) : Set := { start: Idx; - _end: Idx; + end_: Idx; }. End Range. Definition Range := Range.t. diff --git a/CoqOfRust/examples/default/examples/cargo/concurrent_tests.v b/CoqOfRust/examples/default/examples/cargo/concurrent_tests.v index 09a1f8111..b4494e80a 100644 --- a/CoqOfRust/examples/default/examples/cargo/concurrent_tests.v +++ b/CoqOfRust/examples/default/examples/cargo/concurrent_tests.v @@ -86,7 +86,7 @@ Module tests. (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := Integer.of_Z 5; + core.ops.range.Range.end_ := Integer.of_Z 5; |}) in let* α1 : M.Val unit := match α0 with @@ -175,7 +175,7 @@ Module tests. (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := Integer.of_Z 5; + core.ops.range.Range.end_ := Integer.of_Z 5; |}) in let* α1 : M.Val unit := match α0 with @@ -265,7 +265,7 @@ Definition test_file : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := Integer.of_Z 5; + core.ops.range.Range.end_ := Integer.of_Z 5; |}) in let* α1 : M.Val unit := match α0 with @@ -352,7 +352,7 @@ Definition test_file_also : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := Integer.of_Z 5; + core.ops.range.Range.end_ := Integer.of_Z 5; |}) in let* α1 : M.Val unit := match α0 with diff --git a/CoqOfRust/examples/default/examples/flow_of_control/for_and_range_inclusive_to_exclusive.v b/CoqOfRust/examples/default/examples/flow_of_control/for_and_range_inclusive_to_exclusive.v index 1ec5ec3de..fba288468 100644 --- a/CoqOfRust/examples/default/examples/flow_of_control/for_and_range_inclusive_to_exclusive.v +++ b/CoqOfRust/examples/default/examples/flow_of_control/for_and_range_inclusive_to_exclusive.v @@ -26,7 +26,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 1; - core.ops.range.Range._end := Integer.of_Z 101; + core.ops.range.Range.end_ := Integer.of_Z 101; |}) in let* α1 : M.Val unit := match α0 with diff --git a/CoqOfRust/examples/default/examples/functions/diverging_functions_example_sum_odd_numbers.v b/CoqOfRust/examples/default/examples/functions/diverging_functions_example_sum_odd_numbers.v index d2cd24695..d3a2f3cac 100644 --- a/CoqOfRust/examples/default/examples/functions/diverging_functions_example_sum_odd_numbers.v +++ b/CoqOfRust/examples/default/examples/functions/diverging_functions_example_sum_odd_numbers.v @@ -87,7 +87,7 @@ Definition sum_odd_numbers (up_to : u32.t) : M u32.t := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := α0; + core.ops.range.Range.end_ := α0; |}) in let* α2 : M.Val unit := match α1 with diff --git a/CoqOfRust/examples/default/examples/primitives/arrays_and_slices.v b/CoqOfRust/examples/default/examples/primitives/arrays_and_slices.v index b7bc23b04..c5d60ff47 100644 --- a/CoqOfRust/examples/default/examples/primitives/arrays_and_slices.v +++ b/CoqOfRust/examples/default/examples/primitives/arrays_and_slices.v @@ -257,7 +257,7 @@ Definition main : M unit := (borrow ys) {| core.ops.range.Range.start := Integer.of_Z 1; - core.ops.range.Range._end := Integer.of_Z 4; + core.ops.range.Range.end_ := Integer.of_Z 4; |}) in let* α1 : unit := M.call (arrays_and_slices.analyze_slice α0) in M.alloc α1 in @@ -354,7 +354,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := α3; + core.ops.range.Range.end_ := α3; |}) in let* α5 : M.Val unit := match α4 with diff --git a/CoqOfRust/examples/default/examples/scoping_rules/scoping_rules_raii.v b/CoqOfRust/examples/default/examples/scoping_rules/scoping_rules_raii.v index 5550026fa..9cfcc07f8 100644 --- a/CoqOfRust/examples/default/examples/scoping_rules/scoping_rules_raii.v +++ b/CoqOfRust/examples/default/examples/scoping_rules/scoping_rules_raii.v @@ -64,7 +64,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := Integer.of_Z 1000; + core.ops.range.Range.end_ := Integer.of_Z 1000; |}) in let* α1 : M.Val unit := match α0 with diff --git a/CoqOfRust/examples/default/examples/std_library_types/arc.v b/CoqOfRust/examples/default/examples/std_library_types/arc.v index fb5ae22c0..b85f89017 100644 --- a/CoqOfRust/examples/default/examples/std_library_types/arc.v +++ b/CoqOfRust/examples/default/examples/std_library_types/arc.v @@ -37,7 +37,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := Integer.of_Z 10; + core.ops.range.Range.end_ := Integer.of_Z 10; |}) in let* α1 : M.Val unit := match α0 with diff --git a/CoqOfRust/examples/default/examples/std_library_types/vectors.v b/CoqOfRust/examples/default/examples/std_library_types/vectors.v index 9b7619a14..f6db4718f 100644 --- a/CoqOfRust/examples/default/examples/std_library_types/vectors.v +++ b/CoqOfRust/examples/default/examples/std_library_types/vectors.v @@ -64,7 +64,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := Integer.of_Z 10; + core.ops.range.Range.end_ := Integer.of_Z 10; |}) in M.alloc α0 in let* _ : M.Val unit := diff --git a/CoqOfRust/examples/default/examples/std_misc/channels.v b/CoqOfRust/examples/default/examples/std_misc/channels.v index b195c815a..99eb7f971 100644 --- a/CoqOfRust/examples/default/examples/std_misc/channels.v +++ b/CoqOfRust/examples/default/examples/std_misc/channels.v @@ -73,7 +73,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := α1; + core.ops.range.Range.end_ := α1; |}) in let* α3 : M.Val unit := match α2 with @@ -198,7 +198,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := α1; + core.ops.range.Range.end_ := α1; |}) in let* α3 : M.Val unit := match α2 with diff --git a/CoqOfRust/examples/default/examples/std_misc/threads.v b/CoqOfRust/examples/default/examples/std_misc/threads.v index 73df53e68..d664620e3 100644 --- a/CoqOfRust/examples/default/examples/std_misc/threads.v +++ b/CoqOfRust/examples/default/examples/std_misc/threads.v @@ -42,7 +42,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := α0; + core.ops.range.Range.end_ := α0; |}) in let* α2 : M.Val unit := match α1 with diff --git a/CoqOfRust/examples/default/examples/traits/iterators.v b/CoqOfRust/examples/default/examples/traits/iterators.v index 5935dc01c..fa0a474e9 100644 --- a/CoqOfRust/examples/default/examples/traits/iterators.v +++ b/CoqOfRust/examples/default/examples/traits/iterators.v @@ -214,7 +214,7 @@ Definition main : M unit := M.alloc {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := Integer.of_Z 3; + core.ops.range.Range.end_ := Integer.of_Z 3; |} in let* _ : M.Val unit := let* _ : M.Val unit := @@ -364,7 +364,7 @@ Definition main : M unit := (Trait := ltac:(refine _))) {| core.ops.range.Range.start := Integer.of_Z 0; - core.ops.range.Range._end := Integer.of_Z 3; + core.ops.range.Range.end_ := Integer.of_Z 3; |}) in let* α1 : M.Val unit := match α0 with From 8b03911b88f4397c63ed159dfbbb59b6eafa5502 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Fri, 29 Dec 2023 21:30:34 +0800 Subject: [PATCH 6/6] Added the changed rust file --- lib/src/path.rs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/lib/src/path.rs b/lib/src/path.rs index 9fc5d4e8c..06e385b5a 100644 --- a/lib/src/path.rs +++ b/lib/src/path.rs @@ -164,18 +164,12 @@ pub(crate) enum StructOrVariant { } pub(crate) fn to_valid_coq_name(str: &str) -> String { - let reserved_names = ["Set", "Type", "Unset", "by", "exists"]; + let reserved_names = ["Set", "Type", "Unset", "by", "exists", "end"]; if reserved_names.contains(&str) { return format!("{}_", str); } - let reserved_struct_names = ["end"]; - - if reserved_struct_names.contains(&str) { - return format!("_{}", str); - } - let str = str::replace(str, "$", "_"); let str = str::replace(&str, "{{root}}", "CoqOfRust"); str::replace(&str, "::", ".")