diff options
author | 2009-06-07 16:45:00 -0400 | |
---|---|---|
committer | 2009-06-07 16:45:00 -0400 | |
commit | 005fbe2dd67c6ec77282179032f94ffa6cb7788c (patch) | |
tree | 30300e247037398cd77a827ae1c38b96d19baec7 /lib | |
parent | 07249bc2c07b2af3b9decb84ce968e3005a19c0f (diff) |
Fix datatype import bug in Elaborate; fix server-side source setting; more standard library stuff
Diffstat (limited to 'lib')
-rw-r--r-- | lib/ur/basis.urs | 1 | ||||
-rw-r--r-- | lib/ur/list.ur | 12 | ||||
-rw-r--r-- | lib/ur/list.urs | 3 | ||||
-rw-r--r-- | lib/ur/listPair.ur | 11 | ||||
-rw-r--r-- | lib/ur/listPair.urs | 2 | ||||
-rw-r--r-- | lib/ur/option.ur | 5 | ||||
-rw-r--r-- | lib/ur/option.urs | 2 |
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 |