src/Pure/library.ML
changeset 13629 a46362d2b19b
parent 13488 a246d390f033
child 13794 332eb2e69a65
equal deleted inserted replaced
13628:87482b5e3f2e 13629:a46362d2b19b
    88   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    88   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    89   val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
    89   val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
    90   val length: 'a list -> int
    90   val length: 'a list -> int
    91   val take: int * 'a list -> 'a list
    91   val take: int * 'a list -> 'a list
    92   val drop: int * 'a list -> 'a list
    92   val drop: int * 'a list -> 'a list
       
    93   val splitAt: int * 'a list -> 'a list * 'a list
    93   val dropwhile: ('a -> bool) -> 'a list -> 'a list
    94   val dropwhile: ('a -> bool) -> 'a list -> 'a list
    94   val nth_elem: int * 'a list -> 'a
    95   val nth_elem: int * 'a list -> 'a
    95   val map_nth_elem: int -> ('a -> 'a) -> 'a list -> 'a list
    96   val map_nth_elem: int -> ('a -> 'a) -> 'a list -> 'a list
    96   val last_elem: 'a list -> 'a
    97   val last_elem: 'a list -> 'a
    97   val split_last: 'a list -> 'a list * 'a
    98   val split_last: 'a list -> 'a list * 'a
   505 (*drop the first n elements from a list*)
   506 (*drop the first n elements from a list*)
   506 fun drop (n, []) = []
   507 fun drop (n, []) = []
   507   | drop (n, x :: xs) =
   508   | drop (n, x :: xs) =
   508       if n > 0 then drop (n - 1, xs) else x :: xs;
   509       if n > 0 then drop (n - 1, xs) else x :: xs;
   509 
   510 
       
   511 fun splitAt(n,[]) = ([],[])
       
   512   | splitAt(n,xs as x::ys) =
       
   513       if n>0 then let val (ps,qs) = splitAt(n-1,ys) in (x::ps,qs) end
       
   514       else ([],xs)
       
   515 
   510 fun dropwhile P [] = []
   516 fun dropwhile P [] = []
   511   | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
   517   | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
   512 
   518 
   513 (*return nth element of a list, where 0 designates the first element;
   519 (*return nth element of a list, where 0 designates the first element;
   514   raise EXCEPTION if list too short*)
   520   raise EXCEPTION if list too short*)
   530 fun split_last [] = raise LIST "split_last"
   536 fun split_last [] = raise LIST "split_last"
   531   | split_last [x] = ([], x)
   537   | split_last [x] = ([], x)
   532   | split_last (x :: xs) = apfst (cons x) (split_last xs);
   538   | split_last (x :: xs) = apfst (cons x) (split_last xs);
   533 
   539 
   534 (*update nth element*)
   540 (*update nth element*)
   535 fun nth_update x (n, xs) =
   541 fun nth_update x n_xs =
   536   let
   542     (case splitAt n_xs of
   537     val prfx = take (n, xs);
   543       (_,[]) => raise LIST "nth_update"
   538     val sffx = drop (n, xs);
   544     | (prfx, _ :: sffx') => prfx @ (x :: sffx'))
   539   in
       
   540     (case sffx of
       
   541       [] => raise LIST "nth_update"
       
   542     | _ :: sffx' => prfx @ (x :: sffx'))
       
   543   end;
       
   544 
   545 
   545 (*find the position of an element in a list*)
   546 (*find the position of an element in a list*)
   546 fun find_index pred =
   547 fun find_index pred =
   547   let fun find _ [] = ~1
   548   let fun find _ [] = ~1
   548         | find n (x :: xs) = if pred x then n else find (n + 1) xs;
   549         | find n (x :: xs) = if pred x then n else find (n + 1) xs;
   564 
   565 
   565 (*flatten a list of lists to a list*)
   566 (*flatten a list of lists to a list*)
   566 fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
   567 fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
   567 
   568 
   568 fun unflat (xs :: xss) ys =
   569 fun unflat (xs :: xss) ys =
   569       let val n = length xs in take (n, ys) :: unflat xss (drop (n, ys)) end
   570       let val (ps,qs) = splitAt(length xs,ys)
       
   571       in ps :: unflat xss qs end
   570   | unflat [] [] = []
   572   | unflat [] [] = []
   571   | unflat _ _ = raise LIST "unflat";
   573   | unflat _ _ = raise LIST "unflat";
   572 
   574 
   573 (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
   575 (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
   574   (proc x1; ...; proc xn) for side effects*)
   576   (proc x1; ...; proc xn) for side effects*)
  1030 
  1032 
  1031 (*balanced folding; avoids deep nesting*)
  1033 (*balanced folding; avoids deep nesting*)
  1032 fun fold_bal f [x] = x
  1034 fun fold_bal f [x] = x
  1033   | fold_bal f [] = raise Balance
  1035   | fold_bal f [] = raise Balance
  1034   | fold_bal f xs =
  1036   | fold_bal f xs =
  1035       let val k = length xs div 2
  1037       let val (ps,qs) = splitAt(length xs div 2, xs)
  1036       in  f (fold_bal f (take(k, xs)),
  1038       in  f (fold_bal f ps, fold_bal f qs)  end;
  1037              fold_bal f (drop(k, xs)))
       
  1038       end;
       
  1039 
  1039 
  1040 (*construct something of the form f(...g(...(x)...)) for balanced access*)
  1040 (*construct something of the form f(...g(...(x)...)) for balanced access*)
  1041 fun access_bal (f, g, x) n i =
  1041 fun access_bal (f, g, x) n i =
  1042   let fun acc n i =     (*1<=i<=n*)
  1042   let fun acc n i =     (*1<=i<=n*)
  1043           if n=1 then x else
  1043           if n=1 then x else