Mercurial > urweb

changeset 627:f4f2b09a533a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
demo/sum working with manual folders
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 17:39:55 -0500
parents 230654093b51
children 12b73f3c108e
files demo/sum.ur lib/ur/top.ur lib/ur/top.urs
diffstat 3 files changed, 24 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/demo/sum.ur	Sun Feb 22 17:17:01 2009 -0500
+++ b/demo/sum.ur	Sun Feb 22 17:39:55 2009 -0500
@@ -1,10 +1,10 @@
-fun sum (fs ::: {Unit}) (x : $(mapUT int fs)) =
+fun sum (fs ::: {Unit}) (fold : folder fs) (x : $(mapUT int fs)) =
     foldUR [int] [fn _ => int]
     (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] n acc => n + acc)
-    0 [fs] x
+    0 [fs] fold x
 
 fun main () = return <xml><body>
-  {[sum {}]}<br/>
-  {[sum {A = 0, B = 1}]}<br/>
-  {[sum {C = 2, D = 3, E = 4}]}
+  {[sum Folder.nil {}]}<br/>
+  {[sum (Folder.cons [#A] [()] (Folder.cons [#B] [()] Folder.nil)) {A = 0, B = 1}]}<br/>
+  {[sum (Folder.cons [#D] [()] (Folder.cons [#C] [()] (Folder.cons [#E] [()] Folder.nil))) {C = 2, D = 3, E = 4}]}
 </body></xml>
--- a/lib/ur/top.ur	Sun Feb 22 17:17:01 2009 -0500
+++ b/lib/ur/top.ur	Sun Feb 22 17:39:55 2009 -0500
@@ -6,6 +6,19 @@
                           -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
                       -> tf [] -> tf r
 
+structure Folder = struct
+    fun nil K (tf :: {K} -> Type)
+            (f : nm :: Name -> v :: K -> r :: {K} -> tf r
+                 -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
+            (i : tf []) = i
+
+    fun cons K (r ::: {K}) (nm :: Name) (v :: K) [[nm] ~ r] (fold : folder r)
+             (tf :: {K} -> Type)
+             (f : nm :: Name -> v :: K -> r :: {K} -> tf r
+                  -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
+             (i : tf []) = f [nm] [v] [r] (fold [tf] f i)
+end
+
 
 fun not b = if b then False else True
 
--- a/lib/ur/top.urs	Sun Feb 22 17:17:01 2009 -0500
+++ b/lib/ur/top.urs	Sun Feb 22 17:39:55 2009 -0500
@@ -6,6 +6,12 @@
                           -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
                       -> tf [] -> tf r
 
+structure Folder : sig
+    val nil : K --> folder (([]) :: {K})
+    val cons : K --> r ::: {K} -> nm :: Name -> v :: K
+               -> fn [[nm] ~ r] => folder r -> folder ([nm = v] ++ r)
+end
+
 
 val not : bool -> bool