# HG changeset patch # User wenzelm # Date 866798379 -7200 # Node ID fa14fb9a572c6a42a1070de9faa20ab0096aa9db # Parent d10f100676d85f941f0c11246fe888b2eb9f4692 removed old Makefile and compat files; diff -r d10f100676d8 -r fa14fb9a572c src/Pure/Makefile --- a/src/Pure/Makefile Thu Jun 19 11:31:14 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,61 +0,0 @@ -# $Id$ -######################################################################### -# # -# Makefile for Isabelle (Pure) # -# # -######################################################################### - -#The pure part is common to all systems. -#Object-logics (like FOL) are loaded on top of it. - -#To make the system, cd to this directory and type -# make -f Makefile - -#Environment variable ML_DBASE specifies the initial Poly/ML database, from -# the Poly/ML distribution directory. -#WARNING: Poly/ML parent databases should not be moved! - -#Environment variable ISABELLECOMP specifies the compiler. -#Environment variable ISABELLEBIN specifies the destination directory. -#For Poly/ML, ISABELLEBIN must begin with a / - -BIN = $(ISABELLEBIN) -COMP = $(ISABELLECOMP) -FILES = POLY.ML NJ.ML NJ093.ML NJ1xx.ML ROOT.ML basis.ML library.ML\ - term.ML symtab.ML type.ML sign.ML\ - sequence.ML envir.ML pattern.ML unify.ML logic.ML theory.ML thm.ML\ - net.ML display.ML deriv.ML drule.ML tctical.ML search.ML tactic.ML\ - goals.ML axclass.ML install_pp.ML sorts.ML type_infer.ML\ - NJ093.ML NJ1xx.ML ../Provers/simplifier.ML - -SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\ - Syntax/parser.ML Syntax/type_ext.ML Syntax/syn_trans.ML\ - Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\ - Syntax/syn_ext.ML Syntax/mixfix.ML Syntax/symbol_font.ML\ - Syntax/token_trans.ML - -THY_FILES = Thy/ROOT.ML Thy/thy_scan.ML Thy/thy_parse.ML\ - Thy/thy_syn.ML Thy/thy_read.ML Thy/thm_database.ML - -#Uses cp rather than make_database because Poly/ML allows only 3 levels -$(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE) - @case `basename "$(COMP)"` in \ - poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\ - cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\ - echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \ - | $(COMP) $(BIN)/Pure;\ - discgarb -c $(BIN)/Pure;;\ - sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\ - then echo Bad value for ISABELLEBIN: \ - $(BIN) is not a writable directory; \ - exit 1; \ - fi;\ - echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;' | $(COMP);;\ - *) echo Bad value for ISABELLECOMP: $(COMP); \ - echo " " \"`basename "$(COMP)"`\" is not poly or sml;;\ - esac - - -test: $(BIN)/Pure - -.PRECIOUS: $(BIN)/Pure diff -r d10f100676d8 -r fa14fb9a572c src/Pure/NJ.ML --- a/src/Pure/NJ.ML Thu Jun 19 11:31:14 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* 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. -*) - - -(*Determine if we are running under 0.93 or a newer version of SML/NJ - This is based on the variable "version" defined in 0.93's System structure - which is no longer present in 1.09.*) - -local val version = ""; open System in - val smlversion = if version <> "" then 93 else 109 -end; - -use (if smlversion = 93 then "NJ093.ML" else "NJ1xx.ML"); - - -(** Other functions which are not specific to 0.93 or 1.xx*) - -(*Dummy version of the Poly/ML function*) -fun commit() = (); diff -r d10f100676d8 -r fa14fb9a572c src/Pure/NJ093.ML --- a/src/Pure/NJ093.ML Thu Jun 19 11:31:14 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,125 +0,0 @@ -(* Title: Pure/NJ093.ML - ID: $Id$ - Author: Carsten Clasohm, TU Muenchen - Copyright 1996 TU Muenchen - -Compatibility file for Standard ML of New Jersey version 0.93. -*) - - -use"basis.ML"; - -(*** 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 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; - - -(*** 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; if file doesn't exist return an empty string*) -local - open System.Timer; - open System.Unsafe.SysIO; -in - fun file_info "" = "" - | file_info name = makestring (mtime (PATH name)) handle _ => ""; -end; - -structure OS = - struct - structure FileSys = - struct - val chDir = System.Directory.cd - val remove = System.Unsafe.SysIO.unlink (*Delete a file *) - val getDir = System.Directory.getWD (*path of working directory*) - end - end; - - -(*** ML command execution ***) - -fun use_string commands = - System.Compile.use_stream (open_string (implode commands)); - - -(*** System command execution ***) - -(*Execute an Unix command which doesn't take any input from stdin and - sends its output to stdout. - This could be done more easily by IO.execute, but that function - seems to be buggy in SML/NJ 0.93.*) -fun execute command = - let val tmp_name = "isa_converted.tmp" - val is = (System.system (command ^ " > " ^ tmp_name); - open_in tmp_name); - val result = input (is, 999999); - in close_in is; - OS.FileSys.remove tmp_name; - result - end; - -(*redefine to flush its output immediately -- temporary patch suggested - by Kim Dam Petersen*) -val output = fn(s, t) => (output(s, t); flush_out s); - -(*For use in Makefiles -- saves space*) -fun xML filename banner = (exportML filename; print(banner^"\n")); - - -val needs_filtered_use = false; diff -r d10f100676d8 -r fa14fb9a572c src/Pure/NJ1xx.ML --- a/src/Pure/NJ1xx.ML Thu Jun 19 11:31:14 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,132 +0,0 @@ -(* Title: Pure/NJ1xx.ML - ID: $Id$ - Author: Carsten Clasohm, TU Muenchen - Copyright 1996 TU Muenchen - -Compatibility file for Standard ML of New Jersey version 1.xx. -*) - -(*** Poly/ML emulation ***) - - -(*To exit the system with an exit code -- an alternative to ^D *) -fun exit 0 = OS.Process.exit OS.Process.success - | exit _ = OS.Process.exit OS.Process.failure; -fun quit () = exit 0; - -(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*) -fun print_depth n = (Compiler.Control.Print.printDepth := n div 2; - Compiler.Control.Print.printLength := n); - -(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) - -fun make_pp path pprint = - let - open Compiler.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) = Compiler.PPTable.install_pp path pp; - - -(*** New Jersey ML parameters ***) - -(* Suppresses Garbage Collection messages; doesn't work yet *) -(*System.Runtime.gc 0;*) - -val _ = (Compiler.Control.Print.printLength := 1000; - Compiler.Control.Print.printDepth := 350; - Compiler.Control.Print.stringDepth := 250; - Compiler.Control.Print.signatures := 2); - -(*** Character/string functions which are compatible with 0.93 and Poly/ML ***) - -fun ord s = Char.ord (String.sub(s,0)); -val chr = str o Char.chr; -val explode = (map str) o String.explode; -val implode = String.concat; - - -(*** Timing functions ***) - -(*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 open Time (*...for Time.toString, Time.+ and Time.- *) - val CPUtimer = Timer.startCPUTimer(); - val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer); - val result = f(); - val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer) - in print("User " ^ toString (usrt2-usrt1) ^ - " GC " ^ toString (gct2-gct1) ^ - " All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^ - " secs\n") - handle Time => (); - result - end - else f(); - - -(*** File handling ***) - -(*Get time of last modification; if file doesn't exist return an empty string*) -fun file_info "" = "" - | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>""; - - - -(*** ML command execution ***) - - -(*For version 109.21 and later:*) -val use_string = Compiler.Interact.useStream o TextIO.openString o implode; - -(*For versions prior to 109.21:***** -fun use_string commands = - Compiler.Interact.use_stream (open_string (implode commands)); -*) - -(*** System command execution ***) - -(*Execute an Unix command which doesn't take any input from stdin and - sends its output to stdout. - This could be done more easily by Unix.execute, but that function - doesn't use the PATH.*) -fun execute command = - let val tmp_name = "isa_converted.tmp" - val is = (OS.Process.system (command ^ " > " ^ tmp_name); - TextIO.openIn tmp_name); - val result = TextIO.inputAll is; - in TextIO.closeIn is; - OS.FileSys.remove tmp_name; - result - end; - -(*For exporting images. The short name saves space in Makefiles*) -fun xML filename banner = - let open SMLofNJ - val runtime = hd (SMLofNJ.getAllArgs()) - and exec_file = TextIO.openOut filename - in - TextIO.output (*Write a shell script to invoke the actual image*) - (exec_file, - String.concat - ["#!/bin/sh\n", runtime, - " @SMLdebug=/dev/null", (*suppresses GC messages*) - " @SMLload=", filename, ".heap\n"]); - TextIO.closeOut exec_file; - OS.Process.system ("chmod a+x " ^ filename); - exportML (filename^".heap"); - print(banner^"\n") - end; - - -val needs_filtered_use = false; diff -r d10f100676d8 -r fa14fb9a572c src/Pure/POLY.ML --- a/src/Pure/POLY.ML Thu Jun 19 11:31:14 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,118 +0,0 @@ -(* Title: Pure/POLY - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Compatibility file for Poly/ML (AHL release 1.88) -*) - -open PolyML ExtendedIO; - -use"basis.ML"; - -(*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 val before = System.processtime() - val result = f() - val both = real(System.processtime() - before) / 10.0 - in output(std_out, "Process time (incl GC): "^ - makestring both ^ " secs\n"); - result - end - else f(); - - -(*Save function: in Poly/ML, ignores filename and commits to present file*) - -fun xML filename banner = commit(); - - -(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) - -fun make_pp _ pprint (str, blk, brk, en) obj = - pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), - fn () => brk (99999, 0), en); - - -(*** File handling ***) - -local - -(*These are functions from library.ML *) -fun take_suffix _ [] = ([], []) - | take_suffix pred (x :: xs) = - (case take_suffix pred xs of - ([], sffx) => if pred x then ([], x :: sffx) - else ([x], sffx) - | (prfx, sffx) => (x :: prfx, sffx)); - -fun apr (f,y) x = f(x,y); - -fun seq (proc: 'a -> unit) : 'a list -> unit = - let fun seqf [] = () - | seqf (x :: xs) = (proc x; seqf xs) - in seqf end; - -in - -(*Get time of last modification; if file doesn't exist return an empty string*) -fun file_info "" = "" - | file_info name = makestring (System.filedate name) handle _ => ""; - - -structure OS = - struct - structure FileSys = - struct - val chDir = PolyML.cd - - fun remove name = (*Delete a file *) - let val (is, os) = ExtendedIO.execute ("rm " ^ name) - in close_in is; close_out os end; - - (*Get pathname of current working directory *) - fun getDir () = - let val (is, os) = ExtendedIO.execute ("pwd") - val (path, _) = take_suffix (apr(op=,"\n")) (*remove newline*) - (explode (ExtendedIO.input_line is)) - in close_in is; close_out os; implode path end; - - end - end; - - - -(*** ML command execution ***) - -val use_string = - let fun exec command = - let val firstLine = ref true; - - fun getLine () = - if !firstLine - then (firstLine := false; command) - else raise Io "use_string: buffer exhausted" - in PolyML.compiler (getLine, fn s => output (std_out, s)) () end - in seq exec end; - -end; - - -(*** System command execution ***) - -(*Execute an Unix command which doesn't take any input from stdin and - sends its output to stdout.*) -fun execute command = - let val (is, os) = ExtendedIO.execute command; - val result = input (is, 999999); - in close_out os; - close_in is; - result - end; - - -(*Non-printing and 8-bit chars are forbidden in string constants*) -val needs_filtered_use = true;