In-place merge sort for slices

lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti

@@ -30,7 +30,7 @@ without modifying the pointer.
 Use `Pulse.Lib.Slice.slice` instead when possible.
 *)
 
-val ptr : Type0 -> Type0
+val ptr ([@@@strictly_positive] elt: Type0) : Type0
 
 val base #t (p: ptr t) : GTot (A.array t)
 val offset #t (p: ptr t) : GTot nat

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

@@ -20,7 +20,7 @@ open Pulse.Lib.Pervasives
 module SZ = FStar.SizeT
 module A = Pulse.Lib.Array
 
-val slice : Type0 -> Type0
+val slice ([@@@strictly_positive] elt: Type0) : Type0
 
 val len (#t: Type) : slice t -> SZ.t
 

lib/pulse/lib/Pulse.Lib.Sort.Base.fst

@@ -0,0 +1,21 @@
+module Pulse.Lib.Sort.Base
+open Pulse.Lib.Pervasives
+
+module I16 = FStar.Int16
+
+inline_for_extraction
+let impl_compare_t
+  (#tl #th: Type)
+  (vmatch: tl -> th -> slprop)
+  (compare: th -> th -> int)
+= (x1: tl) ->
+  (x2: tl) ->
+  (#y1: Ghost.erased th) ->
+  (#y2: Ghost.erased th) ->
+  stt I16.t
+    (vmatch x1 y1 ** vmatch x2 y2)
+    (fun res -> vmatch x1 y1 ** vmatch x2 y2 ** pure (
+      let v = compare y1 y2 in
+      (v < 0 <==> I16.v res < 0) /\
+      (v > 0 <==> I16.v res > 0)
+    ))