From 167258efc314f978a4cd5f248b8d3df2f36f9d6d Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 16 Jun 2009 17:52:44 -0400 Subject: Fix a variable capture bug in nested JavaScript; some more list stuff --- lib/ur/list.ur | 21 +++++++++++++++++---- lib/ur/list.urs | 4 +++- lib/ur/listPair.ur | 8 ++++---- lib/ur/listPair.urs | 4 ++-- 4 files changed, 26 insertions(+), 11 deletions(-) (limited to 'lib') diff --git a/lib/ur/list.ur b/lib/ur/list.ur index b99ef515..d774cc54 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -31,17 +31,17 @@ fun foldl [a] [b] f = foldl' end -fun foldlPartial [a] [b] f = +fun foldlAbort [a] [b] f = let - fun foldlPartial' acc ls = + fun foldlAbort' acc ls = case ls of [] => Some acc | x :: ls => case f x acc of None => None - | Some acc' => foldlPartial' acc' ls + | Some acc' => foldlAbort' acc' ls in - foldlPartial' + foldlAbort' end val rev = fn [a] => @@ -54,6 +54,19 @@ val rev = fn [a] => rev' [] end +fun foldlMapAbort [a] [b] [c] f = + let + fun foldlMapAbort' ls' acc ls = + case ls of + [] => Some (rev ls', acc) + | x :: ls => + case f x acc of + None => None + | Some (x', acc') => foldlMapAbort' (x' :: ls') acc' ls + in + foldlMapAbort' [] + end + val revAppend = fn [a] => let fun ra (ls : list a) acc = diff --git a/lib/ur/list.urs b/lib/ur/list.urs index f5495d41..1b0fced9 100644 --- a/lib/ur/list.urs +++ b/lib/ur/list.urs @@ -4,7 +4,9 @@ val show : a ::: Type -> show a -> show (t a) val eq : a ::: Type -> eq a -> eq (t a) val foldl : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b -val foldlPartial : a ::: Type -> b ::: Type -> (a -> b -> option b) -> b -> t a -> option b +val foldlAbort : a ::: Type -> b ::: Type -> (a -> b -> option b) -> b -> t a -> option b +val foldlMapAbort : a ::: Type -> b ::: Type -> c ::: Type + -> (a -> b -> option (c * b)) -> b -> t a -> option (t c * b) val rev : a ::: Type -> t a -> t a diff --git a/lib/ur/listPair.ur b/lib/ur/listPair.ur index 745e436c..0182af19 100644 --- a/lib/ur/listPair.ur +++ b/lib/ur/listPair.ur @@ -1,15 +1,15 @@ -fun foldlPartial [a] [b] [c] f = +fun foldlAbort [a] [b] [c] f = let - fun foldlPartial' acc ls1 ls2 = + fun foldlAbort' acc ls1 ls2 = case (ls1, ls2) of ([], []) => Some acc | (x1 :: ls1, x2 :: ls2) => (case f x1 x2 acc of None => None - | Some acc' => foldlPartial' acc' ls1 ls2) + | Some acc' => foldlAbort' acc' ls1 ls2) | _ => None in - foldlPartial' + foldlAbort' end fun mapX [a] [b] [ctx ::: {Unit}] f = diff --git a/lib/ur/listPair.urs b/lib/ur/listPair.urs index 310a1a4e..f2287c13 100644 --- a/lib/ur/listPair.urs +++ b/lib/ur/listPair.urs @@ -1,5 +1,5 @@ -val foldlPartial : a ::: Type -> b ::: Type -> c ::: Type - -> (a -> b -> c -> option c) -> c -> list a -> list b -> option c +val foldlAbort : a ::: Type -> b ::: Type -> c ::: Type + -> (a -> b -> c -> option c) -> c -> list a -> list b -> option c val mapX : a ::: Type -> b ::: Type -> ctx ::: {Unit} -> (a -> b -> xml ctx [] []) -> list a -> list b -> xml ctx [] [] -- cgit v1.2.3