summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-01-11 14:03:54 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2011-01-11 14:03:54 -0500
commit138f64b8f02f05e6073f61b1db2c3d5e805b75c0 (patch)
tree07c262b05b9acf20fbb9aaaef74b8a2b300ad330
parentd6cee9f01237ec6c6ebb2843a33eda0da89fd5bb (diff)
String processing optimizations
-rw-r--r--include/urweb.h1
-rw-r--r--lib/ur/basis.urs1
-rw-r--r--lib/ur/string.ur1
-rw-r--r--lib/ur/string.urs1
-rw-r--r--src/c/urweb.c41
5 files changed, 37 insertions, 8 deletions
diff --git a/include/urweb.h b/include/urweb.h
index 75f8e782..49281ac1 100644
--- a/include/urweb.h
+++ b/include/urweb.h
@@ -134,6 +134,7 @@ uw_Basis_bool uw_Basis_unurlifyBool(uw_context, char **);
uw_Basis_time uw_Basis_unurlifyTime(uw_context, char **);
uw_Basis_int uw_Basis_strlen(uw_context, const char *);
+uw_Basis_bool uw_Basis_strlenGe(uw_context, uw_Basis_string, uw_Basis_int);
uw_Basis_char uw_Basis_strsub(uw_context, const char *, uw_Basis_int);
uw_Basis_string uw_Basis_strsuffix(uw_context, const char *, uw_Basis_int);
uw_Basis_string uw_Basis_strcat(uw_context, const char *, const char *);
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 0938096b..727f2e39 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -81,6 +81,7 @@ val chr : int -> char
(** String operations *)
val strlen : string -> int
+val strlenGe : string -> int -> bool
val strcat : string -> string -> string
val strsub : string -> int -> char
val strsuffix : string -> int -> string
diff --git a/lib/ur/string.ur b/lib/ur/string.ur
index 6a269373..235e5939 100644
--- a/lib/ur/string.ur
+++ b/lib/ur/string.ur
@@ -3,6 +3,7 @@ type t = Basis.string
val str = Basis.str1
val length = Basis.strlen
+val lengthGe = Basis.strlenGe
val append = Basis.strcat
val sub = Basis.strsub
diff --git a/lib/ur/string.urs b/lib/ur/string.urs
index 552da557..52aa27b6 100644
--- a/lib/ur/string.urs
+++ b/lib/ur/string.urs
@@ -3,6 +3,7 @@ type t = string
val str : char -> t
val length : t -> int
+val lengthGe : t -> int -> bool
val append : t -> t -> t
diff --git a/src/c/urweb.c b/src/c/urweb.c
index 17e4bed2..0b4054e9 100644
--- a/src/c/urweb.c
+++ b/src/c/urweb.c
@@ -2133,23 +2133,48 @@ uw_unit uw_Basis_htmlifyTime_w(uw_context ctx, uw_Basis_time t) {
}
uw_Basis_char uw_Basis_strsub(uw_context ctx, uw_Basis_string s, uw_Basis_int n) {
- if (n >= 0 && n < strlen(s))
- return s[n];
- else
- uw_error(ctx, FATAL, "Out-of-bounds strsub");
+ while (n >= 0) {
+ if (*s == 0)
+ uw_error(ctx, FATAL, "Out-of-bounds strsub");
+
+ if (n == 0)
+ return *s;
+
+ --n;
+ ++s;
+ }
+
+ uw_error(ctx, FATAL, "Negative strsub bound");
}
uw_Basis_string uw_Basis_strsuffix(uw_context ctx, uw_Basis_string s, uw_Basis_int n) {
- if (n >= 0 && n < strlen(s))
- return &s[n];
- else
- uw_error(ctx, FATAL, "Out-of-bounds strsuffix");
+ while (n >= 0) {
+ if (*s == 0 || n == 0)
+ return s;
+
+ --n;
+ ++s;
+ }
+
+ uw_error(ctx, FATAL, "Negative strsuffix bound");
}
uw_Basis_int uw_Basis_strlen(uw_context ctx, uw_Basis_string s) {
return strlen(s);
}
+uw_Basis_bool uw_Basis_strlenGe(uw_context ctx, uw_Basis_string s, uw_Basis_int n) {
+ while (n > 0) {
+ if (*s == 0)
+ return uw_Basis_False;
+
+ --n;
+ ++s;
+ }
+
+ return uw_Basis_True;
+}
+
uw_Basis_string uw_Basis_strchr(uw_context ctx, uw_Basis_string s, uw_Basis_char ch) {
return strchr(s, ch);
}