summaryrefslogtreecommitdiff
path: root/lib/ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-06-07 16:45:00 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-06-07 16:45:00 -0400
commit3d7820916ae84710cab458c6b4ba9b1412ee3f5d (patch)
tree30300e247037398cd77a827ae1c38b96d19baec7 /lib/ur
parent818577c761fb4d2ebbddbeb614bfbf33e38b92f6 (diff)
Fix datatype import bug in Elaborate; fix server-side source setting; more standard library stuff
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/basis.urs1
-rw-r--r--lib/ur/list.ur12
-rw-r--r--lib/ur/list.urs3
-rw-r--r--lib/ur/listPair.ur11
-rw-r--r--lib/ur/listPair.urs2
-rw-r--r--lib/ur/option.ur5
-rw-r--r--lib/ur/option.urs2
7 files changed, 36 insertions, 0 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 50909804..c5c4f6f2 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -25,6 +25,7 @@ val eq_string : eq string
val eq_char : eq char
val eq_bool : eq bool
val eq_time : eq time
+val eq_option : t ::: Type -> eq t -> eq (option t)
val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
class num
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 771cddc3..60cd7316 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -171,3 +171,15 @@ fun all [m] f =
in
all'
end
+
+fun app [m] (_ : monad m) [a] f =
+ let
+ fun app' ls =
+ case ls of
+ [] => return ()
+ | x :: ls =>
+ f x;
+ app' ls
+ in
+ app'
+ end
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index 6a653ba9..7906970a 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -35,3 +35,6 @@ val assoc : a ::: Type -> b ::: Type -> eq a -> a -> t (a * b) -> option b
val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b
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
diff --git a/lib/ur/listPair.ur b/lib/ur/listPair.ur
index a46cf187..8d1c873e 100644
--- a/lib/ur/listPair.ur
+++ b/lib/ur/listPair.ur
@@ -8,3 +8,14 @@ fun mapX [a] [b] [ctx ::: {Unit}] f =
in
mapX'
end
+
+fun all [a] [b] f =
+ let
+ fun all' ls1 ls2 =
+ case (ls1, ls2) of
+ ([], []) => True
+ | (x1 :: ls1, x2 :: ls2) => f x1 x2 && all' ls1 ls2
+ | _ => False
+ in
+ all'
+ end
diff --git a/lib/ur/listPair.urs b/lib/ur/listPair.urs
index 55a34b3a..0c5e5443 100644
--- a/lib/ur/listPair.urs
+++ b/lib/ur/listPair.urs
@@ -1,2 +1,4 @@
val mapX : a ::: Type -> b ::: Type -> ctx ::: {Unit}
-> (a -> b -> xml ctx [] []) -> list a -> list b -> xml ctx [] []
+
+val all : a ::: Type -> b ::: Type -> (a -> b -> bool) -> list a -> list b -> bool
diff --git a/lib/ur/option.ur b/lib/ur/option.ur
index cb2a6b57..5ec093c0 100644
--- a/lib/ur/option.ur
+++ b/lib/ur/option.ur
@@ -4,3 +4,8 @@ fun isSome [a] x =
case x of
None => False
| Some _ => True
+
+fun mp [a] [b] f x =
+ case x of
+ None => None
+ | Some y => Some (f y)
diff --git a/lib/ur/option.urs b/lib/ur/option.urs
index 97e52fda..ced6156e 100644
--- a/lib/ur/option.urs
+++ b/lib/ur/option.urs
@@ -1,3 +1,5 @@
datatype t = datatype Basis.option
val isSome : a ::: Type -> t a -> bool
+
+val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b