changeset 844:74a1e3bdf430

Fix datatype import bug in Elaborate; fix server-side source setting; more standard library stuff
author Adam Chlipala <adamc@hcoop.net>
date Sun, 07 Jun 2009 16:45:00 -0400 (2009-06-07)
parents 9f0ea203a1ca
children 6725d73c3c31
files lib/ur/basis.urs lib/ur/list.ur lib/ur/list.urs lib/ur/listPair.ur lib/ur/listPair.urs lib/ur/option.ur lib/ur/option.urs src/c/urweb.c src/elaborate.sml src/monoize.sml
diffstat 10 files changed, 85 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/lib/ur/basis.urs	Sun Jun 07 14:15:22 2009 -0400
+++ b/lib/ur/basis.urs	Sun Jun 07 16:45:00 2009 -0400
@@ -25,6 +25,7 @@
 val eq_char : eq char
 val eq_bool : eq bool
 val eq_time : eq time
+val eq_option : t ::: Type -> eq t -> eq (option t)
 val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
 
 class num
--- a/lib/ur/list.ur	Sun Jun 07 14:15:22 2009 -0400
+++ b/lib/ur/list.ur	Sun Jun 07 16:45:00 2009 -0400
@@ -171,3 +171,15 @@
     in
         all'
     end
+
+fun app [m] (_ : monad m) [a] f =
+    let
+        fun app' ls =
+            case ls of
+                [] => return ()
+              | x :: ls =>
+                f x;
+                app' ls
+    in
+        app'
+    end
--- a/lib/ur/list.urs	Sun Jun 07 14:15:22 2009 -0400
+++ b/lib/ur/list.urs	Sun Jun 07 16:45:00 2009 -0400
@@ -35,3 +35,6 @@
 val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b
 
 val all : a ::: Type -> (a -> bool) -> t a -> bool
+
+val app : m ::: (Type -> Type) -> monad m -> a ::: Type
+          -> (a -> m unit) -> t a -> m unit
--- a/lib/ur/listPair.ur	Sun Jun 07 14:15:22 2009 -0400
+++ b/lib/ur/listPair.ur	Sun Jun 07 16:45:00 2009 -0400
@@ -8,3 +8,14 @@
     in
         mapX'
     end
+
+fun all [a] [b] f =
+    let
+        fun all' ls1 ls2 =
+            case (ls1, ls2) of
+                ([], []) => True
+              | (x1 :: ls1, x2 :: ls2) => f x1 x2 && all' ls1 ls2
+              | _ => False
+    in
+        all'
+    end
--- a/lib/ur/listPair.urs	Sun Jun 07 14:15:22 2009 -0400
+++ b/lib/ur/listPair.urs	Sun Jun 07 16:45:00 2009 -0400
@@ -1,2 +1,4 @@
 val mapX : a ::: Type -> b ::: Type -> ctx ::: {Unit}
            -> (a -> b -> xml ctx [] []) -> list a -> list b -> xml ctx [] []
+
+val all : a ::: Type -> b ::: Type -> (a -> b -> bool) -> list a -> list b -> bool
--- a/lib/ur/option.ur	Sun Jun 07 14:15:22 2009 -0400
+++ b/lib/ur/option.ur	Sun Jun 07 16:45:00 2009 -0400
@@ -4,3 +4,8 @@
     case x of
         None => False
       | Some _ => True
+
+fun mp [a] [b] f x =
+    case x of
+        None => None
+      | Some y => Some (f y)
--- a/lib/ur/option.urs	Sun Jun 07 14:15:22 2009 -0400
+++ b/lib/ur/option.urs	Sun Jun 07 16:45:00 2009 -0400
@@ -1,3 +1,5 @@
 datatype t = datatype Basis.option
 
 val isSome : a ::: Type -> t a -> bool
+
+val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
--- a/src/c/urweb.c	Sun Jun 07 14:15:22 2009 -0400
+++ b/src/c/urweb.c	Sun Jun 07 16:45:00 2009 -0400
@@ -1278,12 +1278,12 @@
   size_t s_len = strlen(s);
 
   uw_check_script(ctx, 6 + INTS_MAX + s_len);
-  sprintf(ctx->script.front, "s%d.v=%n", (int)n, &len);
+  sprintf(ctx->script.front, "sv(s%d,%n", (int)n, &len);
   ctx->script.front += len;
   strcpy(ctx->script.front, s);
   ctx->script.front += s_len;
-  strcpy(ctx->script.front, ";");
-  ctx->script.front++;
+  strcpy(ctx->script.front, ");");
+  ctx->script.front += 2;
 
   return uw_unit_v;
 }
--- a/src/elaborate.sml	Sun Jun 07 14:15:22 2009 -0400
+++ b/src/elaborate.sml	Sun Jun 07 16:45:00 2009 -0400
@@ -3271,6 +3271,10 @@
                                       val env = E.pushDatatype env n' xs xncs
 
                                       val t = (L'.CNamed n', loc)
+                                      val nxs = length xs
+                                      val t = ListUtil.foldli (fn (i, _, t) =>
+                                                                  (L'.CApp (t, (L'.CRel (nxs - 1 - i), loc)), loc))
+                                                              t xs
                                       val env = foldl (fn ((x, n, to), env) =>
                                                           let
                                                               val t = case to of
--- a/src/monoize.sml	Sun Jun 07 14:15:22 2009 -0400
+++ b/src/monoize.sml	Sun Jun 07 16:45:00 2009 -0400
@@ -778,6 +778,48 @@
                                  (L'.TFfi ("Basis", "bool"), loc),
                                  (L'.EBinop ("==", (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc),
              fm)
+          | L.ECApp ((L.EFfi ("Basis", "eq_option"), _), t) =>
+            let
+                val t = monoType env t
+                val t' = (L'.TOption t, loc)
+                val bool = (L'.TFfi ("Basis", "bool"), loc)
+            in
+                ((L'.EAbs ("f", (L'.TFun (t, (L'.TFun (t, bool), loc)), loc),
+                           (L'.TFun (t', (L'.TFun (t', bool), loc)), loc),
+                           (L'.EAbs ("x", t', (L'.TFun (t', bool), loc),
+                                     (L'.EAbs ("y", t', bool,
+                                               (L'.ECase ((L'.ERecord [("1", (L'.ERel 1, loc), t'),
+                                                                       ("2", (L'.ERel 0, loc), t')], loc),
+                                                          [((L'.PRecord [("1", (L'.PNone t, loc), t'),
+                                                                         ("2", (L'.PNone t, loc), t')], loc),
+                                                            (L'.ECon (L'.Enum, L'.PConFfi {mod = "Basis",
+                                                                                           datatyp = "bool",
+                                                                                           con = "True",
+                                                                                           arg = NONE},
+                                                                      NONE), loc)),
+                                                           ((L'.PRecord [("1", (L'.PSome (t,
+                                                                                          (L'.PVar ("x1",
+                                                                                                    t), loc)),
+                                                                                loc), t'),
+                                                                         ("2", (L'.PSome (t,
+                                                                                          (L'.PVar ("x2",
+                                                                                                    t), loc)),
+                                                                                loc), t')], loc),
+                                                            (L'.EApp ((L'.EApp ((L'.ERel 4, loc),
+                                                                                (L'.ERel 1, loc)), loc),
+                                                                      (L'.ERel 0, loc)), loc)),
+                                                           ((L'.PWild, loc),
+                                                            (L'.ECon (L'.Enum, L'.PConFfi {mod = "Basis",
+                                                                                           datatyp = "bool",
+                                                                                           con = "False",
+                                                                                           arg = NONE},
+                                                                      NONE), loc))],
+                                                          {disc = (L'.TRecord [("1", t'), ("2", t')], loc),
+                                                           result = (L'.TFfi ("Basis", "bool"), loc)}),
+                                                loc)), loc)), loc)), loc),
+                 fm)
+            end
+
           | L.ECApp ((L.EFfi ("Basis", "mkEq"), _), t) =>
             let
                 val t = monoType env t