changeset 1498:8c32c7191bf0

Make 'static' protocol handle unlimited retry
author Adam Chlipala <adam@chlipala.net>
date Fri, 15 Jul 2011 18:55:58 -0400 (2011-07-15)
parents 0b639858200b
children 92c929793d0f
files doc/intro.ur src/c/static.c src/tutorial.sml
diffstat 3 files changed, 31 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/doc/intro.ur	Fri Jul 15 18:45:03 2011 -0400
+++ b/doc/intro.ur	Fri Jul 15 18:55:58 2011 -0400
@@ -73,3 +73,22 @@
 (* begin eval *)
 compose inc inc 3
 (* end *)
+
+(* The "option" type family is like ML's "option" or Haskell's "maybe."  Note that, while Ur follows most syntactic conventions of ML, one key difference is that type families appear before their arguments, as in Haskell. *)
+
+fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None
+
+(* begin hide *)
+fun show_option [t] (_ : show t) : show (option t) =
+    mkShow (fn x => case x of
+                        None => "None"
+                      | Some x => "Some(" ^ show x ^ ")")
+(* end *)
+
+(* begin eval *)
+predecessor 6
+(* end *)
+
+(* begin eval *)
+predecessor 0
+(* end *)
--- a/src/c/static.c	Fri Jul 15 18:45:03 2011 -0400
+++ b/src/c/static.c	Fri Jul 15 18:55:58 2011 -0400
@@ -25,15 +25,18 @@
  
   ctx = uw_init(0, NULL, log_debug);
   uw_set_app(ctx, &uw_application);
-  fk = uw_begin(ctx, argv[1]);
 
-  if (fk == SUCCESS) {
-    uw_print(ctx, 1);
-    puts("");
-    return 0;
-  } else {
-    fprintf(stderr, "Error!\n");
-    return 1;
+  while (1) {
+    fk = uw_begin(ctx, argv[1]);
+
+    if (fk == SUCCESS) {
+      uw_print(ctx, 1);
+      puts("");
+      return 0;
+    } else if (fk != UNLIMITED_RETRY) {
+      fprintf(stderr, "Error: %s\n", uw_error_message(ctx));
+      return 1;
+    }
   }
 }
 
--- a/src/tutorial.sml	Fri Jul 15 18:45:03 2011 -0400
+++ b/src/tutorial.sml	Fri Jul 15 18:55:58 2011 -0400
@@ -79,7 +79,7 @@
                 else
                     let
                         val (befor', after) = Substring.position " </span><span class=\"comment-delimiter\">*)</span>"
-                                                             (Substring.slice (after, 64, NONE))
+                                                                 (Substring.slice (after, 64, NONE))
                     in
                         if Substring.isEmpty after then
                             TextIO.outputSubstr (outf, source)