diff demo/more/dlist.ur @ 1304:f0afe61a6f8b

Tweaking unification fix to apply to demo/more
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 15:37:14 -0400
parents c2fe1dbaceb9
children 68429cfce8db
line wrap: on
line diff
--- a/demo/more/dlist.ur	Sun Oct 10 14:41:03 2010 -0400
+++ b/demo/more/dlist.ur	Sun Oct 10 15:37:14 2010 -0400
@@ -119,7 +119,8 @@
                    end}/>
 </xml>
 
-fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter =
+fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] [])
+    : option int -> list (t * position) -> xml (ctx ++ body) [] [] =
     let
         fun renderFlat' len ls =
             case len of
@@ -233,13 +234,13 @@
                                  None => elems
                                | Some pos => skip pos elems
                      in
-                         return (renderFlat f r.Filter len elems)
+                         return (renderFlat f len elems)
                      end}/>
 </xml>
 
 fun delete pos = pos
 
-fun elements' [t] (dl'' : dlist'' t) =
+fun elements' [t] (dl'' : dlist'' t) : signal (list t) =
     case dl'' of
         Nil => return []
       | Cons (x, dl'') =>
@@ -247,13 +248,13 @@
         tl <- elements' dl'';
         return (x :: tl)
 
-fun elements [t] (dl : dlist t) =
+fun elements [t] (dl : dlist t) : signal (list t) =
     dl' <- signal dl;
     case dl' of
         Empty => return []
       | Nonempty {Head = hd, ...} => elements' hd
 
-fun size' [t] (dl'' : dlist'' t) =
+fun size' [t] (dl'' : dlist'' t) : signal int =
     case dl'' of
         Nil => return 0
       | Cons (x, dl'') =>
@@ -261,13 +262,13 @@
         n <- size' dl'';
         return (n + 1)
 
-fun size [t] (dl : dlist t) =
+fun size [t] (dl : dlist t) : signal int =
     dl' <- signal dl;
     case dl' of
         Empty => return 0
       | Nonempty {Head = hd, ...} => size' hd
 
-fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) =
+fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) : signal int =
     case dl'' of
         Nil => return 0
       | Cons (x, dl'') =>
@@ -276,7 +277,7 @@
         n <- numPassing' f dl'';
         return (if b then n + 1 else n)
 
-fun numPassing [t] (f : t -> signal bool) (dl : dlist t) =
+fun numPassing [t] (f : t -> signal bool) (dl : dlist t) : signal int =
     dl' <- signal dl;
     case dl' of
         Empty => return 0