diff --git a/prelude/DATS/strn000.dats b/prelude/DATS/strn000.dats index 5f04849fa..790e6b2b5 100644 --- a/prelude/DATS/strn000.dats +++ b/prelude/DATS/strn000.dats @@ -153,12 +153,25 @@ end//let//end($UN.gasz_lget$at$raw) // #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 index 923a818b5..a411cc6a8 100644 --- 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 index 4d0271b07..aecac11d1 100644 --- 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 index 9d1675b04..15c69db62 100644 --- 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}