Mercurial > urweb
annotate lib/ur/list.ur @ 831:5e1a4b12c83a
strcspn and friends
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 31 May 2009 12:41:34 -0400 |
parents | d07980bf1444 |
children | b2413e4dd109 |
rev | line source |
---|---|
adamc@794 | 1 datatype t = datatype Basis.list |
adamc@794 | 2 |
adamc@826 | 3 val show = fn [a] (_ : show a) => |
adamc@826 | 4 let |
adamc@826 | 5 fun show' (ls : list a) = |
adamc@826 | 6 case ls of |
adamc@826 | 7 [] => "[]" |
adamc@826 | 8 | x :: ls => show x ^ " :: " ^ show' ls |
adamc@826 | 9 in |
adamc@826 | 10 mkShow show' |
adamc@826 | 11 end |
adamc@794 | 12 |
adamc@826 | 13 val rev = fn [a] => |
adamc@826 | 14 let |
adamc@826 | 15 fun rev' acc (ls : list a) = |
adamc@826 | 16 case ls of |
adamc@826 | 17 [] => acc |
adamc@826 | 18 | x :: ls => rev' (x :: acc) ls |
adamc@826 | 19 in |
adamc@826 | 20 rev' [] |
adamc@826 | 21 end |
adamc@794 | 22 |
adamc@826 | 23 val revAppend = fn [a] => |
adamc@826 | 24 let |
adamc@826 | 25 fun ra (ls : list a) acc = |
adamc@826 | 26 case ls of |
adamc@826 | 27 [] => acc |
adamc@826 | 28 | x :: ls => ra ls (x :: acc) |
adamc@826 | 29 in |
adamc@826 | 30 ra |
adamc@826 | 31 end |
adamc@821 | 32 |
adamc@826 | 33 fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2 |
adamc@821 | 34 |
adamc@826 | 35 fun mp [a] [b] f = |
adamc@794 | 36 let |
adamc@794 | 37 fun mp' acc ls = |
adamc@794 | 38 case ls of |
adamc@794 | 39 [] => rev acc |
adamc@794 | 40 | x :: ls => mp' (f x :: acc) ls |
adamc@794 | 41 in |
adamc@794 | 42 mp' [] |
adamc@794 | 43 end |
adamc@796 | 44 |
adamc@826 | 45 fun mapPartial [a] [b] f = |
adamc@821 | 46 let |
adamc@821 | 47 fun mp' acc ls = |
adamc@821 | 48 case ls of |
adamc@821 | 49 [] => rev acc |
adamc@821 | 50 | x :: ls => mp' (case f x of |
adamc@821 | 51 None => acc |
adamc@821 | 52 | Some y => y :: acc) ls |
adamc@821 | 53 in |
adamc@821 | 54 mp' [] |
adamc@821 | 55 end |
adamc@821 | 56 |
adamc@826 | 57 fun mapX [a] [ctx ::: {Unit}] f = |
adamc@796 | 58 let |
adamc@796 | 59 fun mapX' ls = |
adamc@796 | 60 case ls of |
adamc@796 | 61 [] => <xml/> |
adamc@796 | 62 | x :: ls => <xml>{f x}{mapX' ls}</xml> |
adamc@796 | 63 in |
adamc@796 | 64 mapX' |
adamc@796 | 65 end |
adamc@800 | 66 |
adamc@826 | 67 fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f = |
adamc@800 | 68 let |
adamc@800 | 69 fun mapM' acc ls = |
adamc@800 | 70 case ls of |
adamc@818 | 71 [] => return (rev acc) |
adamc@818 | 72 | x :: ls => x' <- f x; mapM' (x' :: acc) ls |
adamc@800 | 73 in |
adamc@818 | 74 mapM' [] |
adamc@800 | 75 end |
adamc@821 | 76 |
adamc@830 | 77 fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f = |
adamc@830 | 78 let |
adamc@830 | 79 fun mapXM' ls = |
adamc@830 | 80 case ls of |
adamc@830 | 81 [] => return <xml/> |
adamc@830 | 82 | x :: ls => |
adamc@830 | 83 this <- f x; |
adamc@830 | 84 rest <- mapXM' ls; |
adamc@830 | 85 return <xml>{this}{rest}</xml> |
adamc@830 | 86 in |
adamc@830 | 87 mapXM' |
adamc@830 | 88 end |
adamc@830 | 89 |
adamc@826 | 90 fun filter [a] f = |
adamc@821 | 91 let |
adamc@821 | 92 fun fil acc ls = |
adamc@821 | 93 case ls of |
adamc@821 | 94 [] => rev acc |
adamc@821 | 95 | x :: ls => fil (if f x then x :: acc else acc) ls |
adamc@821 | 96 in |
adamc@821 | 97 fil [] |
adamc@821 | 98 end |
adamc@822 | 99 |
adamc@826 | 100 fun exists [a] f = |
adamc@822 | 101 let |
adamc@822 | 102 fun ex ls = |
adamc@822 | 103 case ls of |
adamc@822 | 104 [] => False |
adamc@822 | 105 | x :: ls => |
adamc@822 | 106 if f x then |
adamc@822 | 107 True |
adamc@822 | 108 else |
adamc@822 | 109 ex ls |
adamc@822 | 110 in |
adamc@822 | 111 ex |
adamc@822 | 112 end |
adamc@822 | 113 |
adamc@826 | 114 fun foldlMap [a] [b] [c] f = |
adamc@822 | 115 let |
adamc@822 | 116 fun fold ls' st ls = |
adamc@822 | 117 case ls of |
adamc@822 | 118 [] => (rev ls', st) |
adamc@822 | 119 | x :: ls => |
adamc@822 | 120 case f x st of |
adamc@822 | 121 (y, st) => fold (y :: ls') st ls |
adamc@822 | 122 in |
adamc@822 | 123 fold [] |
adamc@822 | 124 end |