Updating: very very minorly

githwxi · Aug 18, 2024 · 982e7f8 · 982e7f8
1 parent 402837c
commit 982e7f8
Show file tree

Hide file tree

Showing 4 changed files with 58 additions and 14 deletions.
diff --git a/prelude/DATS/strn000.dats b/prelude/DATS/strn000.dats
@@ -153,12 +153,25 @@ end//let//end($UN.gasz_lget$at$raw<strn><cgtz>)
 //
 #impltmp
 <(*tmp*)>
+strn_slice
+(cs, i0, j0) =
+(
+strn_make_nfun<>
+(
+j0-i0,
+lam(k0) =>
+$UN.strn_get$at$raw<>(cs,i0+k0)
+)
+)//end-of-[strn_slice(cs,i0,j0)]
+//
+(* ****** ****** *)
+//
+#impltmp
+<(*tmp*)>
 strn_prefix
   (cs, i0) =
 (
-strn_make_nfun<>(i0,
-lam(j0) =>
-$UN.strn_get$at$raw<>(cs, j0)))
+  strn_slice<>(cs, 0, i0))
 //
 #impltmp
 <(*tmp*)>
@@ -167,12 +180,12 @@ strn_suffix
 let
 val n0 =
 strn_length<>(cs) in//let
-strn_make_nfun<>(n0-i0,
-lam(j0) =>
-$UN.strn_get$at$raw<>(cs, i0+j0))
-end//let//end-of-[strn_suffix(...)]
+(
+  strn_slice<>(cs, i0, n0)) end
+//let//end-of-[strn_suffix(cs,i0)]
 //
 (* ****** ****** *)
+(* ****** ****** *)
 //
 (*
 HX-2024-08-17:

diff --git a/prelude/SATS/strn000.sats b/prelude/SATS/strn000.sats
@@ -150,20 +150,35 @@ strn_gmake1(x: (!a)): (strn)
 (* ****** ****** *)
 //
 fun<>
+strn_slice
+{n0:i0}
+{i0:nat
+;j0:int
+|i0<=j0
+;j0<=n0}
+( cs: strn(n0)
+, i0: sint(i0)
+, j0: sint(j0)): strn(j0-i0)
+#symload
+slice with strn_slice of 1000
+//
+fun<>
 strn_prefix
 {n0:i0}
-{i0:i0|i0<=n0}
+{i0:nat
+|i0<=n0}
 ( cs: strn(n0)
 , i0: sint(i0)): strn(i0)
+#symload
+prefix with strn_prefix of 1000
+//
 fun<>
 strn_suffix
 {n0:i0}
-{i0:i0|i0<=n0}
+{i0:nat
+|i0<=n0}
 ( cs: strn(n0)
 , i0: sint(i0)): strn(n0-i0)
-//
-#symload
-prefix with strn_prefix of 1000
 #symload
 suffix with strn_suffix of 1000
 //

diff --git a/prelude/basics0.sats b/prelude/basics0.sats
@@ -380,10 +380,13 @@ neq_i0_i0: (i0, i0) -> b0
 //
 (* ****** ****** *)
 //
-#sortdef pos = {a:i0 | a > 0}
-#sortdef neg = {a:i0 | a < 0}
+#sortdef n0 = {a:i0 | a >= 0}
+//
+(* ****** ****** *)
 //
+#sortdef neg = {a:i0 | a < 0}
 #sortdef nat = {a:i0 | a >= 0}
+#sortdef pos = {a:i0 | a >= 1}
 //
 (* ****** ****** *)
 //

diff --git a/srcgen1/prelude/SATS/xunimpl.sats b/srcgen1/prelude/SATS/xunimpl.sats
@@ -429,6 +429,19 @@ strn_gmake( a ): strn
 (* ****** ****** *)
 //
 fun<>
+strn_slice
+{n0:i0}
+{i0:nat
+;j0:int
+|i0<=j0
+;j0<=n0}
+( cs: strn(n0)
+, i0: sint(i0)
+, j0: sint(j0)): strn(j0-i0)
+#symload
+slice with strn_slice of 1000
+//
+fun<>
 strn_prefix
 {n0:i0}
 {i0:i0|i0<=n0}