# HG changeset patch # User Adam Chlipala # Date 1244407500 14400 # Node ID 74a1e3bdf4300c75e0f59b241ec5123edc63dde9 # Parent 9f0ea203a1ca0498ff5a24d48b1217893fb4fc1d Fix datatype import bug in Elaborate; fix server-side source setting; more standard library stuff diff -r 9f0ea203a1ca -r 74a1e3bdf430 lib/ur/basis.urs --- 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 diff -r 9f0ea203a1ca -r 74a1e3bdf430 lib/ur/list.ur --- 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 diff -r 9f0ea203a1ca -r 74a1e3bdf430 lib/ur/list.urs --- 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 diff -r 9f0ea203a1ca -r 74a1e3bdf430 lib/ur/listPair.ur --- 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 diff -r 9f0ea203a1ca -r 74a1e3bdf430 lib/ur/listPair.urs --- 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 diff -r 9f0ea203a1ca -r 74a1e3bdf430 lib/ur/option.ur --- 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) diff -r 9f0ea203a1ca -r 74a1e3bdf430 lib/ur/option.urs --- 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 diff -r 9f0ea203a1ca -r 74a1e3bdf430 src/c/urweb.c --- 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; } diff -r 9f0ea203a1ca -r 74a1e3bdf430 src/elaborate.sml --- 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 diff -r 9f0ea203a1ca -r 74a1e3bdf430 src/monoize.sml --- 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