adamc@794: datatype t = datatype Basis.list
adamc@794:
adamc@826: val show = fn [a] (_ : show a) =>
adamc@826: let
adamc@826: fun show' (ls : list a) =
adamc@826: case ls of
adamc@826: [] => "[]"
adamc@826: | x :: ls => show x ^ " :: " ^ show' ls
adamc@826: in
adamc@826: mkShow show'
adamc@826: end
adamc@794:
adamc@846: val eq = fn [a] (_ : eq a) =>
adamc@846: let
adamc@846: fun eq' (ls1 : list a) ls2 =
adamc@846: case (ls1, ls2) of
adamc@846: ([], []) => True
adamc@846: | (x1 :: ls1, x2 :: ls2) => x1 = x2 && eq' ls1 ls2
adamc@846: | _ => False
adamc@846: in
adamc@846: mkEq eq'
adamc@846: end
adamc@846:
adamc@1057: fun foldl [a] [b] (f : a -> b -> b) =
adamc@845: let
adamc@845: fun foldl' acc ls =
adamc@845: case ls of
adamc@845: [] => acc
adamc@845: | x :: ls => foldl' (f x acc) ls
adamc@845: in
adamc@845: foldl'
adamc@845: end
adamc@845:
adamc@1057: val rev = fn [a] =>
adamc@1057: let
adamc@1057: fun rev' acc (ls : list a) =
adamc@1057: case ls of
adamc@1057: [] => acc
adamc@1057: | x :: ls => rev' (x :: acc) ls
adamc@1057: in
adamc@1057: rev' []
adamc@1057: end
adamc@1057:
adamc@1057: fun foldr [a] [b] f (acc : b) (ls : list a) = foldl f acc (rev ls)
adamc@1057:
adamc@850: fun foldlAbort [a] [b] f =
adamc@846: let
adamc@850: fun foldlAbort' acc ls =
adamc@846: case ls of
adamc@846: [] => Some acc
adamc@846: | x :: ls =>
adamc@846: case f x acc of
adamc@846: None => None
adamc@850: | Some acc' => foldlAbort' acc' ls
adamc@846: in
adamc@850: foldlAbort'
adamc@846: end
adamc@846:
adamc@916: val length = fn [a] =>
adamc@916: let
adamc@916: fun length' acc (ls : list a) =
adamc@916: case ls of
adamc@916: [] => acc
adamc@916: | _ :: ls => length' (acc + 1) ls
adamc@916: in
adamc@916: length' 0
adamc@916: end
adamc@916:
adamc@850: fun foldlMapAbort [a] [b] [c] f =
adamc@850: let
adamc@850: fun foldlMapAbort' ls' acc ls =
adamc@850: case ls of
adamc@850: [] => Some (rev ls', acc)
adamc@850: | x :: ls =>
adamc@850: case f x acc of
adamc@850: None => None
adamc@850: | Some (x', acc') => foldlMapAbort' (x' :: ls') acc' ls
adamc@850: in
adamc@850: foldlMapAbort' []
adamc@850: end
adamc@850:
adamc@826: val revAppend = fn [a] =>
adamc@826: let
adamc@826: fun ra (ls : list a) acc =
adamc@826: case ls of
adamc@826: [] => acc
adamc@826: | x :: ls => ra ls (x :: acc)
adamc@826: in
adamc@826: ra
adamc@826: end
adamc@821:
adamc@826: fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
adamc@821:
adamc@826: fun mp [a] [b] f =
adamc@794: let
adamc@794: fun mp' acc ls =
adamc@794: case ls of
adamc@794: [] => rev acc
adamc@794: | x :: ls => mp' (f x :: acc) ls
adamc@794: in
adamc@794: mp' []
adamc@794: end
adamc@796:
adamc@1279: fun mapi [a] [b] f =
adamc@1279: let
adamc@1279: fun mp' n acc ls =
adamc@1279: case ls of
adamc@1279: [] => rev acc
adamc@1279: | x :: ls => mp' (n + 1) (f n x :: acc) ls
adamc@1279: in
adamc@1279: mp' 0 []
adamc@1279: end
adamc@1279:
adamc@826: fun mapPartial [a] [b] f =
adamc@821: let
adamc@821: fun mp' acc ls =
adamc@821: case ls of
adamc@821: [] => rev acc
adamc@821: | x :: ls => mp' (case f x of
adamc@821: None => acc
adamc@821: | Some y => y :: acc) ls
adamc@821: in
adamc@821: mp' []
adamc@821: end
adamc@821:
adamc@826: fun mapX [a] [ctx ::: {Unit}] f =
adamc@796: let
adamc@796: fun mapX' ls =
adamc@796: case ls of
adamc@796: [] =>
adamc@796: | x :: ls => {f x}{mapX' ls}
adamc@796: in
adamc@796: mapX'
adamc@796: end
adamc@800:
adam@1539: fun mapXi [a] [ctx ::: {Unit}] f =
adam@1539: let
adam@1539: fun mapX' i ls =
adam@1539: case ls of
adam@1539: [] =>
adam@1539: | x :: ls => {f i x}{mapX' (i + 1) ls}
adam@1539: in
adam@1539: mapX' 0
adam@1539: end
adam@1539:
adamc@826: fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@800: let
adamc@800: fun mapM' acc ls =
adamc@800: case ls of
adamc@818: [] => return (rev acc)
adamc@818: | x :: ls => x' <- f x; mapM' (x' :: acc) ls
adamc@800: in
adamc@818: mapM' []
adamc@800: end
adamc@821:
adamc@1107: fun mapPartialM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@1107: let
adamc@1107: fun mapPartialM' acc ls =
adamc@1107: case ls of
adamc@1107: [] => return (rev acc)
adamc@1107: | x :: ls =>
adamc@1107: v <- f x;
adamc@1107: mapPartialM' (case v of
adamc@1107: None => acc
adamc@1107: | Some x' => x' :: acc) ls
adamc@1107: in
adamc@1107: mapPartialM' []
adamc@1107: end
adamc@1107:
adamc@830: fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
adamc@830: let
adamc@830: fun mapXM' ls =
adamc@830: case ls of
adamc@830: [] => return
adamc@830: | x :: ls =>
adamc@830: this <- f x;
adamc@830: rest <- mapXM' ls;
adamc@830: return {this}{rest}
adamc@830: in
adamc@830: mapXM'
adamc@830: end
adamc@830:
adamc@826: fun filter [a] f =
adamc@821: let
adamc@821: fun fil acc ls =
adamc@821: case ls of
adamc@821: [] => rev acc
adamc@821: | x :: ls => fil (if f x then x :: acc else acc) ls
adamc@821: in
adamc@821: fil []
adamc@821: end
adamc@822:
adamc@826: fun exists [a] f =
adamc@822: let
adamc@822: fun ex ls =
adamc@822: case ls of
adamc@822: [] => False
adamc@822: | x :: ls =>
adamc@822: if f x then
adamc@822: True
adamc@822: else
adamc@822: ex ls
adamc@822: in
adamc@822: ex
adamc@822: end
adamc@822:
adamc@826: fun foldlMap [a] [b] [c] f =
adamc@822: let
adamc@822: fun fold ls' st ls =
adamc@822: case ls of
adamc@822: [] => (rev ls', st)
adamc@822: | x :: ls =>
adamc@822: case f x st of
adamc@822: (y, st) => fold (y :: ls') st ls
adamc@822: in
adamc@822: fold []
adamc@822: end
adamc@839:
adam@1519: fun find [a] f =
adam@1519: let
adam@1519: fun find' ls =
adam@1519: case ls of
adam@1519: [] => None
adam@1519: | x :: ls =>
adam@1519: if f x then
adam@1519: Some x
adam@1519: else
adam@1519: find' ls
adam@1519: in
adam@1519: find'
adam@1519: end
adam@1519:
adamc@839: fun search [a] [b] f =
adamc@839: let
adamc@839: fun search' ls =
adamc@839: case ls of
adamc@839: [] => None
adamc@839: | x :: ls =>
adamc@839: case f x of
adamc@839: None => search' ls
adamc@839: | v => v
adamc@839: in
adamc@839: search'
adamc@839: end
adamc@839:
adamc@840: fun foldlM [m] (_ : monad m) [a] [b] f =
adamc@840: let
adamc@840: fun foldlM' acc ls =
adamc@840: case ls of
adamc@840: [] => return acc
adamc@840: | x :: ls =>
adamc@840: acc <- f x acc;
adamc@840: foldlM' acc ls
adamc@840: in
adamc@840: foldlM'
adamc@840: end
adamc@843:
adam@1547: fun foldlMi [m] (_ : monad m) [a] [b] f =
adam@1547: let
adam@1547: fun foldlMi' i acc ls =
adam@1547: case ls of
adam@1547: [] => return acc
adam@1547: | x :: ls =>
adam@1547: acc <- f i x acc;
adam@1547: foldlMi' (i + 1) acc ls
adam@1547: in
adam@1547: foldlMi' 0
adam@1547: end
adam@1547:
adam@1634: fun filterM [m] (_ : monad m) [a] (p : a -> m bool) =
adam@1634: let
adam@1634: fun filterM' (acc : list a) (xs : list a) : m (list a) =
adam@1634: case xs of
adam@1634: [] => return (rev acc)
adam@1634: | x :: xs =>
adam@1634: c <- p x;
adam@1634: filterM' (if c then x :: acc else acc) xs
adam@1634: in
adam@1634: filterM' []
adam@1634: end
adam@1634:
adamc@843: fun all [m] f =
adamc@843: let
adamc@843: fun all' ls =
adamc@843: case ls of
adamc@843: [] => True
adamc@843: | x :: ls => f x && all' ls
adamc@843: in
adamc@843: all'
adamc@843: end
adamc@844:
adamc@844: fun app [m] (_ : monad m) [a] f =
adamc@844: let
adamc@844: fun app' ls =
adamc@844: case ls of
adamc@844: [] => return ()
adamc@844: | x :: ls =>
adamc@844: f x;
adamc@844: app' ls
adamc@844: in
adamc@844: app'
adamc@844: end
adamc@845:
adamc@908: fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adam@1394: [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@908: (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
adamc@995: ls <- query q
adamc@995: (fn fs acc => return (f fs :: acc))
adamc@995: [];
adamc@995: return (rev ls)
adamc@908:
adamc@1107: fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adam@1394: [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@1107: (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) =
adamc@1107: ls <- query q
adamc@1107: (fn fs acc => v <- f fs; return (v :: acc))
adamc@1107: [];
adamc@1107: return (rev ls)
adamc@1107:
adamc@1107: fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adam@1394: [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@1107: (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) =
adamc@1107: ls <- query q
adamc@1107: (fn fs acc => v <- f fs;
adamc@1107: return (case v of
adamc@1107: None => acc
adamc@1107: | Some v => v :: acc))
adamc@1107: [];
adamc@1107: return (rev ls)
adamc@1107:
adam@1321: fun sort [a] (gt : a -> a -> bool) (ls : t a) : t a =
adam@1321: let
adam@1321: fun split ls acc1 acc2 =
adam@1321: case ls of
adam@1321: [] => (rev acc1, rev acc2)
adam@1321: | x :: [] => (rev (x :: acc1), rev acc2)
adam@1321: | x1 :: x2 :: ls' => split ls' (x1 :: acc1) (x2 :: acc2)
adam@1321:
adam@1321: fun merge ls1 ls2 acc =
adam@1321: case (ls1, ls2) of
adam@1321: ([], _) => revAppend acc ls2
adam@1321: | (_, []) => revAppend acc ls1
adam@1321: | (x1 :: ls1', x2 :: ls2') => if gt x1 x2 then merge ls1 ls2' (x2 :: acc) else merge ls1' ls2 (x1 :: acc)
adam@1321:
adam@1321: fun sort' ls =
adam@1321: case ls of
adam@1321: [] => ls
adam@1321: | _ :: [] => ls
adam@1321: | _ =>
adam@1321: let
adam@1321: val (ls1, ls2) = split ls [] []
adam@1321: in
adam@1321: merge (sort' ls1) (sort' ls2) []
adam@1321: end
adam@1321: in
adam@1321: sort' ls
adam@1321: end
adam@1321:
adam@1322: val nth [a] =
adam@1322: let
adam@1322: fun nth (ls : list a) (n : int) : option a =
adam@1322: case ls of
adam@1322: [] => None
adam@1322: | x :: ls' =>
adam@1322: if n <= 0 then
adam@1322: Some x
adam@1322: else
adam@1322: nth ls' (n-1)
adam@1322: in
adam@1322: nth
adam@1322: end
adam@1322:
adam@1345: fun replaceNth [a] (ls : list a) (n : int) (v : a) : list a =
adam@1345: let
adam@1345: fun repNth (ls : list a) (n : int) (acc : list a) =
adam@1345: case ls of
adam@1345: [] => rev acc
adam@1345: | x :: ls' => if n <= 0 then
adam@1345: revAppend acc (v :: ls')
adam@1345: else
adam@1345: repNth ls' (n-1) (x :: acc)
adam@1345: in
adam@1345: repNth ls n []
adam@1345: end
adam@1345:
adamc@845: fun assoc [a] [b] (_ : eq a) (x : a) =
adamc@845: let
adamc@845: fun assoc' (ls : list (a * b)) =
adamc@845: case ls of
adamc@845: [] => None
adamc@845: | (y, z) :: ls =>
adamc@845: if x = y then
adamc@845: Some z
adamc@845: else
adamc@845: assoc' ls
adamc@845: in
adamc@845: assoc'
adamc@845: end
adamc@845:
adamc@845: fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
adamc@845: case assoc x ls of
adamc@845: None => (x, y) :: ls
adamc@845: | Some _ => ls
greenrd@1481:
greenrd@1481: fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r)
greenrd@1481: = @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs =>
greenrd@1481: x :: xs) [] fl
adam@1634:
adam@1634: fun take [a] (n : int) (xs : list a) : list a =
adam@1634: if n <= 0 then
adam@1634: []
adam@1634: else
adam@1634: case xs of
adam@1634: [] => []
adam@1634: | x :: xs => x :: take (n-1) xs
adam@1634:
adam@1634: fun drop [a] (n : int) (xs : list a) : list a =
adam@1634: if n <= 0 then
adam@1634: xs
adam@1634: else
adam@1634: case xs of
adam@1634: [] => []
adam@1634: | x :: xs => drop (n-1) xs
adam@1634:
adam@1634: fun splitAt [a] (n : int) (xs : list a) : list a * list a =
adam@1634: (take n xs, drop n xs)
adam@1768:
adam@1768: fun mapXiM [m ::: Type -> Type] (_ : monad m) [a] [ctx ::: {Unit}] (f : int -> a -> m (xml ctx [] [])) : t a -> m (xml ctx [] []) =
adam@1768: let
adam@1768: fun mapXiM' i ls =
adam@1768: case ls of
adam@1768: [] => return
adam@1768: | x :: ls =>
adam@1768: this <- f i x;
adam@1768: rest <- mapXiM' (i+1) ls;
adam@1768: return {this}{rest}
adam@1768: in
adam@1768: mapXiM' 0
adam@1768: end