src/Pure/library.ML
changeset 14826 48cfe0fe53e2
parent 14797 546365fe8349
child 14868 617e4b19a2e5
     1.1 --- a/src/Pure/library.ML	Sat May 29 15:01:36 2004 +0200
     1.2 +++ b/src/Pure/library.ML	Sat May 29 15:02:13 2004 +0200
     1.3 @@ -5,8 +5,8 @@
     1.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.5  
     1.6  Basic library: functions, options, pairs, booleans, lists, integers,
     1.7 -strings, lists as sets, association lists, generic tables, balanced
     1.8 -trees, orders, I/O and diagnostics, timing, misc.
     1.9 +rational numbers, strings, lists as sets, association lists, generic
    1.10 +tables, balanced trees, orders, current directory, misc.
    1.11  *)
    1.12  
    1.13  infix |> |>> |>>> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
    1.14 @@ -44,6 +44,7 @@
    1.15    val is_some: 'a option -> bool
    1.16    val is_none: 'a option -> bool
    1.17    val apsome: ('a -> 'b) -> 'a option -> 'b option
    1.18 +  exception ERROR
    1.19    val try: ('a -> 'b) -> 'a -> 'b option
    1.20    val can: ('a -> 'b) -> 'a -> bool
    1.21  
    1.22 @@ -138,9 +139,13 @@
    1.23    val radixstring: int * string * int -> string
    1.24    val string_of_int: int -> string
    1.25    val string_of_indexname: string * int -> string
    1.26 +  val read_radixint: int * string list -> int * string list
    1.27 +  val read_int: string list -> int * string list
    1.28 +  val oct_char: string -> string
    1.29  
    1.30    (*rational numbers*)
    1.31    type rat
    1.32 +  exception RAT of string
    1.33    val rep_rat: rat -> int * int
    1.34    val ratadd: rat * rat -> rat
    1.35    val ratmul: rat * rat -> rat
    1.36 @@ -161,11 +166,8 @@
    1.37    val commas_quote: string list -> string
    1.38    val cat_lines: string list -> string
    1.39    val space_explode: string -> string -> string list
    1.40 -  val std_output: string -> unit
    1.41 -  val std_error: string -> unit
    1.42 -  val writeln_default: string -> unit
    1.43 +  val split_lines: string -> string list
    1.44    val prefix_lines: string -> string -> string
    1.45 -  val split_lines: string -> string list
    1.46    val untabify: string list -> string list
    1.47    val suffix: string -> string -> string
    1.48    val unsuffix: string -> string -> string
    1.49 @@ -213,7 +215,6 @@
    1.50    val assoc2: (''a * (''b * 'c) list) list * (''a * ''b) -> 'c option
    1.51    val gen_assoc: ('a * 'b -> bool) -> ('b * 'c) list * 'a -> 'c option
    1.52    val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
    1.53 -  val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
    1.54    val gen_overwrite: ('a * 'a -> bool) -> ('a * 'b) list * ('a * 'b) -> ('a * 'b) list
    1.55  
    1.56    (*lists as tables*)
    1.57 @@ -249,42 +250,9 @@
    1.58    val one_of: 'a list -> 'a
    1.59    val frequency: (int * 'a) list -> 'a
    1.60  
    1.61 -  (*I/O and diagnostics*)
    1.62 +  (*current directory*)
    1.63    val cd: string -> unit
    1.64    val pwd: unit -> string
    1.65 -  val writeln_fn: (string -> unit) ref
    1.66 -  val priority_fn: (string -> unit) ref
    1.67 -  val tracing_fn: (string -> unit) ref
    1.68 -  val warning_fn: (string -> unit) ref
    1.69 -  val error_fn: (string -> unit) ref
    1.70 -  val writeln: string -> unit
    1.71 -  val priority: string -> unit
    1.72 -  val tracing: string -> unit
    1.73 -  val warning: string -> unit
    1.74 -  exception ERROR
    1.75 -  val error_msg: string -> unit
    1.76 -  val error: string -> 'a
    1.77 -  val sys_error: string -> 'a
    1.78 -  val assert: bool -> string -> unit
    1.79 -  val deny: bool -> string -> unit
    1.80 -  val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
    1.81 -  datatype 'a error = Error of string | OK of 'a
    1.82 -  val get_error: 'a error -> string option
    1.83 -  val get_ok: 'a error -> 'a option
    1.84 -  datatype 'a result = Result of 'a | Exn of exn
    1.85 -  val get_result: 'a result -> 'a option
    1.86 -  val get_exn: 'a result -> exn option
    1.87 -  val handle_error: ('a -> 'b) -> 'a -> 'b error
    1.88 -  exception ERROR_MESSAGE of string
    1.89 -  val transform_error: ('a -> 'b) -> 'a -> 'b
    1.90 -  val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
    1.91 -
    1.92 -  (*timing*)
    1.93 -  val cond_timeit: bool -> (unit -> 'a) -> 'a
    1.94 -  val timeit: (unit -> 'a) -> 'a
    1.95 -  val timeap: ('a -> 'b) -> 'a -> 'b
    1.96 -  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
    1.97 -  val timing: bool ref
    1.98  
    1.99    (*misc*)
   1.100    val make_keylist: ('a -> 'b) -> 'a list -> ('a * 'b) list
   1.101 @@ -294,7 +262,6 @@
   1.102    val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   1.103    val gensym: string -> string
   1.104    val scanwords: (string -> bool) -> string list -> string list
   1.105 -  datatype 'a mtree = Join of 'a * 'a mtree list
   1.106  end;
   1.107  
   1.108  structure Library: LIBRARY =
   1.109 @@ -429,7 +396,7 @@
   1.110  
   1.111  fun change r f = r := f (! r);
   1.112  
   1.113 -(*temporarily set flag, handling errors*)
   1.114 +(*temporarily set flag, handling exceptions*)
   1.115  fun setmp flag value f x =
   1.116    let
   1.117      val orig_value = ! flag;
   1.118 @@ -749,6 +716,24 @@
   1.119    | string_of_indexname (a,i) = a ^ "_" ^ Int.toString i;
   1.120  
   1.121  
   1.122 +(* read integers *)
   1.123 +
   1.124 +fun read_radixint (radix: int, cs) : int * string list =
   1.125 +  let val zero = ord"0"
   1.126 +      val limit = zero+radix
   1.127 +      fun scan (num,[]) = (num,[])
   1.128 +        | scan (num, c::cs) =
   1.129 +              if  zero <= ord c  andalso  ord c < limit
   1.130 +              then scan(radix*num + ord c - zero, cs)
   1.131 +              else (num, c::cs)
   1.132 +  in  scan(0,cs)  end;
   1.133 +
   1.134 +fun read_int cs = read_radixint (10, cs);
   1.135 +
   1.136 +fun oct_char s = chr (#1 (read_radixint (8, explode s)));
   1.137 +
   1.138 +
   1.139 +
   1.140  (** strings **)
   1.141  
   1.142  (*functions tuned for strings, avoiding explode*)
   1.143 @@ -794,6 +779,9 @@
   1.144  
   1.145  val split_lines = space_explode "\n";
   1.146  
   1.147 +fun prefix_lines "" txt = txt
   1.148 +  | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
   1.149 +
   1.150  (*untabify*)
   1.151  fun untabify chs =
   1.152    let
   1.153 @@ -1184,126 +1172,19 @@
   1.154    in pick (random_range 1 sum) xs end;
   1.155  
   1.156  
   1.157 -(** input / output and diagnostics **)
   1.158 +(** current directory **)
   1.159  
   1.160  val cd = OS.FileSys.chDir;
   1.161  val pwd = OS.FileSys.getDir;
   1.162  
   1.163 -fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
   1.164 -fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
   1.165 -
   1.166 -fun prefix_lines "" txt = txt
   1.167 -  | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
   1.168 -
   1.169 -val writeln_default = std_output o suffix "\n";
   1.170 -
   1.171 -(*hooks for various output channels*)
   1.172 -val writeln_fn = ref writeln_default;
   1.173 -val priority_fn = ref (fn s => ! writeln_fn s);
   1.174 -val tracing_fn = ref (fn s => ! writeln_fn s);
   1.175 -val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
   1.176 -val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
   1.177 -
   1.178 -fun writeln s = ! writeln_fn s;
   1.179 -fun priority s = ! priority_fn s;
   1.180 -fun tracing s = ! tracing_fn s;
   1.181 -fun warning s = ! warning_fn s;
   1.182 -
   1.183 -(*print error message and abort to top level*)
   1.184 -
   1.185 -fun error_msg s = ! error_fn s;
   1.186 -fun error s = (error_msg s; raise ERROR);
   1.187 -fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);
   1.188 -
   1.189 -fun assert p msg = if p then () else error msg;
   1.190 -fun deny p msg = if p then error msg else ();
   1.191 -
   1.192 -(*Assert pred for every member of l, generating a message if pred fails*)
   1.193 -fun assert_all pred l msg_fn =
   1.194 -  let fun asl [] = ()
   1.195 -        | asl (x::xs) = if pred x then asl xs else error (msg_fn x)
   1.196 -  in asl l end;
   1.197 -
   1.198 -
   1.199 -(* handle errors capturing messages *)
   1.200 -
   1.201 -datatype 'a error =
   1.202 -  Error of string |
   1.203 -  OK of 'a;
   1.204 -
   1.205 -fun get_error (Error msg) = Some msg
   1.206 -  | get_error _ = None;
   1.207 -
   1.208 -fun get_ok (OK x) = Some x
   1.209 -  | get_ok _ = None;
   1.210 -
   1.211 -datatype 'a result =
   1.212 -  Result of 'a |
   1.213 -  Exn of exn;
   1.214 -
   1.215 -fun get_result (Result x) = Some x
   1.216 -  | get_result _ = None;
   1.217 -
   1.218 -fun get_exn (Exn exn) = Some exn
   1.219 -  | get_exn _ = None;
   1.220 -
   1.221 -fun handle_error f x =
   1.222 -  let
   1.223 -    val buffer = ref ([]: string list);
   1.224 -    fun capture s = buffer := ! buffer @ [s];
   1.225 -    fun err_msg () = if not (null (! buffer)) then error_msg (cat_lines (! buffer)) else ();
   1.226 -  in
   1.227 -    (case Result (setmp error_fn capture f x) handle exn => Exn exn of
   1.228 -      Result y => (err_msg (); OK y)
   1.229 -    | Exn ERROR => Error (cat_lines (! buffer))
   1.230 -    | Exn exn => (err_msg (); raise exn))
   1.231 -  end;
   1.232 -
   1.233 -
   1.234 -(* transform ERROR into ERROR_MESSAGE *)
   1.235 -
   1.236 -exception ERROR_MESSAGE of string;
   1.237 -
   1.238 -fun transform_error f x =
   1.239 -  (case handle_error f x of
   1.240 -    OK y => y
   1.241 -  | Error msg => raise ERROR_MESSAGE msg);
   1.242 -
   1.243 -
   1.244 -(* transform any exception, including ERROR *)
   1.245 -
   1.246 -fun transform_failure exn f x =
   1.247 -  transform_error f x handle Interrupt => raise Interrupt | e => raise exn e;
   1.248 -
   1.249 -
   1.250 -
   1.251 -(** timing **)
   1.252 -
   1.253 -(*a conditional timing function: applies f to () and, if the flag is true,
   1.254 -  prints its runtime on warning channel*)
   1.255 -fun cond_timeit flag f =
   1.256 -  if flag then
   1.257 -    let val start = startTiming()
   1.258 -        val result = f ()
   1.259 -    in warning (endTiming start);  result end
   1.260 -  else f ();
   1.261 -
   1.262 -(*unconditional timing function*)
   1.263 -fun timeit x = cond_timeit true x;
   1.264 -
   1.265 -(*timed application function*)
   1.266 -fun timeap f x = timeit (fn () => f x);
   1.267 -fun timeap_msg s f x = (warning s; timeap f x);
   1.268 -
   1.269 -(*global timing mode*)
   1.270 -val timing = ref false;
   1.271 -
   1.272  
   1.273  
   1.274  (** rational numbers **)
   1.275  
   1.276  datatype rat = Rat of bool * int * int
   1.277  
   1.278 +exception RAT of string;
   1.279 +
   1.280  fun rep_rat(Rat(a,p,q)) = (if a then p else ~p,q)
   1.281  
   1.282  fun ratnorm(a,p,q) = if p=0 then Rat(a,0,1) else
   1.283 @@ -1319,10 +1200,10 @@
   1.284  
   1.285  fun ratmul(Rat(a,p,q),Rat(b,r,s)) = ratnorm(a=b,p*r,q*s)
   1.286  
   1.287 -fun ratinv(Rat(a,p,q)) = if p=0 then error("ratinv") else Rat(a,q,p)
   1.288 +fun ratinv(Rat(a,p,q)) = if p=0 then raise RAT "ratinv" else Rat(a,q,p)
   1.289  
   1.290  fun int_ratdiv(p,q) =
   1.291 -  if q=0 then error("int_ratdiv") else ratnorm(0<=q, p, abs q)
   1.292 +  if q=0 then raise RAT "int_ratdiv" else ratnorm(0<=q, p, abs q)
   1.293  
   1.294  fun ratneg(Rat(b,p,q)) = Rat(not b,p,q);
   1.295  
   1.296 @@ -1331,10 +1212,6 @@
   1.297  
   1.298  (** misc **)
   1.299  
   1.300 -fun overwrite_warn (args as (alist, (a, _))) msg =
   1.301 - (if is_none (assoc (alist, a)) then () else warning msg;
   1.302 -  overwrite args);
   1.303 -
   1.304  (*use the keyfun to make a list of (x, key) pairs*)
   1.305  fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list =
   1.306    let fun keypair x = (x, keyfun x)
   1.307 @@ -1416,11 +1293,6 @@
   1.308    in scan1 (#2 (take_prefix (not o is_let) cs)) end;
   1.309  
   1.310  
   1.311 -
   1.312 -(* Variable-branching trees: for proof terms etc. *)
   1.313 -datatype 'a mtree = Join of 'a * 'a mtree list;
   1.314 -
   1.315 -
   1.316  end;
   1.317  
   1.318  open Library;