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:                 [] => <xml/>
adamc@796:               | x :: ls => <xml>{f x}{mapX' ls}</xml>
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:                 [] => <xml/>
adam@1539:               | x :: ls => <xml>{f i x}{mapX' (i + 1) ls}</xml>
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 <xml/>
adamc@830:               | x :: ls =>
adamc@830:                 this <- f x;
adamc@830:                 rest <- mapXM' ls;
adamc@830:                 return <xml>{this}{rest}</xml>
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@2095: fun mem [a] (_ : eq a) (x : a) =
adam@2095:     let
adam@2095:         fun mm ls =
adam@2095:             case ls of
adam@2095:                 [] => False
adam@2095:               | y :: ls => y = x || mm ls
adam@2095:     in
adam@2095:         mm
adam@2095:     end
adam@2095: 
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 <xml/>
adam@1768:               | x :: ls =>
adam@1768:                 this <- f i x;
adam@1768:                 rest <- mapXiM' (i+1) ls;
adam@1768:                 return <xml>{this}{rest}</xml>
adam@1768:     in
adam@1768:         mapXiM' 0
adam@1768:     end
adam@1840: 
adam@1840: fun tabulateM [m] (_ : monad m) [a] (f : int -> m a) n =
adam@1840:     let
adam@1840:         fun tabulate' n acc =
adam@1840:             if n <= 0 then
adam@1840:                 return acc
adam@1840:             else
adam@1840:                 (v <- f (n-1);
adam@1840:                  tabulate' (n-1) (v :: acc))
adam@1840:     in
adam@1840:         tabulate' n []
adam@1840:     end