src/Pure/library.ML
changeset 12284 131e743d168a
parent 12260 4898247d0102
child 12295 83f747db967c
equal deleted inserted replaced
12283:d42aa776889e 12284:131e743d168a
     1 (*  Title:      Pure/library.ML
     1 (*  Title:      Pure/library.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Author:	Markus Wenzel, TU Munich
     4     Author:     Markus Wenzel, TU Munich
     5     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6 
     6 
     7 Basic library: functions, options, pairs, booleans, lists, integers,
     7 Basic library: functions, options, pairs, booleans, lists, integers,
     8 strings, lists as sets, association lists, generic tables, balanced
     8 strings, lists as sets, association lists, generic tables, balanced
     9 trees, orders, I/O and diagnostics, timing, misc.
     9 trees, orders, I/O and diagnostics, timing, misc.
   209   val gen_assoc: ('a * 'b -> bool) -> ('b * 'c) list * 'a -> 'c option
   209   val gen_assoc: ('a * 'b -> bool) -> ('b * 'c) list * 'a -> 'c option
   210   val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
   210   val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
   211   val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
   211   val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
   212   val gen_overwrite: ('a * 'a -> bool) -> ('a * 'b) list * ('a * 'b) -> ('a * 'b) list
   212   val gen_overwrite: ('a * 'a -> bool) -> ('a * 'b) list * ('a * 'b) -> ('a * 'b) list
   213 
   213 
   214   (*generic tables*)
   214   (*lists as tables*)
   215   val generic_extend: ('a * 'a -> bool)
   215   val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
   216     -> ('b -> 'a list) -> ('a list -> 'b) -> 'b -> 'a list -> 'b
   216   val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
   217   val generic_merge: ('a * 'a -> bool) -> ('b -> 'a list) -> ('a list -> 'b) -> 'b -> 'b -> 'b
       
   218   val extend_list: ''a list -> ''a list -> ''a list
       
   219   val merge_lists: ''a list -> ''a list -> ''a list
   217   val merge_lists: ''a list -> ''a list -> ''a list
       
   218   val merge_lists': ''a list -> ''a list -> ''a list
   220   val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
   219   val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
   221   val merge_rev_lists: ''a list -> ''a list -> ''a list
       
   222 
   220 
   223   (*balanced trees*)
   221   (*balanced trees*)
   224   exception Balance
   222   exception Balance
   225   val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a
   223   val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a
   226   val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a
   224   val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a
   878   | (x :: xs) inter_string ys =
   876   | (x :: xs) inter_string ys =
   879       if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
   877       if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
   880 
   878 
   881 (*generalized intersection*)
   879 (*generalized intersection*)
   882 fun gen_inter eq ([], ys) = []
   880 fun gen_inter eq ([], ys) = []
   883   | gen_inter eq (x::xs, ys) = 
   881   | gen_inter eq (x::xs, ys) =
   884       if gen_mem eq (x,ys) then x :: gen_inter eq (xs, ys)
   882       if gen_mem eq (x,ys) then x :: gen_inter eq (xs, ys)
   885 	                   else      gen_inter eq (xs, ys);
   883                            else      gen_inter eq (xs, ys);
   886 
   884 
   887 
   885 
   888 (*subset*)
   886 (*subset*)
   889 fun [] subset ys = true
   887 fun [] subset ys = true
   890   | (x :: xs) subset ys = x mem ys andalso xs subset ys;
   888   | (x :: xs) subset ys = x mem ys andalso xs subset ys;
  1011             if eq (keyi, key) then p :: pairs else q :: (over pairs)
  1009             if eq (keyi, key) then p :: pairs else q :: (over pairs)
  1012         | over [] = [p]
  1010         | over [] = [p]
  1013   in over al end;
  1011   in over al end;
  1014 
  1012 
  1015 
  1013 
  1016 
  1014 (* lists as tables *)
  1017 (** generic tables **)
  1015 
  1018 
  1016 fun gen_merge_lists _ xs [] = xs
  1019 (*Tables are supposed to be 'efficient' encodings of lists of elements distinct
  1017   | gen_merge_lists _ [] ys = ys
  1020   wrt. an equality "eq". The extend and merge operations below are optimized
  1018   | gen_merge_lists eq xs ys = xs @ gen_rems eq (ys, xs);
  1021   for long-term space efficiency.*)
  1019 
  1022 
  1020 fun gen_merge_lists' _ xs [] = xs
  1023 (*append (new) elements to a table*)
  1021   | gen_merge_lists' _ [] ys = ys
  1024 fun generic_extend _ _ _ tab [] = tab
  1022   | gen_merge_lists' eq xs ys = gen_rems eq (xs, ys) @ ys;
  1025   | generic_extend eq dest_tab mk_tab tab1 lst2 =
  1023 
  1026       let
  1024 fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
  1027         val lst1 = dest_tab tab1;
  1025 fun merge_lists' xs ys = gen_merge_lists' (op =) xs ys;
  1028         val new_lst2 = gen_rems eq (lst2, lst1);
  1026 fun merge_alists al = gen_merge_lists eq_fst al;
  1029       in
       
  1030         if null new_lst2 then tab1
       
  1031         else mk_tab (lst1 @ new_lst2)
       
  1032       end;
       
  1033 
       
  1034 (*append (new) elements of 2nd table to 1st table*)
       
  1035 fun generic_merge eq dest_tab mk_tab tab1 tab2 =
       
  1036   let
       
  1037     val lst1 = dest_tab tab1;
       
  1038     val lst2 = dest_tab tab2;
       
  1039     val new_lst2 = gen_rems eq (lst2, lst1);
       
  1040   in
       
  1041     if null new_lst2 then tab1
       
  1042     else if gen_subset eq (lst1, lst2) then tab2
       
  1043     else mk_tab (lst1 @ new_lst2)
       
  1044   end;
       
  1045 
       
  1046 
       
  1047 (*lists as tables*)
       
  1048 fun extend_list tab = generic_extend (op =) I I tab;
       
  1049 fun merge_lists tab = generic_merge (op =) I I tab;
       
  1050 fun merge_alists tab = generic_merge eq_fst I I tab;
       
  1051 
       
  1052 fun merge_rev_lists xs [] = xs
       
  1053   | merge_rev_lists [] ys = ys
       
  1054   | merge_rev_lists xs (y :: ys) =
       
  1055       (if y mem xs then I else cons y) (merge_rev_lists xs ys);
       
  1056 
  1027 
  1057 
  1028 
  1058 
  1029 
  1059 (** balanced trees **)
  1030 (** balanced trees **)
  1060 
  1031