summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-22 17:39:55 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-22 17:39:55 -0500
commitadcf93304e6fc100d0e714a898033d2a9033173c (patch)
treea2766814d1fec880c763910917d1e4771455320a /lib
parent1f7d0c20ae30c11cdc64a2c2fc90f15cdf02c34b (diff)
demo/sum working with manual folders
Diffstat (limited to 'lib')
-rw-r--r--lib/ur/top.ur13
-rw-r--r--lib/ur/top.urs6
2 files changed, 19 insertions, 0 deletions
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 9016fd27..5d2ae606 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -6,6 +6,19 @@ con folder = K ==> fn r :: {K} =>
-> 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
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index d891c80d..d4cd34f4 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -6,6 +6,12 @@ con folder = K ==> fn r :: {K} =>
-> 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