From b7de8e9ac590f9d06df72d22489375b33a6efef9 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 9 Jun 2009 18:11:59 -0400 Subject: Some standard library reorgs and additions; handle mutual datatypes better in Specialize --- lib/ur/list.ur | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'lib/ur/list.ur') diff --git a/lib/ur/list.ur b/lib/ur/list.ur index 2e62facb..b99ef515 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -10,6 +10,17 @@ val show = fn [a] (_ : show a) => mkShow show' end +val eq = fn [a] (_ : eq a) => + let + fun eq' (ls1 : list a) ls2 = + case (ls1, ls2) of + ([], []) => True + | (x1 :: ls1, x2 :: ls2) => x1 = x2 && eq' ls1 ls2 + | _ => False + in + mkEq eq' + end + fun foldl [a] [b] f = let fun foldl' acc ls = @@ -20,6 +31,19 @@ fun foldl [a] [b] f = foldl' end +fun foldlPartial [a] [b] f = + let + fun foldlPartial' acc ls = + case ls of + [] => Some acc + | x :: ls => + case f x acc of + None => None + | Some acc' => foldlPartial' acc' ls + in + foldlPartial' + end + val rev = fn [a] => let fun rev' acc (ls : list a) = -- cgit v1.2.3