Remove slice_pair in favor of standard F* pairs

lib/pulse/lib/Pulse.Lib.Slice.Util.fst

@@ -29,9 +29,9 @@ fn append_split (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t)
     (#v1: Ghost.erased (Seq.seq t) { SZ.v i == Seq.length v1 })
     (#v2: Ghost.erased (Seq.seq t))
   requires pts_to s #p (v1 `Seq.append` v2)
-  returns res: S.slice_pair t
+  returns res: (slice t & slice t)
   ensures
-    (let S.SlicePair s1 s2 = res in
+    (let (s1, s2) = res in
       pts_to s1 #p v1 **
       pts_to s2 #p v2 **
       S.is_split s s1 s2)
@@ -47,48 +47,56 @@ fn append_split_trade (#t: Type) (input: S.slice t) (#p: perm) (i: SZ.t)
     (#v1: Ghost.erased (Seq.seq t) { SZ.v i == Seq.length v1 })
     (#v2: Ghost.erased (Seq.seq t))
   requires pts_to input #p (v1 `Seq.append` v2)
-  returns res: S.slice_pair t
+  returns res: (slice t & slice t)
   ensures
-    (let SlicePair s1 s2 = res in
+    (let (s1, s2) = res in
       pts_to s1 #p v1 ** pts_to s2 #p v2 **
       trade (pts_to s1 #p v1 ** pts_to s2 #p v2)
         (pts_to input #p (v1 `Seq.append` v2)))
 {
-  let SlicePair s1 s2 = append_split input i;
-  ghost fn aux ()
-    requires S.is_split input s1 s2 ** (pts_to s1 #p v1 ** pts_to s2 #p v2)
-    ensures pts_to input #p (v1 `Seq.append` v2)
-  {
-    S.join s1 s2 input
-  };
-  intro_trade _ _ _ aux;
-  SlicePair s1 s2
+  let s = append_split input i;
+  match s {
+    Mktuple2 s1 s2 -> {
+      ghost fn aux ()
+        requires S.is_split input s1 s2 ** (pts_to s1 #p v1 ** pts_to s2 #p v2)
+        ensures pts_to input #p (v1 `Seq.append` v2)
+      {
+        S.join s1 s2 input
+      };
+      intro_trade _ _ _ aux;
+      (s1, s2)
+    }
+  }
 }
 
 inline_for_extraction
 noextract
 fn split_trade (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v })
   requires pts_to s #p v
-  returns res: S.slice_pair t
+  returns res: (slice t & slice t)
   ensures
-    (let SlicePair s1 s2 = res in
+    (let (s1, s2) = res in
       let v1 = Seq.slice v 0 (SZ.v i) in
       let v2 = Seq.slice v (SZ.v i) (Seq.length v) in
       pts_to s1 #p v1 ** pts_to s2 #p v2 **
       trade (pts_to s1 #p v1 ** pts_to s2 #p v2)
         (pts_to s #p v))
 {
   Seq.lemma_split v (SZ.v i);
-  let SlicePair s1 s2 = S.split s i;
-  with v1 v2. assert pts_to s1 #p v1 ** pts_to s2 #p v2;
-  ghost fn aux ()
-    requires S.is_split s s1 s2 ** (pts_to s1 #p v1 ** pts_to s2 #p v2)
-    ensures pts_to s #p v
-  {
-    S.join s1 s2 s
-  };
-  intro_trade _ _ _ aux;
-  S.SlicePair s1 s2
+  let s' = S.split s i;
+  match s' {
+    Mktuple2 s1 s2 -> {
+      with v1 v2. assert pts_to s1 #p v1 ** pts_to s2 #p v2;
+      ghost fn aux ()
+        requires S.is_split s s1 s2 ** (pts_to s1 #p v1 ** pts_to s2 #p v2)
+        ensures pts_to s #p v
+      {
+        S.join s1 s2 s
+      };
+      intro_trade _ _ _ aux;
+      (s1, s2)
+    }
+  }
 }
 
 inline_for_extraction

lib/pulse/lib/Pulse.Lib.Slice.fst

@@ -175,9 +175,9 @@ let is_split_is_slprop2 s s1 s2 = ()
 fn split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t)
     (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v })
   requires pts_to s #p v
-  returns res : slice_pair t
+  returns res : (slice t & slice t)
   ensures
-    (let SlicePair s1 s2 = res in
+    (let (s1, s2) = res in
     pts_to s1 #p (Seq.slice v 0 (SZ.v i)) **
     pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)) **
     is_split s s1 s2)
@@ -196,7 +196,7 @@ fn split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t)
     };
     fold_pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v));
     fold (is_split s s1 s2);
-    (s1 `SlicePair` s2)
+    (s1, s2)
 }
 
 ghost

lib/pulse/lib/Pulse.Lib.Slice.fsti

@@ -97,11 +97,9 @@ val is_split_is_slprop2 (#t: Type) (s: slice t) (left: slice t) (right: slice t)
   : Lemma (is_slprop2 (is_split s left right))
           [SMTPat (is_slprop2 (is_split s left right))]
 
-noeq type slice_pair (t: Type) = | SlicePair: (fst: slice t) -> (snd: slice t) -> slice_pair t
-
-val split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) : stt (slice_pair t)
+val split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) : stt (slice t & slice t)
     (requires pts_to s #p v)
-    (ensures fun (SlicePair s1 s2) ->
+    (ensures fun (s1, s2) ->
       pts_to s1 #p (Seq.slice v 0 (SZ.v i)) **
       pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)) **
       is_split s s1 s2)

pulse2rust/src/Pulse2Rust.Extract.fst

@@ -406,10 +406,6 @@ let rec extract_mlpattern_to_pat (g:env) (p:S.mlpattern) : env & pat =
     let g, ps = fold_left_map extract_mlpattern_to_pat g ps in
     g,
     mk_pat_tuple ps
-  | S.MLP_CTor (p, ps) when snd p = "SlicePair" ->
-    let g, ps = fold_left_map extract_mlpattern_to_pat g ps in
-    g,
-    mk_pat_tuple ps
   | S.MLP_CTor (p, ps) ->
     let g, ps = fold_left_map extract_mlpattern_to_pat g ps in
     let path =

pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml

@@ -583,14 +583,6 @@ let rec (extract_mlpattern_to_pat :
            | (g1, ps1) ->
                let uu___1 = Pulse2Rust_Rust_Syntax.mk_pat_tuple ps1 in
                (g1, uu___1))
-      | FStarC_Extraction_ML_Syntax.MLP_CTor (p1, ps) when
-          (FStar_Pervasives_Native.snd p1) = "SlicePair" ->
-          let uu___ =
-            FStarC_Compiler_List.fold_left_map extract_mlpattern_to_pat g ps in
-          (match uu___ with
-           | (g1, ps1) ->
-               let uu___1 = Pulse2Rust_Rust_Syntax.mk_pat_tuple ps1 in
-               (g1, uu___1))
       | FStarC_Extraction_ML_Syntax.MLP_CTor (p1, ps) ->
           let uu___ =
             FStarC_Compiler_List.fold_left_map extract_mlpattern_to_pat g ps in

share/pulse/examples/Example.Slice.fst

@@ -25,19 +25,27 @@ fn test (arr: A.array UInt8.t)
     ensures exists* s. pts_to arr s ** pure (s `Seq.equal` seq![0uy; 5uy; 4uy; 5uy; 4uy; 5uy]) {
   A.pts_to_len arr;
   let slice = from_array arr 6sz;
-  let SlicePair s1 s2 = split slice 2sz;
-  pts_to_len s1;
-  share s2;
-  let s2' = subslice_trade s2 1sz 4sz;
-  let x = s2'.(len s1);
-  s1.(1sz) <- x;
-  elim_trade _ _;
-  gather s2;
-  let SlicePair s3 s4 = split s2 2sz;
-  pts_to_len s3;
-  pts_to_len s4;
-  copy s3 s4;
-  join s3 s4 s2;
-  join s1 s2 slice;
-  to_array slice;
-}
+  let s' = split slice 2sz;
+  match s' {
+    Mktuple2 s1 s2 -> {
+      pts_to_len s1;
+      share s2;
+      let s2' = subslice_trade s2 1sz 4sz;
+      let x = s2'.(len s1);
+      s1.(1sz) <- x;
+      elim_trade _ _;
+      gather s2;
+      let s' = split s2 2sz;
+      match s' {
+        Mktuple2 s3 s4 -> {
+          pts_to_len s3;
+          pts_to_len s4;
+          copy s3 s4;
+          join s3 s4 s2;
+          join s1 s2 slice;
+          to_array slice;
+        }
+      }
+    }
+  }
+}