From d8801e05ef2f81f21eb27555b626ee2e52c3365f Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 26 May 2009 12:25:06 -0400
Subject: Chars and more string operations

---
 lib/js/urweb.js   |  3 +++
 lib/ur/basis.urs  |  7 +++++++
 lib/ur/list.ur    | 34 ++++++++++++++++++++++++++++++++++
 lib/ur/list.urs   |  8 ++++++++
 lib/ur/string.ur  |  4 ++++
 lib/ur/string.urs |  4 ++++
 6 files changed, 60 insertions(+)
 create mode 100644 lib/ur/string.ur
 create mode 100644 lib/ur/string.urs

(limited to 'lib')

diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index c031678a..2b4d2643 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -351,6 +351,9 @@ function eh(x) {
 function ts(x) { return x.toString() }
 function bs(b) { return (b ? "True" : "False") }
 
+function sub(x, i) { return x[i]; }
+function suf(x, i) { return x.substring(i); }
+
 function pi(s) {
   var r = parseInt(s);
   if (r.toString() == s)
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
-- 
cgit v1.2.3