src/Pure/library.ML
changeset 2243 3ebeaaacfbd1
parent 2196 1b36ebc70487
child 2271 7c4744ed8fc3
equal deleted inserted replaced
2242:fa8c6c695a97 2243:3ebeaaacfbd1
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Basic library: functions, options, pairs, booleans, lists, integers,
     6 Basic library: functions, options, pairs, booleans, lists, integers,
     7 strings, lists as sets, association lists, generic tables, balanced trees,
     7 strings, lists as sets, association lists, generic tables, balanced trees,
     8 input / output, timing, filenames, misc functions.
     8 input / TextIO.output, timing, filenames, misc functions.
     9 *)
     9 *)
    10 
    10 
    11 infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
    11 infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
    12       mem mem_int mem_string union union_int union_string  
    12       mem mem_int mem_string union union_int union_string  
    13       inter inter_int inter_string subset subset_int subset_string subdir_of;
    13       inter inter_int inter_string subset subset_int subset_string subdir_of;
   504 
   504 
   505 (*removing an element from a list WITHOUT duplicates*)
   505 (*removing an element from a list WITHOUT duplicates*)
   506 fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
   506 fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
   507   | [] \ x = [];
   507   | [] \ x = [];
   508 
   508 
   509 val op \\ = foldl (op \);
   509 fun ys \\ xs = foldl (op \) (ys,xs);
   510 
   510 
   511 (*removing an element from a list -- possibly WITH duplicates*)
   511 (*removing an element from a list -- possibly WITH duplicates*)
   512 fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
   512 fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
   513 
   513 
   514 val gen_rems = foldl o gen_rem;
   514 fun gen_rems eq = foldl (gen_rem eq);
   515 
   515 
   516 
   516 
   517 (*makes a list of the distinct members of the input; preserves order, takes
   517 (*makes a list of the distinct members of the input; preserves order, takes
   518   first of equal elements*)
   518   first of equal elements*)
   519 fun gen_distinct eq lst =
   519 fun gen_distinct eq lst =
   526           else dist (x :: rev_seen, xs);
   526           else dist (x :: rev_seen, xs);
   527   in
   527   in
   528     dist ([], lst)
   528     dist ([], lst)
   529   end;
   529   end;
   530 
   530 
   531 val distinct = gen_distinct (op =);
   531 fun distinct l = gen_distinct (op =) l;
   532 
   532 
   533 
   533 
   534 (*returns the tail beginning with the first repeated element, or []*)
   534 (*returns the tail beginning with the first repeated element, or []*)
   535 fun findrep [] = []
   535 fun findrep [] = []
   536   | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
   536   | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
   549           else dups (x :: rev_dups, xs);
   549           else dups (x :: rev_dups, xs);
   550   in
   550   in
   551     dups ([], lst)
   551     dups ([], lst)
   552   end;
   552   end;
   553 
   553 
   554 val duplicates = gen_duplicates (op =);
   554 fun duplicates l = gen_duplicates (op =) l;
   555 
   555 
   556 
   556 
   557 
   557 
   558 (** association lists **)
   558 (** association lists **)
   559 
   559 
   631     else mk_tab (lst1 @ new_lst2)
   631     else mk_tab (lst1 @ new_lst2)
   632   end;
   632   end;
   633 
   633 
   634 
   634 
   635 (*lists as tables*)
   635 (*lists as tables*)
   636 val extend_list = generic_extend (op =) I I;
   636 fun extend_list tab = generic_extend (op =) I I tab;
   637 val merge_lists = generic_merge (op =) I I;
   637 fun merge_lists tab = generic_merge (op =) I I tab;
   638 
   638 
   639 fun merge_rev_lists xs [] = xs
   639 fun merge_rev_lists xs [] = xs
   640   | merge_rev_lists [] ys = ys
   640   | merge_rev_lists [] ys = ys
   641   | merge_rev_lists xs (y :: ys) =
   641   | merge_rev_lists xs (y :: ys) =
   642       (if y mem xs then I else cons y) (merge_rev_lists xs ys);
   642       (if y mem xs then I else cons y) (merge_rev_lists xs ys);
   678 
   678 
   679 
   679 
   680 
   680 
   681 (** input / output **)
   681 (** input / output **)
   682 
   682 
   683 val prs_fn = ref(fn s => output (std_out, s));
   683 val cd = OS.FileSys.chDir;
       
   684 
       
   685 val prs_fn = ref(fn s => TextIO.output (TextIO.stdOut, s));
   684 
   686 
   685 fun prs s = !prs_fn s;
   687 fun prs s = !prs_fn s;
   686 fun writeln s = prs (s ^ "\n");
   688 fun writeln s = prs (s ^ "\n");
   687 
   689 
   688 (* output to LaTeX / xdvi *)
   690 (* TextIO.output to LaTeX / xdvi *)
   689 fun latex s = 
   691 fun latex s = 
   690 	execute ( "( cd /tmp ; echo \"" ^ s ^
   692         execute ( "( cd /tmp ; echo \"" ^ s ^
   691 	"\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &" ) ;
   693         "\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &" ) ;
   692 
   694 
   693 (*print warning*)
   695 (*print warning*)
   694 val warning_fn = ref(fn s => output (std_out, s ^ "\n"));
   696 val warning_fn = ref(fn s => TextIO.output (TextIO.stdOut, s ^ "\n"));
   695 fun warning s = !warning_fn ("Warning: " ^ s);
   697 fun warning s = !warning_fn ("Warning: " ^ s);
   696 
   698 
   697 (*print error message and abort to top level*)
   699 (*print error message and abort to top level*)
   698 
   700 
   699 val error_fn = ref(fn s => output (std_out, s ^ "\n"));
   701 val error_fn = ref(fn s => TextIO.output (TextIO.stdOut, s ^ "\n"));
   700 
   702 
   701 exception ERROR;
   703 exception ERROR;
   702 fun error msg = (!error_fn msg; raise ERROR);
   704 fun error msg = (!error_fn msg; raise ERROR);
   703 fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
   705 fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
   704 
   706 
   706 fun deny p msg = if p then error msg else ();
   708 fun deny p msg = if p then error msg else ();
   707 
   709 
   708 (*Assert pred for every member of l, generating a message if pred fails*)
   710 (*Assert pred for every member of l, generating a message if pred fails*)
   709 fun assert_all pred l msg_fn = 
   711 fun assert_all pred l msg_fn = 
   710   let fun asl [] = ()
   712   let fun asl [] = ()
   711 	| asl (x::xs) = if pred x then asl xs
   713         | asl (x::xs) = if pred x then asl xs
   712 	                else error (msg_fn x)
   714                         else error (msg_fn x)
   713   in  asl l  end;
   715   in  asl l  end;
   714 
   716 
   715 (*for the "test" target in Makefiles -- signifies successful termination*)
   717 (*for the "test" target in Makefiles -- signifies successful termination*)
   716 fun maketest msg =
   718 fun maketest msg =
   717   (writeln msg; 
   719   (writeln msg; 
   718    let val os = open_out "test" 
   720    let val os = TextIO.openOut "test" 
   719    in  output (os, "Test examples ran successfully\n");
   721    in  TextIO.output (os, "Test examples ran successfully\n");
   720        close_out os
   722        TextIO.closeOut os
   721    end);
   723    end);
   722 
   724 
   723 
   725 
   724 (*print a list surrounded by the brackets lpar and rpar, with comma separator
   726 (*print a list surrounded by the brackets lpar and rpar, with comma separator
   725   print nothing for empty list*)
   727   print nothing for empty list*)
   741 
   743 
   742 
   744 
   743 (** timing **)
   745 (** timing **)
   744 
   746 
   745 (*unconditional timing function*)
   747 (*unconditional timing function*)
   746 val timeit = cond_timeit true;
   748 fun timeit x = cond_timeit true x;
   747 
   749 
   748 (*timed application function*)
   750 (*timed application function*)
   749 fun timeap f x = timeit (fn () => f x);
   751 fun timeap f x = timeit (fn () => f x);
   750 
   752 
   751 (*timed "use" function, printing filenames*)
   753 (*timed "use" function, printing filenames*)
   877 fun transitive_closure [] = []
   879 fun transitive_closure [] = []
   878   | transitive_closure ((x, ys)::ps) =
   880   | transitive_closure ((x, ys)::ps) =
   879       let val qs = transitive_closure ps
   881       let val qs = transitive_closure ps
   880           val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
   882           val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
   881           fun step(u, us) = (u, if x mem_string us then zs union_string us 
   883           fun step(u, us) = (u, if x mem_string us then zs union_string us 
   882 				else us)
   884                                 else us)
   883       in (x, zs) :: map step qs end;
   885       in (x, zs) :: map step qs end;
   884 
   886 
   885 
   887 
   886 (** Recommended by Stephen K. Park and Keith W. Miller, 
   888 (** Recommended by Stephen K. Park and Keith W. Miller, 
   887       Random number generators: good ones are hard to find,
   889       Random number generators: good ones are hard to find,
   915 
   917 
   916 (*Randomly generated identifiers with given prefix; MUST start with a letter
   918 (*Randomly generated identifiers with given prefix; MUST start with a letter
   917     [division by two avoids overflow for ML systems whose maxint is 2^30 - 1 *)
   919     [division by two avoids overflow for ML systems whose maxint is 2^30 - 1 *)
   918 fun gensym pre = pre ^ 
   920 fun gensym pre = pre ^ 
   919                  (#1(newid (floor (!seedr/2.0)), 
   921                  (#1(newid (floor (!seedr/2.0)), 
   920 		     seedr := nextrandom (!seedr)))
   922                      seedr := nextrandom (!seedr)))
   921 
   923 
   922 (*Increment a list of letters like a reversed base 26 number.
   924 (*Increment a list of letters like a reversed base 26 number.
   923   If head is "z", bumps chars in tail.
   925   If head is "z", bumps chars in tail.
   924   Digits are incremented as if they were integers.
   926   Digits are incremented as if they were integers.
   925   "_" and "'" are not changed.
   927   "_" and "'" are not changed.