src/Pure/NJ.ML

HOL.thy:

"@" is no longer introduced as a "binder" but has its own explicit
translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further
translation rules for abstractions with patterns take care of the rest. This
is very modular and avoids problems with "binders" such as "!" mentioned
below.

let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)

Set.thy:

UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"
above, except that "@" was a "binder" originally.

Prod.thy:

Added new syntax for pttrn which allows arbitrarily nested tuples. Two
translation rules take care of %pttrn. Unfortunately they cannot be
reversed. Hence a little ML-code is used as well.

Note that now "! (x,y). ..." is syntactically valid but leads to a
translation error. This is because "!" is introduced as a "binder" which
means that its translation into lambda-terms is not done by a rewrite rule
(aka macro) but by some fixed ML-code which comes after the rewriting stage
and does not know how to handle patterns. This looks like a minor blemish
since patterns in unbounded quantifiers are not that useful (well, except
maybe in unique existence ...). Ideally, there should be two syntactic
categories:

idts, as we know and love it, which does not admit patterns.
patterns, which is what idts has become now.

There is one more point where patterns are now allowed but don't make sense:

{e | idts . P}

where idts is the list of local variables.

Univ.thy: converted the defs for <++> and <**> into pattern form. It worked
perfectly.

(*  Title:      Pure/NJ
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Compatibility file for Standard ML of New Jersey.
*)

(*** Poly/ML emulation ***)

(*To exit the system with an exit code -- an alternative to ^D *)
val exit = System.Unsafe.CInterface.exit;
fun quit () = exit 0;

(*To change the current directory*)
val cd = System.Directory.cd;

(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
fun print_depth n = (System.Control.Print.printDepth := n div 2;
                     System.Control.Print.printLength := n);


(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)

fun make_pp path pprint =
  let
    open System.PrettyPrint;

    fun pp pps obj =
      pprint obj
        (add_string pps, begin_block pps INCONSISTENT,
          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
          fn () => end_block pps);
  in
    (path, pp)
  end;

fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;


(*** New Jersey ML parameters ***)

(* Suppresses Garbage Collection messages;  default was 2 *)
System.Control.Runtime.gcmessages := 0;

(*redefine to flush its output immediately -- temporary patch suggested
  by Kim Dam Petersen*)
val output = fn(s, t) => (output(s, t); flush_out s);

(*Dummy version of the Poly/ML function*)
fun commit() = ();

(*For use in Makefiles -- saves space*)
fun xML filename banner = (exportML filename;  print(banner^"\n"));

(*** Timing functions ***)

(*Print microseconds, suppressing trailing zeroes*)
fun umakestring 0 = ""
  | umakestring n = chr(ord"0" + n div 100000) ^
                    umakestring(10 * (n mod 100000));

(*A conditional timing function: applies f to () and, if the flag is true,
  prints its runtime. *)
fun cond_timeit flag f =
  if flag then
    let fun string_of_time (System.Timer.TIME {sec, usec}) =
            makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
        open System.Timer;
        val start = start_timer()
        val result = f();
        val nongc = check_timer(start)
        and gc = check_timer_gc(start);
        val both = add_time(nongc, gc)
    in  print("Non GC " ^ string_of_time nongc ^
               "   GC " ^ string_of_time gc ^
               "  both "^ string_of_time both ^ " secs\n");
        result
    end
  else f();


(*** File handling ***)

(*Get time of last modification.*)
local
    open System.Timer;
    open System.Unsafe.SysIO;
in
  fun file_info "" = ""
    | file_info name = makestring (mtime (PATH name));

  val delete_file = unlink;
end;

(*Get pathname of current working directory *)
fun pwd () = System.Directory.getWD ();


(*** ML command execution ***)

fun use_string commands = 
  System.Compile.use_stream (open_string (implode commands));