aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-26 12:25:06 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-26 12:25:06 -0400
commitd8801e05ef2f81f21eb27555b626ee2e52c3365f (patch)
tree53e0b285bbcb0e28d3cbbd507da21fcc41d8995e /lib/ur
parent5232b7e45cf55208a0a3ea41395bb9f87d06dd21 (diff)
Chars and more string operations
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/basis.urs7
-rw-r--r--lib/ur/list.ur34
-rw-r--r--lib/ur/list.urs8
-rw-r--r--lib/ur/string.ur4
-rw-r--r--lib/ur/string.urs4
5 files changed, 57 insertions, 0 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index c5251bb8..1209d265 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -1,6 +1,7 @@
type int
type float
type string
+type char
type time
type blob
@@ -21,6 +22,7 @@ val ne : t ::: Type -> eq t -> t -> t -> bool
val eq_int : eq int
val eq_float : eq float
val eq_string : eq string
+val eq_char : eq char
val eq_bool : eq bool
val eq_time : eq time
val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
@@ -44,6 +46,7 @@ val ge : t ::: Type -> ord t -> t -> t -> bool
val ord_int : ord int
val ord_float : ord float
val ord_string : ord string
+val ord_char : ord char
val ord_bool : ord bool
val ord_time : ord time
@@ -51,12 +54,15 @@ val ord_time : ord time
(** String operations *)
val strcat : string -> string -> string
+val strsub : string -> int -> char
+val strsuffix : string -> int -> string
class show
val show : t ::: Type -> show t -> t -> string
val show_int : show int
val show_float : show float
val show_string : show string
+val show_char : show char
val show_bool : show bool
val show_time : show time
val mkShow : t ::: Type -> (t -> string) -> show t
@@ -68,6 +74,7 @@ val readError : t ::: Type -> read t -> string -> t
val read_int : read int
val read_float : read float
val read_string : read string
+val read_char : read char
val read_bool : read bool
val read_time : read time
val mkRead : t ::: Type -> (string -> t) -> (string -> option t) -> read t
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 7079f6bc..7527362d 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -20,6 +20,18 @@ val rev (a ::: Type) =
rev' []
end
+val revAppend (a ::: Type) =
+ let
+ fun ra (ls : list a) acc =
+ case ls of
+ [] => acc
+ | x :: ls => ra ls (x :: acc)
+ in
+ ra
+ end
+
+fun append (a ::: Type) (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
+
fun mp (a ::: Type) (b ::: Type) f =
let
fun mp' acc ls =
@@ -30,6 +42,18 @@ fun mp (a ::: Type) (b ::: Type) f =
mp' []
end
+fun mapPartial (a ::: Type) (b ::: Type) f =
+ let
+ fun mp' acc ls =
+ case ls of
+ [] => rev acc
+ | x :: ls => mp' (case f x of
+ None => acc
+ | Some y => y :: acc) ls
+ in
+ mp' []
+ end
+
fun mapX (a ::: Type) (ctx ::: {Unit}) f =
let
fun mapX' ls =
@@ -49,3 +73,13 @@ fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f =
in
mapM' []
end
+
+fun filter (a ::: Type) f =
+ let
+ fun fil acc ls =
+ case ls of
+ [] => rev acc
+ | x :: ls => fil (if f x then x :: acc else acc) ls
+ in
+ fil []
+ end
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index d27ad997..fb3407ae 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -4,9 +4,17 @@ val show : a ::: Type -> show a -> show (list a)
val rev : a ::: Type -> t a -> t a
+val revAppend : a ::: Type -> t a -> t a -> t a
+
+val append : a ::: Type -> t a -> t a -> t a
+
val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
+val mapPartial : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b
+
val mapX : a ::: Type -> ctx ::: {Unit} -> (a -> xml ctx [] []) -> t a -> xml ctx [] []
val mapM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
-> (a -> m b) -> list a -> m (list b)
+
+val filter : a ::: Type -> (a -> bool) -> t a -> t a
diff --git a/lib/ur/string.ur b/lib/ur/string.ur
new file mode 100644
index 00000000..5362805b
--- /dev/null
+++ b/lib/ur/string.ur
@@ -0,0 +1,4 @@
+type t = Basis.string
+
+val sub = Basis.strsub
+val suffix = Basis.strsuffix
diff --git a/lib/ur/string.urs b/lib/ur/string.urs
new file mode 100644
index 00000000..524e002d
--- /dev/null
+++ b/lib/ur/string.urs
@@ -0,0 +1,4 @@
+type t = string
+
+val sub : t -> int -> char
+val suffix : t -> int -> string