Support pts_to_range array accesses.

FStarLang · Sep 25, 2024 · f905b1b · f905b1b
1 parent ea84ad3
commit f905b1b
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 13 deletions.
diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst
@@ -544,15 +544,17 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
     mk_call (mk_expr_path (["std"; "boxed"; "Box"; "new"])) [e]
 
 
-  | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, [e; i; _; _])
+  | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e::i::_)
     when S.string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Access" ||
+         S.string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_index" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.op_Array_Access" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.read_ref" ->
 
     mk_expr_index (extract_mlexpr g e) (extract_mlexpr g i)
 
   | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e1::e2::e3::_)
     when S.string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Assignment" ||
+         S.string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_upd" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.op_Array_Assignment" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.write_ref" ->
 

diff --git a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml
@@ -953,19 +953,22 @@ and (extract_mlexpr :
                 uu___2::[]);
              FStar_Extraction_ML_Syntax.mlty = uu___3;
              FStar_Extraction_ML_Syntax.loc = uu___4;_},
-           e1::i::uu___5::uu___6::[])
+           e1::i::uu___5)
           when
-          ((let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-            uu___7 = "Pulse.Lib.Array.Core.op_Array_Access") ||
-             (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-              uu___7 = "Pulse.Lib.Vec.op_Array_Access"))
+          (((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+             uu___6 = "Pulse.Lib.Array.Core.op_Array_Access") ||
+              (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+               uu___6 = "Pulse.Lib.Array.Core.pts_to_range_index"))
+             ||
+             (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+              uu___6 = "Pulse.Lib.Vec.op_Array_Access"))
             ||
-            (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-             uu___7 = "Pulse.Lib.Vec.read_ref")
+            (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+             uu___6 = "Pulse.Lib.Vec.read_ref")
           ->
-          let uu___7 = extract_mlexpr g e1 in
-          let uu___8 = extract_mlexpr g i in
-          Pulse2Rust_Rust_Syntax.mk_expr_index uu___7 uu___8
+          let uu___6 = extract_mlexpr g e1 in
+          let uu___7 = extract_mlexpr g i in
+          Pulse2Rust_Rust_Syntax.mk_expr_index uu___6 uu___7
       | FStar_Extraction_ML_Syntax.MLE_App
           ({
              FStar_Extraction_ML_Syntax.expr =
@@ -980,8 +983,11 @@ and (extract_mlexpr :
              FStar_Extraction_ML_Syntax.loc = uu___4;_},
            e1::e2::e3::uu___5)
           when
-          ((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-            uu___6 = "Pulse.Lib.Array.Core.op_Array_Assignment") ||
+          (((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+             uu___6 = "Pulse.Lib.Array.Core.op_Array_Assignment") ||
+              (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+               uu___6 = "Pulse.Lib.Array.Core.pts_to_range_upd"))
+             ||
              (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
               uu___6 = "Pulse.Lib.Vec.op_Array_Assignment"))
             ||