From 11fd1db04f22101a5a0fa8e1d5b57126e75f6eb5 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sat, 19 Sep 2009 13:32:33 -0400
Subject: Grid sorting working

---
 lib/js/urweb.js   |  3 +++
 lib/ur/basis.urs  |  1 +
 lib/ur/option.ur  | 12 ++++++++++++
 lib/ur/option.urs |  1 +
 4 files changed, 17 insertions(+)

(limited to 'lib')

diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index b1046aa6..638bb2b9 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -506,6 +506,9 @@ function uul(getToken, getData) {
     throw ("Can't unmarshal list (" + tok + ")");
 }
 
+function strcmp(str1, str2) {
+  return ((str1 == str2) ? 0 : ((str1 > str2) ? 1 : -1));
+}
 
 
 // Remote calls
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 04404ad5..b7468d2f 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -49,6 +49,7 @@ val ord_string : ord string
 val ord_char : ord char
 val ord_bool : ord bool
 val ord_time : ord time
+val mkOrd : t ::: Type -> {Lt : t -> t -> bool, Le : t -> t -> bool} -> ord t
 
 
 (** String operations *)
diff --git a/lib/ur/option.ur b/lib/ur/option.ur
index a22cf5b5..1ba33d8e 100644
--- a/lib/ur/option.ur
+++ b/lib/ur/option.ur
@@ -7,6 +7,18 @@ fun eq [a] (_ : eq a) =
                | (Some x, Some y) => x = y
                | _ => False)
 
+fun ord [a] (_ : ord a) =
+    mkOrd {Lt = fn x y =>
+                   case (x, y) of
+                       (None, Some _) => True
+                     | (Some x, Some y) => x < y
+                     | _ => False,
+           Le = fn x y =>
+                   case (x, y) of
+                       (None, _) => True
+                     | (Some x, Some y) => x <= y
+                     | _ => False}
+
 fun isNone [a] x =
     case x of
         None => True
diff --git a/lib/ur/option.urs b/lib/ur/option.urs
index f4570768..60ca6db9 100644
--- a/lib/ur/option.urs
+++ b/lib/ur/option.urs
@@ -1,6 +1,7 @@
 datatype t = datatype Basis.option
 
 val eq : a ::: Type -> eq a -> eq (t a)
+val ord : a ::: Type -> ord a -> ord (t a)
 
 val isNone : a ::: Type -> t a -> bool
 val isSome : a ::: Type -> t a -> bool
-- 
cgit v1.2.3