moved some fundamental concepts to General/basics.ML;
authorwenzelm
Thu Nov 16 01:07:25 2006 +0100 (2006-11-16)
changeset 21395f34ac19659ae
parent 21394 9f20604d2b5e
child 21396 afd8ba74313c
moved some fundamental concepts to General/basics.ML;
src/HOL/Import/lazy_seq.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/old_inductive_package.ML
src/HOL/ex/svc_funcs.ML
src/Provers/IsaPlanner/zipper.ML
src/Pure/General/seq.ML
src/Pure/IsaMakefile
src/Pure/Isar/rule_cases.ML
src/Pure/library.ML
     1.1 --- a/src/HOL/Import/lazy_seq.ML	Thu Nov 16 01:07:23 2006 +0100
     1.2 +++ b/src/HOL/Import/lazy_seq.ML	Thu Nov 16 01:07:25 2006 +0100
     1.3 @@ -453,7 +453,7 @@
     1.4  (*partial function as procedure*)
     1.5  fun try f x =
     1.6      make (fn () =>
     1.7 -	     case Library.try f x of
     1.8 +	     case Basics.try f x of
     1.9  		 SOME y => SOME(y,Seq (value NONE))
    1.10  	       | NONE => NONE)
    1.11  
    1.12 @@ -528,7 +528,7 @@
    1.13      else
    1.14  	case getItem xq of
    1.15  	    NONE => ([], xq)
    1.16 -	  | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))
    1.17 +	  | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1, xq'))
    1.18  
    1.19  fun foldl f e s =
    1.20      let
     2.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Nov 16 01:07:23 2006 +0100
     2.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Nov 16 01:07:25 2006 +0100
     2.3 @@ -295,7 +295,7 @@
     2.4      val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
     2.5      val (_, params) = strip_comb S;
     2.6      val params' = map dest_Var params;
     2.7 -    val rss = [] |> Library.fold add_rule intrs;
     2.8 +    val rss = [] |> fold add_rule intrs;
     2.9      val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
    2.10      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
    2.11  
     3.1 --- a/src/HOL/Tools/old_inductive_package.ML	Thu Nov 16 01:07:23 2006 +0100
     3.2 +++ b/src/HOL/Tools/old_inductive_package.ML	Thu Nov 16 01:07:25 2006 +0100
     3.3 @@ -403,7 +403,7 @@
     3.4  
     3.5      val ind_prems = map mk_ind_prem intr_ts;
     3.6  
     3.7 -    val factors = Library.fold (mg_prod_factors preds) ind_prems [];
     3.8 +    val factors = fold (mg_prod_factors preds) ind_prems [];
     3.9  
    3.10      (* make conclusions for induction rules *)
    3.11  
    3.12 @@ -814,7 +814,7 @@
    3.13  (* external interfaces *)
    3.14  
    3.15  fun try_term f msg thy t =
    3.16 -  (case Library.try f t of
    3.17 +  (case try f t of
    3.18      SOME x => x
    3.19    | NONE => error (msg ^ Sign.string_of_term thy t));
    3.20  
     4.1 --- a/src/HOL/ex/svc_funcs.ML	Thu Nov 16 01:07:23 2006 +0100
     4.2 +++ b/src/HOL/ex/svc_funcs.ML	Thu Nov 16 01:07:25 2006 +0100
     4.3 @@ -73,7 +73,7 @@
     4.4                          " " ^ File.shell_path svc_input_file ^
     4.5                          ">/dev/null 2>&1"))
     4.6        val svc_output =
     4.7 -        (case Library.try File.read svc_output_file of
     4.8 +        (case try File.read svc_output_file of
     4.9            SOME out => out
    4.10          | NONE => error "SVC returned no output");
    4.11    in
     5.1 --- a/src/Provers/IsaPlanner/zipper.ML	Thu Nov 16 01:07:23 2006 +0100
     5.2 +++ b/src/Provers/IsaPlanner/zipper.ML	Thu Nov 16 01:07:25 2006 +0100
     5.3 @@ -215,7 +215,7 @@
     5.4    fun add_outerctxt ctop cbottom = cbottom @ ctop; 
     5.5  
     5.6    (* mkterm : zipper -> trm -> trm *)
     5.7 -  val apply = Library.fold D.apply;
     5.8 +  val apply = Basics.fold D.apply;
     5.9    
    5.10    (* named type context *)
    5.11    val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys
    5.12 @@ -228,7 +228,7 @@
    5.13  
    5.14    val map = List.map : (D.dtrm -> D.dtrm) -> T -> T
    5.15  
    5.16 -  val fold = Library.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
    5.17 +  val fold = Basics.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
    5.18  
    5.19  end;
    5.20  
     6.1 --- a/src/Pure/General/seq.ML	Thu Nov 16 01:07:23 2006 +0100
     6.2 +++ b/src/Pure/General/seq.ML	Thu Nov 16 01:07:25 2006 +0100
     6.3 @@ -80,7 +80,7 @@
     6.4  
     6.5  (*partial function as procedure*)
     6.6  fun try f x =
     6.7 -  (case Library.try f x of
     6.8 +  (case Basics.try f x of
     6.9      SOME y => single y
    6.10    | NONE => empty);
    6.11  
    6.12 @@ -92,7 +92,7 @@
    6.13    else
    6.14      (case pull xq of
    6.15        NONE => ([], xq)
    6.16 -    | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1) xq'));
    6.17 +    | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1) xq'));
    6.18  
    6.19  (*conversion from sequence to list*)
    6.20  fun list_of xq =
     7.1 --- a/src/Pure/IsaMakefile	Thu Nov 16 01:07:23 2006 +0100
     7.2 +++ b/src/Pure/IsaMakefile	Thu Nov 16 01:07:25 2006 +0100
     7.3 @@ -23,16 +23,15 @@
     7.4  
     7.5  Pure: $(OUT)/Pure$(ML_SUFFIX)
     7.6  
     7.7 -$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML		\
     7.8 -  General/buffer.ML General/file.ML General/graph.ML General/heap.ML		\
     7.9 -  General/history.ML General/name_space.ML		\
    7.10 -  General/ord_list.ML General/output.ML General/path.ML				\
    7.11 -  General/position.ML General/pretty.ML General/rat.ML General/scan.ML		\
    7.12 -  General/secure.ML General/seq.ML General/source.ML General/stack.ML		\
    7.13 -  General/susp.ML General/symbol.ML General/table.ML General/url.ML		\
    7.14 -  General/xml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML	\
    7.15 -  Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML			\
    7.16 -  Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML			\
    7.17 +$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML 		\
    7.18 +  General/basics.ML General/buffer.ML General/file.ML General/graph.ML 		\
    7.19 +  General/heap.ML General/history.ML General/name_space.ML General/ord_list.ML	\
    7.20 +  General/output.ML General/path.ML General/position.ML General/pretty.ML	\
    7.21 +  General/rat.ML General/scan.ML General/secure.ML General/seq.ML		\
    7.22 +  General/source.ML General/stack.ML General/susp.ML General/symbol.ML		\
    7.23 +  General/table.ML General/url.ML General/xml.ML Isar/ROOT.ML Isar/antiquote.ML	\
    7.24 +  Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML		\
    7.25 +  Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML	\
    7.26    Isar/induct_attrib.ML Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML	\
    7.27    Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML	\
    7.28    Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML		\
     8.1 --- a/src/Pure/Isar/rule_cases.ML	Thu Nov 16 01:07:23 2006 +0100
     8.2 +++ b/src/Pure/Isar/rule_cases.ML	Thu Nov 16 01:07:25 2006 +0100
     8.3 @@ -234,8 +234,9 @@
     8.4  val save_consumes = put_consumes o lookup_consumes;
     8.5  
     8.6  fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x;
     8.7 +
     8.8  fun consumes_default n x =
     8.9 -  if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
    8.10 +  if is_some (lookup_consumes (#2 x)) then x else consumes n x;
    8.11  
    8.12  
    8.13  
     9.1 --- a/src/Pure/library.ML	Thu Nov 16 01:07:23 2006 +0100
     9.2 +++ b/src/Pure/library.ML	Thu Nov 16 01:07:25 2006 +0100
     9.3 @@ -5,15 +5,16 @@
     9.4  
     9.5  Basic library: functions, options, pairs, booleans, lists, integers,
     9.6  strings, lists as sets, balanced trees, orders, current directory, misc.
     9.7 +
     9.8 +See also General/basics.ML for the most fundamental concepts.
     9.9  *)
    9.10  
    9.11 -infix 1 |> |-> ||> ||>> |>> #> #-> ##> ##>> #>> |>>> ;
    9.12 -infix 2 ?;
    9.13 -infix 3 o oo ooo oooo;
    9.14 -
    9.15 -infix 4 ~~ upto downto;
    9.16 +infix 1 |>>>
    9.17 +infix 2 ?
    9.18 +infix 3 o oo ooo oooo
    9.19 +infix 4 ~~ upto downto
    9.20  infix orf andf \ \\ mem mem_int mem_string union union_int
    9.21 -  union_string inter inter_int inter_string subset subset_int subset_string;
    9.22 +  union_string inter inter_int inter_string subset subset_int subset_string
    9.23  
    9.24  signature BASIC_LIBRARY =
    9.25  sig
    9.26 @@ -22,37 +23,14 @@
    9.27    val K: 'a -> 'b -> 'a
    9.28    val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
    9.29    val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
    9.30 -  val |> : 'a * ('a -> 'b) -> 'b
    9.31 -  val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
    9.32 -  val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
    9.33 -  val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
    9.34 -  val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c
    9.35 -  val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    9.36 -  val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
    9.37 -  val ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd
    9.38 -  val ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd
    9.39 -  val #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b
    9.40    val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    9.41    val ? : ('a -> bool) * ('a -> 'a) -> 'a -> 'a
    9.42 -  val ` : ('b -> 'a) -> 'b -> 'a * 'b
    9.43 -  val tap: ('b -> 'a) -> 'b -> 'b
    9.44    val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    9.45    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    9.46    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    9.47    val funpow: int -> ('a -> 'a) -> 'a -> 'a
    9.48  
    9.49 -  (*options*)
    9.50 -  val the: 'a option -> 'a
    9.51 -  val these: 'a list option -> 'a list
    9.52 -  val the_default: 'a -> 'a option -> 'a
    9.53 -  val the_list: 'a option -> 'a list
    9.54 -  val is_some: 'a option -> bool
    9.55 -  val is_none: 'a option -> bool
    9.56 -  val perhaps: ('a -> 'a option) -> 'a -> 'a
    9.57 -
    9.58    (*exceptions*)
    9.59 -  val try: ('a -> 'b) -> 'a -> 'b option
    9.60 -  val can: ('a -> 'b) -> 'a -> bool
    9.61    exception EXCEPTION of exn * string
    9.62    val do_transform_failure: bool ref
    9.63    val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
    9.64 @@ -102,22 +80,17 @@
    9.65  
    9.66    (*lists*)
    9.67    exception UnequalLengths
    9.68 -  val cons: 'a -> 'a list -> 'a list
    9.69    val single: 'a -> 'a list
    9.70    val the_single: 'a list -> 'a
    9.71    val singleton: ('a list -> 'b list) -> 'a -> 'b
    9.72 -  val append: 'a list -> 'a list -> 'a list
    9.73    val apply: ('a -> 'a) list -> 'a -> 'a
    9.74 -  val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    9.75 -  val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    9.76 -  val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    9.77    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    9.78    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    9.79    val flat: 'a list list -> 'a list
    9.80 -  val maps: ('a -> 'b list) -> 'a list -> 'b list
    9.81    val unflat: 'a list list -> 'b list -> 'b list list
    9.82    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
    9.83    val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
    9.84 +  val maps: ('a -> 'b list) -> 'a list -> 'b list
    9.85    val chop: int -> 'a list -> 'a list * 'a list
    9.86    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    9.87    val nth: 'a list -> int -> 'a
    9.88 @@ -290,36 +263,19 @@
    9.89  structure Library: LIBRARY =
    9.90  struct
    9.91  
    9.92 -
    9.93 -(** functions **)
    9.94 +(* functions *)
    9.95  
    9.96  fun I x = x;
    9.97  fun K x = fn _ => x;
    9.98  fun curry f x y = f (x, y);
    9.99  fun uncurry f (x, y) = f x y;
   9.100  
   9.101 -(*reverse application and structured results*)
   9.102 -fun x |> f = f x;
   9.103 -fun (x, y) |-> f = f x y;
   9.104 -fun (x, y) |>> f = (f x, y);
   9.105 -fun (x, y) ||> f = (x, f y);
   9.106 +(*application and structured results -- old version*)
   9.107  fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
   9.108 -fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
   9.109 -
   9.110 -(*reverse composition and structured results*)
   9.111 -fun f #> g = g o f;
   9.112 -fun f #-> g = uncurry g o f;
   9.113 -fun (f ##> g) x = let val (y, z) = f x in (y, g z) end;
   9.114 -fun (f ##>> g) x = let val (y, z) = f x; val (w, u) = g z in ((y, w), u) end;
   9.115 -fun (f #>> g) x = let val (y, z) = f x in (g y, z) end;
   9.116  
   9.117  (*conditional application*)
   9.118  fun b ? f = fn x => if b x then f x else x;
   9.119  
   9.120 -(*view results*)
   9.121 -fun `f = fn x => (f x, x);
   9.122 -fun tap f = fn x => (f x; x);
   9.123 -
   9.124  (*composition with multiple args*)
   9.125  fun (f oo g) x y = f (g x y);
   9.126  fun (f ooo g) x y z = f (g x y z);
   9.127 @@ -332,28 +288,6 @@
   9.128    in rep (n, x) end;
   9.129  
   9.130  
   9.131 -(** options **)
   9.132 -
   9.133 -val the = Option.valOf;
   9.134 -
   9.135 -fun these (SOME x) = x
   9.136 -  | these _ = [];
   9.137 -
   9.138 -fun the_default x (SOME y) = y
   9.139 -  | the_default x _ = x;
   9.140 -
   9.141 -fun the_list (SOME x) = [x]
   9.142 -  | the_list _ = []
   9.143 -
   9.144 -fun is_some (SOME _) = true
   9.145 -  | is_some NONE = false;
   9.146 -
   9.147 -fun is_none (SOME _) = false
   9.148 -  | is_none NONE = true;
   9.149 -
   9.150 -fun perhaps f x = the_default x (f x);
   9.151 -
   9.152 -
   9.153  (* exceptions *)
   9.154  
   9.155  val do_transform_failure = ref true;
   9.156 @@ -365,13 +299,6 @@
   9.157  
   9.158  exception EXCEPTION of exn * string;
   9.159  
   9.160 -
   9.161 -fun try f x = SOME (f x)
   9.162 -  handle Interrupt => raise Interrupt | _ => NONE;
   9.163 -
   9.164 -fun can f x = is_some (try f x);
   9.165 -
   9.166 -
   9.167  datatype 'a result =
   9.168    Result of 'a |
   9.169    Exn of exn;
   9.170 @@ -409,7 +336,7 @@
   9.171    in ass list end;
   9.172  
   9.173  
   9.174 -(** pairs **)
   9.175 +(* pairs *)
   9.176  
   9.177  fun pair x y = (x, y);
   9.178  fun rpair x y = (y, x);
   9.179 @@ -431,20 +358,16 @@
   9.180  fun string_of_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
   9.181  
   9.182  
   9.183 -(** booleans **)
   9.184 +(* booleans *)
   9.185  
   9.186 -(* equality *)
   9.187 -
   9.188 +(*polymorphic equality*)
   9.189  fun equal x y = x = y;
   9.190  fun not_equal x y = x <> y;
   9.191  
   9.192 -(* operators for combining predicates *)
   9.193 -
   9.194 +(*combining predicates*)
   9.195  fun p orf q = fn x => p x orelse q x;
   9.196  fun p andf q = fn x => p x andalso q x;
   9.197  
   9.198 -(* predicates on lists *)
   9.199 -
   9.200  (*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
   9.201  fun exists (pred: 'a -> bool) : 'a list -> bool =
   9.202    let fun boolf [] = false
   9.203 @@ -481,12 +404,11 @@
   9.204  fun conditional b f = if b then f () else ();
   9.205  
   9.206  
   9.207 +
   9.208  (** lists **)
   9.209  
   9.210  exception UnequalLengths;
   9.211  
   9.212 -fun cons x xs = x :: xs;
   9.213 -
   9.214  fun single x = [x];
   9.215  
   9.216  fun the_single [x] = x
   9.217 @@ -494,35 +416,11 @@
   9.218  
   9.219  fun singleton f x = the_single (f [x]);
   9.220  
   9.221 -fun append xs ys = xs @ ys;
   9.222 -
   9.223  fun apply [] x = x
   9.224    | apply (f :: fs) x = apply fs (f x);
   9.225  
   9.226  
   9.227 -(* fold *)
   9.228 -
   9.229 -fun fold f =
   9.230 -  let
   9.231 -    fun fold_aux [] y = y
   9.232 -      | fold_aux (x :: xs) y = fold_aux xs (f x y);
   9.233 -  in fold_aux end;
   9.234 -
   9.235 -fun fold_rev f =
   9.236 -  let
   9.237 -    fun fold_aux [] y = y
   9.238 -      | fold_aux (x :: xs) y = f x (fold_aux xs y);
   9.239 -  in fold_aux end;
   9.240 -
   9.241 -fun fold_map f =
   9.242 -  let
   9.243 -    fun fold_aux [] y = ([], y)
   9.244 -      | fold_aux (x :: xs) y =
   9.245 -          let
   9.246 -            val (x', y') = f x y;
   9.247 -            val (xs', y'') = fold_aux xs y';
   9.248 -          in (x' :: xs', y'') end;
   9.249 -  in fold_aux end;
   9.250 +(* fold -- old versions *)
   9.251  
   9.252  (*the following versions of fold are designed to fit nicely with infixes*)
   9.253  
   9.254 @@ -570,9 +468,7 @@
   9.255  fun maps f [] = []
   9.256    | maps f (x :: xs) = f x @ maps f xs;
   9.257  
   9.258 -fun chop 0 xs = ([], xs)
   9.259 -  | chop _ [] = ([], [])
   9.260 -  | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
   9.261 +fun chop n xs = unfold_rev n dest xs;
   9.262  
   9.263  (*take the first n elements from a list*)
   9.264  fun take (n, []) = []