src/Tools/isac/library.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 38022 e6d356fc4d38
child 38051 efdeff9df986
equal deleted inserted replaced
38030:95d956108461 38031:460c24a6a6ba
    31 fun drop (n, []) = [] (*FIXME.2009*)
    31 fun drop (n, []) = [] (*FIXME.2009*)
    32   | drop (n, x :: xs) =
    32   | drop (n, x :: xs) =
    33       if n > 0 then drop (n - 1, xs) else x :: xs;
    33       if n > 0 then drop (n - 1, xs) else x :: xs;
    34 
    34 
    35 (*exn LIST has disappeared in 2009 ... replaced by error...*)
    35 (*exn LIST has disappeared in 2009 ... replaced by error...*)
    36 fun last_elem [] = raise error "last_elem" (*FIXME.2009*)
    36 fun last_elem [] = error "last_elem" (*FIXME.2009*)
    37   | last_elem [x] = x
    37   | last_elem [x] = x
    38   | last_elem (_ :: xs) = last_elem xs;
    38   | last_elem (_ :: xs) = last_elem xs;
    39 
    39 
    40 fun gen_mem eq (x, []) = false (*FIXME.2009*)
    40 fun gen_mem eq (x, []) = false (*FIXME.2009*)
    41   | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
    41   | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
    98   | gen_union eq pr ([], ys) = ys
    98   | gen_union eq pr ([], ys) = ys
    99   | gen_union eq pr (x :: xs, ys) = gen_union eq pr (xs, gen_ins eq (x, ys));
    99   | gen_union eq pr (x :: xs, ys) = gen_union eq pr (xs, gen_ins eq (x, ys));
   100 
   100 
   101 fun cons2 (f,g) x = (f x, g x); (*PL softwareparadigmen*)
   101 fun cons2 (f,g) x = (f x, g x); (*PL softwareparadigmen*)
   102 
   102 
   103 fun nth _ []      = raise error "nth _ []"
   103 fun nth _ []      = error "nth _ []"
   104   | nth 1 (x::_) = x
   104   | nth 1 (x::_) = x
   105   | nth n (_::xs) = nth (n-1) xs;
   105   | nth n (_::xs) = nth (n-1) xs;
   106 (*WN050106 quick for test: doesn't check for exns*)
   106 (*WN050106 quick for test: doesn't check for exns*)
   107 fun drop_nth ls (_, []) = ls
   107 fun drop_nth ls (_, []) = ls
   108   | drop_nth ls (n, x :: xs) = 
   108   | drop_nth ls (n, x :: xs) = 
   266 
   266 
   267 local
   267 local
   268 fun intsto1 0 = []
   268 fun intsto1 0 = []
   269   | intsto1 n = (intsto1 (n-1)) @ [n]
   269   | intsto1 n = (intsto1 (n-1)) @ [n]
   270 in
   270 in
   271 fun intsto n  = if n < 0 then (raise error "intsto < 0") else intsto1 n
   271 fun intsto n  = if n < 0 then (error "intsto < 0") else intsto1 n
   272 end;
   272 end;
   273 
   273 
   274 
   274 
   275 type 'a stack = 'a list;
   275 type 'a stack = 'a list;
   276 fun top ((x::xs):'a stack) = x
   276 fun top ((x::xs):'a stack) = x
   277   | top _ = raise error "top called for empty list";
   277   | top _ = error "top called for empty list";
   278 fun pop ((x::xs):'a stack) = xs:'a stack
   278 fun pop ((x::xs):'a stack) = xs:'a stack
   279   | pop _ = raise error "pop called for empty list";
   279   | pop _ = error "pop called for empty list";
   280 fun push x (xs:'a stack) = x::xs:'a stack;
   280 fun push x (xs:'a stack) = x::xs:'a stack;
   281 
   281 
   282 
   282 
   283 fun drop_last l = ((rev o tl o rev) l);
   283 fun drop_last l = ((rev o tl o rev) l);
   284 fun drop_last_n n l = rev (takerest (n, rev l));
   284 fun drop_last_n n l = rev (takerest (n, rev l));
   293 fun bool2str true = "true"
   293 fun bool2str true = "true"
   294   | bool2str false = "false";
   294   | bool2str false = "false";
   295 
   295 
   296 (*.take elements from b to e including both.*)
   296 (*.take elements from b to e including both.*)
   297 fun take_fromto from to l = 
   297 fun take_fromto from to l = 
   298     if from > to then raise error ("take_fromto from="^string_of_int from^
   298     if from > to then error ("take_fromto from="^string_of_int from^
   299 				  " > to="^string_of_int to)
   299 				  " > to="^string_of_int to)
   300     else drop (from - 1, take (to, l));
   300     else drop (from - 1, take (to, l));
   301 (*> take_fromto 3 5 [1,2,3,4,5,6,7];
   301 (*> take_fromto 3 5 [1,2,3,4,5,6,7];
   302 val it = [3,4,5] : int list 
   302 val it = [3,4,5] : int list 
   303 > take_fromto 3 3  [1,2,3,4,5,6,7];
   303 > take_fromto 3 3  [1,2,3,4,5,6,7];