summaryrefslogtreecommitdiff
path: root/lib/ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-12-27 15:34:11 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2012-12-27 15:34:11 -0500
commit53c633b53e8825cb9058fb88e86d1ca7828b83e6 (patch)
tree94682452c654491c184a8e2d43d3dbfdb4e46cf9 /lib/ur
parentbf6fbd81d4e60a87b19f8c8149349217b4620360 (diff)
Add some name-mangling rules to allow XML attribute 'name' and attributes with dashes
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/list.ur12
-rw-r--r--lib/ur/list.urs3
2 files changed, 15 insertions, 0 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index bce5335e..cbb4faf2 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -437,3 +437,15 @@ fun mapXiM [m ::: Type -> Type] (_ : monad m) [a] [ctx ::: {Unit}] (f : int -> a
in
mapXiM' 0
end
+
+fun tabulateM [m] (_ : monad m) [a] (f : int -> m a) n =
+ let
+ fun tabulate' n acc =
+ if n <= 0 then
+ return acc
+ else
+ (v <- f (n-1);
+ tabulate' (n-1) (v :: acc))
+ in
+ tabulate' n []
+ end
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index b26c9ad9..66007a39 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -63,6 +63,9 @@ 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
+val tabulateM : m ::: (Type -> Type) -> monad m -> a ::: Type
+ -> (int -> m a) -> int -> m (t a)
+
val mapQuery : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
-> [tables ~ exps] =>
sql_query [] [] tables exps