Merge pull request #436 from formal-land/gy@ChangeLiteralsError

Fixes on `concurrent_tests.v`
formal-land · Dec 29, 2023 · 89c6124 · 89c6124
2 parents 65f9e09 + 8b03911
commit 89c6124
Show file tree

Hide file tree

Showing 14 changed files with 48 additions and 26 deletions.
diff --git 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.

diff --git a/CoqOfRust/_std/ops.v b/CoqOfRust/_std/ops.v
@@ -82,7 +82,7 @@ pub struct Range<Idx> {
 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<Idx> {
 *)
 Module RangeTo.
   Record t (Idx : Set) : Set := { 
-    _end : Idx;
+    end_ : Idx;
   }.
 End RangeTo.
 Definition RangeTo := RangeTo.t.
@@ -130,7 +130,7 @@ pub struct RangeToInclusive<Idx> {
 *)
 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
@@ -4,6 +4,26 @@ Require CoqOfRust.alloc.vec.
 Require CoqOfRust.core.convert.
 Require CoqOfRust.core.result.
 
+(* 
+pub struct Range<Idx> {
+    /// 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/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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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/lib/src/path.rs b/lib/src/path.rs
@@ -164,7 +164,7 @@ 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);