--- a/Admin/CHECKLIST Sun May 31 21:59:33 2009 -0700
+++ b/Admin/CHECKLIST Sun May 31 22:00:56 2009 -0700
@@ -1,8 +1,9 @@
Checklist for official releases
===============================
-- test mosml, polyml-5.2, polyml-5.1, polyml-5.0, polyml-4.1.3, polyml-4.1.4, polyml-4.2.0,
- sparc-solaris, x86-solaris;
+- test mosml, polyml-5.2, polyml-5.1, polyml-5.0;
+
+- test sparc-solaris, x86-solaris;
- test ProofGeneral;
--- a/Admin/isatest/isatest-settings Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/isatest-settings Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
# $Id$
# Author: Gerwin Klein, NICTA
#
--- a/Admin/isatest/settings/annomaly Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/annomaly Sun May 31 22:00:56 2009 -0700
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
ML_SYSTEM=annomaly
ML_HOME="$SMLNJ_HOME/bin"
ML_OPTIONS="-m $SMLNJ_HOME/annomaly/annomaly.cm @SMLdebug=/dev/null"
--- a/Admin/isatest/settings/at-mac-poly-5.1-para Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Sun May 31 22:00:56 2009 -0700
@@ -1,7 +1,7 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2.1"
- ML_SYSTEM="polyml-5.2.1"
+ POLYML_HOME="/home/polyml/polyml-svn"
+ ML_SYSTEM="polyml-experimental"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 800 --immutable 2000"
--- a/Admin/isatest/settings/at-poly Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/at-poly Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
POLYML_HOME="/home/polyml/polyml-5.2"
ML_SYSTEM="polyml-5.2"
--- a/Admin/isatest/settings/at-poly-4.1.3 Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-# -*- shell-script -*-
-
- POLYML_HOME="/home/polyml/polyml-4.1.3"
- ML_SYSTEM="polyml-4.1.3"
- ML_PLATFORM="x86-linux"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-h 30000"
-
-ISABELLE_HOME_USER=~/isabelle-at-poly-4.1.3
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-
-HOL_USEDIR_OPTIONS="-p 2"
--- a/Admin/isatest/settings/at-poly-5.1-para-e Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/at-poly-5.1-para-e Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
POLYML_HOME="/home/polyml/polyml-5.2.1"
ML_SYSTEM="polyml-5.2.1"
--- a/Admin/isatest/settings/at-poly-dev-e Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/at-poly-dev-e Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
POLYML_HOME="/home/polyml/polyml-5.2"
ML_SYSTEM="polyml-5.2"
--- a/Admin/isatest/settings/at-poly-e Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-# -*- shell-script -*-
-
- POLYML_HOME="/home/polyml/polyml-4.2.0"
- ML_SYSTEM="polyml-4.2.0"
- ML_PLATFORM="x86-linux"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-h 30000"
-
-ISABELLE_HOME_USER=~/isabelle-at-poly-e
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-
-HOL_USEDIR_OPTIONS="-p 2"
--- a/Admin/isatest/settings/at-sml Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/at-sml Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
# Standard ML of New Jersey 110 or later
ML_SYSTEM=smlnj-110.0.7
--- a/Admin/isatest/settings/at-sml-dev-e Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/at-sml-dev-e Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
# Standard ML of New Jersey 110 or later
ML_SYSTEM=smlnj
--- a/Admin/isatest/settings/at-sml-dev-p Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/at-sml-dev-p Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
# Standard ML of New Jersey 110 or later
ML_SYSTEM=smlnj
--- a/Admin/isatest/settings/at64-poly Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/at64-poly Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
POLYML_HOME="/home/polyml/polyml-5.2"
ML_SYSTEM="polyml-5.2"
--- a/Admin/isatest/settings/at64-poly-5.1-para Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/at64-poly-5.1-para Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
POLYML_HOME="/home/polyml/polyml-5.2.1"
ML_SYSTEM="polyml-5.2.1"
--- a/Admin/isatest/settings/at64-sml-dev Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/at64-sml-dev Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
# Standard ML of New Jersey 110 or later
ML_SYSTEM=smlnj
--- a/Admin/isatest/settings/mac-poly Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/mac-poly Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
POLYML_HOME="/home/polyml/polyml-5.2"
ML_SYSTEM="polyml-5.2"
--- a/Admin/isatest/settings/mac-sml-dev Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/mac-sml-dev Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
# Standard ML of New Jersey 110 or later
ML_SYSTEM=smlnj
--- a/Admin/isatest/settings/sun-poly Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/sun-poly Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
POLYML_HOME="/home/polyml/polyml-5.1"
ML_SYSTEM="polyml-5.1"
--- a/Admin/isatest/settings/sun-sml Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/sun-sml Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
# Standard ML of New Jersey 110.0.7 (stable version)
ML_SYSTEM=smlnj-110.0.7
--- a/Admin/isatest/settings/sun-sml-dev Sun May 31 21:59:33 2009 -0700
+++ b/Admin/isatest/settings/sun-sml-dev Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
# Standard ML of New Jersey 110 or later
ML_SYSTEM=smlnj-110
--- a/NEWS Sun May 31 21:59:33 2009 -0700
+++ b/NEWS Sun May 31 22:00:56 2009 -0700
@@ -26,6 +26,22 @@
by the code generator; see Predicate.thy for an example.
+*** ML ***
+
+* Eliminated old Attrib.add_attributes, Method.add_methods and related
+cominators for "args". INCOMPATIBILITY, need to use simplified
+Attrib/Method.setup introduced in Isabelle2009.
+
+
+*** System ***
+
+* Discontinued support for Poly/ML 4.x versions.
+
+* Removed "compress" option from isabelle-process and isabelle usedir;
+this is always enabled.
+
+
+
New in Isabelle2009 (April 2009)
--------------------------------
--- a/bin/isabelle-process Sun May 31 21:59:33 2009 -0700
+++ b/bin/isabelle-process Sun May 31 22:00:56 2009 -0700
@@ -26,13 +26,11 @@
echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
echo
echo " Options are:"
- echo " -C tell ML system to copy output image"
echo " -I startup Isar interaction mode"
echo " -P startup Proof General interaction mode"
echo " -S secure mode -- disallow critical operations"
echo " -X startup PGIP interaction mode"
echo " -W OUTPUT startup process wrapper, with messages going to OUTPUT stream"
- echo " -c tell ML system to compress output image"
echo " -e MLTEXT pass MLTEXT to the ML session"
echo " -f pass 'Session.finish();' to the ML session"
echo " -m MODE add print mode for output"
@@ -60,25 +58,20 @@
# options
-COPYDB=""
ISAR=false
PROOFGENERAL=""
SECURE=""
WRAPPER_OUTPUT=""
PGIP=""
-COMPRESS=""
MLTEXT=""
MODES=""
TERMINATE=""
READONLY=""
NOWRITE=""
-while getopts "CIPSW:Xce:fm:qruw" OPT
+while getopts "IPSW:Xe:fm:qruw" OPT
do
case "$OPT" in
- C)
- COPYDB=true
- ;;
I)
ISAR=true
;;
@@ -94,9 +87,6 @@
X)
PGIP=true
;;
- c)
- COMPRESS=true
- ;;
e)
MLTEXT="$MLTEXT $OPTARG"
;;
@@ -235,8 +225,7 @@
NICE=""
fi
-export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
- ISABELLE_PID ISABELLE_TMP
+export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP
if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
$NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
--- a/doc-src/System/Thy/Basics.thy Sun May 31 21:59:33 2009 -0700
+++ b/doc-src/System/Thy/Basics.thy Sun May 31 22:00:56 2009 -0700
@@ -266,13 +266,11 @@
Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
Options are:
- -C tell ML system to copy output image
-I startup Isar interaction mode
-P startup Proof General interaction mode
-S secure mode -- disallow critical operations
-W OUTPUT startup process wrapper, with messages going to OUTPUT stream
-X startup PGIP interaction mode
- -c tell ML system to compress output image
-e MLTEXT pass MLTEXT to the ML session
-f pass 'Session.finish();' to the ML session
-m MODE add print mode for output
@@ -320,16 +318,6 @@
read-only after terminating. Thus subsequent invocations cause the
logic image to be read-only automatically.
- \medskip The @{verbatim "-c"} option tells the underlying ML system
- to compress the output heap (fully transparently). On Poly/ML for
- example, the image is garbage collected and all stored values are
- maximally shared, resulting in up to @{text "50%"} less disk space
- consumption.
-
- \medskip The @{verbatim "-C"} option tells the ML system to produce
- a completely self-contained output image, probably including a copy
- of the ML runtime system itself.
-
\medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
passed to the Isabelle session from the command line. Multiple
@{verbatim "-e"}'s are evaluated in the given order. Strange things
--- a/doc-src/System/Thy/Presentation.thy Sun May 31 21:59:33 2009 -0700
+++ b/doc-src/System/Thy/Presentation.thy Sun May 31 22:00:56 2009 -0700
@@ -446,7 +446,6 @@
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
- -c BOOL tell ML system to compress output image (default true)
-d FORMAT build document as FORMAT (default false)
-f NAME use ML file NAME (default ROOT.ML)
-g BOOL generate session graph image for document (default false)
--- a/doc-src/System/Thy/document/Basics.tex Sun May 31 21:59:33 2009 -0700
+++ b/doc-src/System/Thy/document/Basics.tex Sun May 31 22:00:56 2009 -0700
@@ -275,13 +275,11 @@
Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
Options are:
- -C tell ML system to copy output image
-I startup Isar interaction mode
-P startup Proof General interaction mode
-S secure mode -- disallow critical operations
-W OUTPUT startup process wrapper, with messages going to OUTPUT stream
-X startup PGIP interaction mode
- -c tell ML system to compress output image
-e MLTEXT pass MLTEXT to the ML session
-f pass 'Session.finish();' to the ML session
-m MODE add print mode for output
@@ -331,16 +329,6 @@
read-only after terminating. Thus subsequent invocations cause the
logic image to be read-only automatically.
- \medskip The \verb|-c| option tells the underlying ML system
- to compress the output heap (fully transparently). On Poly/ML for
- example, the image is garbage collected and all stored values are
- maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space
- consumption.
-
- \medskip The \verb|-C| option tells the ML system to produce
- a completely self-contained output image, probably including a copy
- of the ML runtime system itself.
-
\medskip Using the \verb|-e| option, arbitrary ML code may be
passed to the Isabelle session from the command line. Multiple
\verb|-e|'s are evaluated in the given order. Strange things
--- a/doc-src/System/Thy/document/Presentation.tex Sun May 31 21:59:33 2009 -0700
+++ b/doc-src/System/Thy/document/Presentation.tex Sun May 31 22:00:56 2009 -0700
@@ -472,7 +472,6 @@
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
- -c BOOL tell ML system to compress output image (default true)
-d FORMAT build document as FORMAT (default false)
-f NAME use ML file NAME (default ROOT.ML)
-g BOOL generate session graph image for document (default false)
--- a/doc-src/antiquote_setup.ML Sun May 31 21:59:33 2009 -0700
+++ b/doc-src/antiquote_setup.ML Sun May 31 22:00:56 2009 -0700
@@ -159,9 +159,9 @@
end);
fun entity_antiqs check markup kind =
- [(entity check markup kind NONE),
- (entity check markup kind (SOME true)),
- (entity check markup kind (SOME false))];
+ ((entity check markup kind NONE);
+ (entity check markup kind (SOME true));
+ (entity check markup kind (SOME false)));
in
--- a/etc/settings Sun May 31 21:59:33 2009 -0700
+++ b/etc/settings Sun May 31 22:00:56 2009 -0700
@@ -15,7 +15,7 @@
# not invent new ML system names unless you know what you are doing.
# Only one of the sections below should be activated.
-# Poly/ML 4.x/5.x (automated settings)
+# Poly/ML 5.x (automated settings)
POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
ML_HOME=$(choosefrom \
@@ -29,24 +29,18 @@
ML_OPTIONS="-H 200"
ML_DBASE=""
-# Poly/ML 5.1
+# Poly/ML 5.2.1
#ML_PLATFORM=x86-linux
#ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-5.1
+#ML_SYSTEM=polyml-5.2.1
#ML_OPTIONS="-H 500"
-# Poly/ML 5.1 (64 bit)
+# Poly/ML 5.2.1 (64 bit)
#ML_PLATFORM=x86_64-linux
#ML_HOME=/usr/local/polyml/x86_64-linux
-#ML_SYSTEM=polyml-5.1
+#ML_SYSTEM=polyml-5.2.1
#ML_OPTIONS="-H 1000"
-# Poly/ML 4.2.0
-#ML_PLATFORM=x86-linux
-#ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-4.2.0
-#ML_OPTIONS="-H 80"
-
# Standard ML of New Jersey (slow!)
#ML_SYSTEM=smlnj-110
#ML_HOME="/usr/local/smlnj/bin"
--- a/etc/user-settings.sample Sun May 31 21:59:33 2009 -0700
+++ b/etc/user-settings.sample Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
#
# Isabelle user settings sample -- for use in ~/.isabelle/etc/settings
--- a/lib/Tools/usedir Sun May 31 21:59:33 2009 -0700
+++ b/lib/Tools/usedir Sun May 31 22:00:56 2009 -0700
@@ -23,7 +23,6 @@
echo " -T LEVEL multithreading: trace level (default 0)"
echo " -V VERSION declare alternative document VERSION"
echo " -b build mode (output heap image, using current dir)"
- echo " -c BOOL tell ML system to compress output image (default true)"
echo " -d FORMAT build document as FORMAT (default false)"
echo " -f NAME use ML file NAME (default ROOT.ML)"
echo " -g BOOL generate session graph image for document (default false)"
@@ -77,7 +76,6 @@
TRACETHREADS="0"
DOCUMENT_VERSIONS=""
BUILD=""
-COMPRESS=true
DOCUMENT=false
ROOT_FILE="ROOT.ML"
DOCUMENT_GRAPH=false
@@ -91,7 +89,7 @@
function getoptions()
{
OPTIND=1
- while getopts "C:D:M:P:Q:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
+ while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:v:" OPT
do
case "$OPT" in
C)
@@ -129,10 +127,6 @@
b)
BUILD=true
;;
- c)
- check_bool "$OPTARG"
- COMPRESS="$OPTARG"
- ;;
d)
DOCUMENT="$OPTARG"
;;
@@ -175,7 +169,8 @@
done
}
-getoptions $ISABELLE_USEDIR_OPTIONS
+eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)"
+getoptions "${OPTIONS[@]}"
getoptions "$@"
shift $(($OPTIND - 1))
@@ -233,12 +228,9 @@
echo "Building $ITEM ..." >&2
LOG="$LOGDIR/$ITEM"
- OPT_C=""
- [ "$COMPRESS" = true ] && OPT_C="-c"
-
"$ISABELLE_PROCESS" \
-e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
- $OPT_C -q -w $LOGIC $NAME > "$LOG"
+ -q -w $LOGIC $NAME > "$LOG"
RC="$?"
else
ITEM=$(basename "$LOGIC")-"$SESSION"
--- a/lib/scripts/run-mosml Sun May 31 21:59:33 2009 -0700
+++ b/lib/scripts/run-mosml Sun May 31 22:00:56 2009 -0700
@@ -4,7 +4,7 @@
#
# Moscow ML 2.00 startup script
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
## diagnostics
--- a/lib/scripts/run-polyml Sun May 31 21:59:33 2009 -0700
+++ b/lib/scripts/run-polyml Sun May 31 22:00:56 2009 -0700
@@ -4,7 +4,7 @@
#
# Poly/ML 5.1/5.2 startup script.
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
## diagnostics
@@ -54,11 +54,7 @@
if [ -z "$OUTFILE" ]; then
COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
else
- if [ -z "$COMPRESS" ]; then
- COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
- else
- COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
- fi
+ COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
fi
--- a/lib/scripts/run-polyml-4.1.3 Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# Poly/ML 4.x startup script.
-
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail_out()
-{
- echo "Unable to create output heap file: \"$OUTFILE\"" >&2
- exit 2
-}
-
-function check_file()
-{
- if [ ! -f "$1" ]; then
- echo "Unable to locate $1" >&2
- echo "Please check your ML system settings!" >&2
- exit 2
- fi
-}
-
-
-## Poly/ML executable and database
-
-ML_DBASE_PREFIX=""
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-if [ -z "$ML_DBASE" ]; then
- if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then
- ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)"
- else
- ML_DBASE_HOME="$ML_HOME"
- fi
- if [ -z "$COPYDB" ]; then
- ML_DBASE_PREFIX="$ML_DBASE_HOME/"
- ML_DBASE="ML_dbase"
- else
- ML_DBASE="$ML_DBASE_HOME/ML_dbase"
- fi
- export POLYPATH="$ML_DBASE_HOME"
-else
- export POLYPATH="$(dirname "$ML_DBASE")"
-fi
-
-DISCGARB_OPTIONS="-d -c"
-
-EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- check_file "$ML_DBASE_PREFIX$ML_DBASE"
- INFILE="$ML_DBASE"
- MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
- DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
-else
- COPYDB=true
-fi
-
-if [ -z "$OUTFILE" ]; then
- DB="$INFILE"
- ML_OPTIONS="-r $ML_OPTIONS"
-elif [ "$INFILE" -ef "$OUTFILE" ]; then
- DB="$INFILE"
-elif [ -n "$COPYDB" ]; then
- [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
- cp "$INFILE" "$OUTFILE" || fail_out
- chmod +w "$OUTFILE" || fail_out
- DB="$OUTFILE"
-else
- [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
- echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
- [ -f "$OUTFILE" ] || fail_out
- DB="$OUTFILE"
-fi
-
-
-## run it!
-
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
-else
- FEEDER_OPTS="-q"
-fi
-
-DB_INFO="$(ls -l "$DB" 2>/dev/null)"
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | {
- read FPID; "$POLY" $ML_OPTIONS "$DB";
- RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-RC="$?"
-
-NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
-[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
- "$POLY" $DISCGARB_OPTIONS "$OUTFILE"
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
--- a/lib/scripts/run-polyml-4.1.4 Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# Poly/ML 4.x startup script.
-
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail_out()
-{
- echo "Unable to create output heap file: \"$OUTFILE\"" >&2
- exit 2
-}
-
-function check_file()
-{
- if [ ! -f "$1" ]; then
- echo "Unable to locate $1" >&2
- echo "Please check your ML system settings!" >&2
- exit 2
- fi
-}
-
-
-## Poly/ML executable and database
-
-ML_DBASE_PREFIX=""
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-if [ -z "$ML_DBASE" ]; then
- if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then
- ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)"
- else
- ML_DBASE_HOME="$ML_HOME"
- fi
- if [ -z "$COPYDB" ]; then
- ML_DBASE_PREFIX="$ML_DBASE_HOME/"
- ML_DBASE="ML_dbase"
- else
- ML_DBASE="$ML_DBASE_HOME/ML_dbase"
- fi
- export POLYPATH="$ML_DBASE_HOME"
-else
- export POLYPATH="$(dirname "$ML_DBASE")"
-fi
-
-DISCGARB_OPTIONS="-d -c"
-
-EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- check_file "$ML_DBASE_PREFIX$ML_DBASE"
- INFILE="$ML_DBASE"
- MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
- DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
-else
- COPYDB=true
-fi
-
-if [ -z "$OUTFILE" ]; then
- DB="$INFILE"
- ML_OPTIONS="-r $ML_OPTIONS"
-elif [ "$INFILE" -ef "$OUTFILE" ]; then
- DB="$INFILE"
-elif [ -n "$COPYDB" ]; then
- [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
- cp "$INFILE" "$OUTFILE" || fail_out
- chmod +w "$OUTFILE" || fail_out
- DB="$OUTFILE"
-else
- [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
- echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
- [ -f "$OUTFILE" ] || fail_out
- DB="$OUTFILE"
-fi
-
-
-## run it!
-
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
-else
- FEEDER_OPTS="-q"
-fi
-
-DB_INFO="$(ls -l "$DB" 2>/dev/null)"
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | {
- read FPID; "$POLY" $ML_OPTIONS "$DB";
- RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-RC="$?"
-
-NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
-[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
- "$POLY" $DISCGARB_OPTIONS "$OUTFILE"
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
--- a/lib/scripts/run-polyml-4.2.0 Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# Poly/ML 4.x startup script.
-
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail_out()
-{
- echo "Unable to create output heap file: \"$OUTFILE\"" >&2
- exit 2
-}
-
-function check_file()
-{
- if [ ! -f "$1" ]; then
- echo "Unable to locate $1" >&2
- echo "Please check your ML system settings!" >&2
- exit 2
- fi
-}
-
-
-## Poly/ML executable and database
-
-ML_DBASE_PREFIX=""
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-if [ -z "$ML_DBASE" ]; then
- if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then
- ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)"
- else
- ML_DBASE_HOME="$ML_HOME"
- fi
- if [ -z "$COPYDB" ]; then
- ML_DBASE_PREFIX="$ML_DBASE_HOME/"
- ML_DBASE="ML_dbase"
- else
- ML_DBASE="$ML_DBASE_HOME/ML_dbase"
- fi
- export POLYPATH="$ML_DBASE_HOME"
-else
- export POLYPATH="$(dirname "$ML_DBASE")"
-fi
-
-DISCGARB_OPTIONS="-d -c"
-
-EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- check_file "$ML_DBASE_PREFIX$ML_DBASE"
- INFILE="$ML_DBASE"
- MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
- DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
-else
- COPYDB=true
-fi
-
-if [ -z "$OUTFILE" ]; then
- DB="$INFILE"
- ML_OPTIONS="-r $ML_OPTIONS"
-elif [ "$INFILE" -ef "$OUTFILE" ]; then
- DB="$INFILE"
-elif [ -n "$COPYDB" ]; then
- [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
- cp "$INFILE" "$OUTFILE" || fail_out
- chmod +w "$OUTFILE" || fail_out
- DB="$OUTFILE"
-else
- [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
- echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
- [ -f "$OUTFILE" ] || fail_out
- DB="$OUTFILE"
-fi
-
-
-## run it!
-
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
-else
- FEEDER_OPTS="-q"
-fi
-
-DB_INFO="$(ls -l "$DB" 2>/dev/null)"
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | {
- read FPID; "$POLY" $ML_OPTIONS "$DB";
- RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-RC="$?"
-
-NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
-[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
- "$POLY" $DISCGARB_OPTIONS "$OUTFILE"
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
--- a/lib/scripts/run-polyml-5.0 Sun May 31 21:59:33 2009 -0700
+++ b/lib/scripts/run-polyml-5.0 Sun May 31 22:00:56 2009 -0700
@@ -4,7 +4,7 @@
#
# Poly/ML 5.0 startup script.
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
## diagnostics
@@ -54,11 +54,7 @@
if [ -z "$OUTFILE" ]; then
COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
else
- if [ -z "$COMPRESS" ]; then
- COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
- else
- COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
- fi
+ COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
rm -f "${OUTFILE}.o" || fail_out
fi
--- a/lib/scripts/run-smlnj Sun May 31 21:59:33 2009 -0700
+++ b/lib/scripts/run-smlnj Sun May 31 22:00:56 2009 -0700
@@ -4,7 +4,7 @@
#
# SML/NJ startup script (for 110 or later).
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
## diagnostics
--- a/lib/scripts/timestart.bash Sun May 31 21:59:33 2009 -0700
+++ b/lib/scripts/timestart.bash Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
#
# Author: Makarius
#
--- a/lib/scripts/timestop.bash Sun May 31 21:59:33 2009 -0700
+++ b/lib/scripts/timestop.bash Sun May 31 22:00:56 2009 -0700
@@ -1,4 +1,4 @@
-# -*- shell-script -*-
+# -*- shell-script -*- :mode=shellscript:
#
# Author: Makarius
#
--- a/src/FOL/IFOL.thy Sun May 31 21:59:33 2009 -0700
+++ b/src/FOL/IFOL.thy Sun May 31 22:00:56 2009 -0700
@@ -610,7 +610,7 @@
subsection {* Intuitionistic Reasoning *}
-setup {* Intuitionistic.method_setup "iprover" *}
+setup {* Intuitionistic.method_setup @{binding iprover} *}
lemma impE':
assumes 1: "P --> Q"
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sun May 31 22:00:56 2009 -0700
@@ -2,6 +2,13 @@
Author: Amine Chaieb, TU Muenchen
*)
+signature FERRACK_TAC =
+sig
+ val trace: bool ref
+ val linr_tac: Proof.context -> bool -> int -> tactic
+ val setup: theory -> theory
+end
+
structure Ferrack_Tac =
struct
@@ -98,12 +105,10 @@
THEN tac) st
end handle Subscript => no_tac st);
-fun linr_meth src =
- Method.syntax (Args.mode "no_quantify") src
- #> (fn (q, ctxt) => SIMPLE_METHOD' (linr_tac ctxt (not q)));
-
val setup =
- Method.add_method ("rferrack", linr_meth,
- "decision procedure for linear real arithmetic");
+ Method.setup @{binding rferrack}
+ (Args.mode "no_quantify" >> (fn q => fn ctxt =>
+ SIMPLE_METHOD' (linr_tac ctxt (not q))))
+ "decision procedure for linear real arithmetic";
end
--- a/src/HOL/HOL.thy Sun May 31 21:59:33 2009 -0700
+++ b/src/HOL/HOL.thy Sun May 31 22:00:56 2009 -0700
@@ -31,7 +31,7 @@
("Tools/recfun_codegen.ML")
begin
-setup {* Intuitionistic.method_setup "iprover" *}
+setup {* Intuitionistic.method_setup @{binding iprover} *}
subsection {* Primitive logic *}
--- a/src/HOL/Library/Efficient_Nat.thy Sun May 31 21:59:33 2009 -0700
+++ b/src/HOL/Library/Efficient_Nat.thy Sun May 31 22:00:56 2009 -0700
@@ -317,7 +317,7 @@
setup {*
fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
- true false) ["SML", "OCaml", "Haskell"]
+ false true) ["SML", "OCaml", "Haskell"]
*}
text {*
--- a/src/HOL/Relation_Power.thy Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,154 +0,0 @@
-(* Title: HOL/Relation_Power.thy
- Author: Tobias Nipkow
- Copyright 1996 TU Muenchen
-*)
-
-header{*Powers of Relations and Functions*}
-
-theory Relation_Power
-imports Power Transitive_Closure Plain
-begin
-
-consts funpower :: "('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "^^" 80)
-
-overloading
- relpow \<equiv> "funpower \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set"
-begin
-
-text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *}
-
-primrec relpow where
- "(R \<Colon> ('a \<times> 'a) set) ^^ 0 = Id"
- | "(R \<Colon> ('a \<times> 'a) set) ^^ Suc n = R O (R ^^ n)"
-
-end
-
-overloading
- funpow \<equiv> "funpower \<Colon> ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
-begin
-
-text {* @{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f} *}
-
-primrec funpow where
- "(f \<Colon> 'a \<Rightarrow> 'a) ^^ 0 = id"
- | "(f \<Colon> 'a \<Rightarrow> 'a) ^^ Suc n = f o (f ^^ n)"
-
-end
-
-primrec fun_pow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
- "fun_pow 0 f = id"
- | "fun_pow (Suc n) f = f o fun_pow n f"
-
-lemma funpow_fun_pow [code unfold]:
- "f ^^ n = fun_pow n f"
- unfolding funpow_def fun_pow_def ..
-
-lemma funpow_add:
- "f ^^ (m + n) = f ^^ m o f ^^ n"
- by (induct m) simp_all
-
-lemma funpow_swap1:
- "f ((f ^^ n) x) = (f ^^ n) (f x)"
-proof -
- have "f ((f ^^ n) x) = (f ^^ (n+1)) x" unfolding One_nat_def by simp
- also have "\<dots> = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add)
- also have "\<dots> = (f ^^ n) (f x)" unfolding One_nat_def by simp
- finally show ?thesis .
-qed
-
-lemma rel_pow_1 [simp]:
- fixes R :: "('a * 'a) set"
- shows "R ^^ 1 = R"
- by simp
-
-lemma rel_pow_0_I:
- "(x, x) \<in> R ^^ 0"
- by simp
-
-lemma rel_pow_Suc_I:
- "(x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
- by auto
-
-lemma rel_pow_Suc_I2:
- "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
- by (induct n arbitrary: z) (simp, fastsimp)
-
-lemma rel_pow_0_E:
- "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
- by simp
-
-lemma rel_pow_Suc_E:
- "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P"
- by auto
-
-lemma rel_pow_E:
- "(x, z) \<in> R ^^ n \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
- \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P)
- \<Longrightarrow> P"
- by (cases n) auto
-
-lemma rel_pow_Suc_D2:
- "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)"
- apply (induct n arbitrary: x z)
- apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
- apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
- done
-
-lemma rel_pow_Suc_D2':
- "\<forall>x y z. (x, y) \<in> R ^^ n \<and> (y, z) \<in> R \<longrightarrow> (\<exists>w. (x, w) \<in> R \<and> (w, z) \<in> R ^^ n)"
- by (induct n) (simp_all, blast)
-
-lemma rel_pow_E2:
- "(x, z) \<in> R ^^ n \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
- \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)
- \<Longrightarrow> P"
- apply (cases n, simp)
- apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
- done
-
-lemma rtrancl_imp_UN_rel_pow:
- "p \<in> R^* \<Longrightarrow> p \<in> (\<Union>n. R ^^ n)"
- apply (cases p) apply (simp only:)
- apply (erule rtrancl_induct)
- apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
- done
-
-lemma rel_pow_imp_rtrancl:
- "p \<in> R ^^ n \<Longrightarrow> p \<in> R^*"
- apply (induct n arbitrary: p)
- apply (simp_all only: split_tupled_all)
- apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
- apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
- done
-
-lemma rtrancl_is_UN_rel_pow:
- "R^* = (UN n. R ^^ n)"
- by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
-
-lemma trancl_power:
- "x \<in> r^+ = (\<exists>n > 0. x \<in> r ^^ n)"
- apply (cases x)
- apply simp
- apply (rule iffI)
- apply (drule tranclD2)
- apply (clarsimp simp: rtrancl_is_UN_rel_pow)
- apply (rule_tac x="Suc x" in exI)
- apply (clarsimp simp: rel_comp_def)
- apply fastsimp
- apply clarsimp
- apply (case_tac n, simp)
- apply clarsimp
- apply (drule rel_pow_imp_rtrancl)
- apply fastsimp
- done
-
-lemma single_valued_rel_pow:
- fixes R :: "('a * 'a) set"
- shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)"
- apply (induct n arbitrary: R)
- apply simp_all
- apply (rule single_valuedI)
- apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
- done
-
-end
--- a/src/HOL/Tools/primrec_package.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/HOL/Tools/primrec_package.ML Sun May 31 22:00:56 2009 -0700
@@ -268,7 +268,7 @@
val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
fun attr_bindings prefix = map (fn ((b, attrs), _) =>
(Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
- fun simp_attr_binding prefix = (Binding.qualify false prefix (Binding.name "simps"),
+ fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"),
map (Attrib.internal o K)
[Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]);
in
--- a/src/HOL/ex/predicate_compile.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/HOL/ex/predicate_compile.ML Sun May 31 22:00:56 2009 -0700
@@ -31,6 +31,8 @@
(* debug stuff *)
+fun makestring _ = "?"; (* FIXME dummy *)
+
fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single);
--- a/src/Pure/IsaMakefile Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/IsaMakefile Sun May 31 22:00:56 2009 -0700
@@ -19,16 +19,15 @@
## Pure
-BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML \
+BOOTSTRAP_FILES = ML-Systems/compiler_polyml-5.0.ML \
+ ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML \
+ ML-Systems/exn.ML ML-Systems/ml_name_space.ML \
ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \
ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
- ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML \
- ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML \
- ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
- ML-Systems/polyml-experimental.ML ML-Systems/polyml.ML \
- ML-Systems/polyml_common.ML ML-Systems/polyml_old_compiler4.ML \
- ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML \
- ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
+ ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \
+ ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \
+ ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
+ ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
ML-Systems/time_limit.ML ML-Systems/universal.ML
--- a/src/Pure/Isar/attrib.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/Isar/attrib.ML Sun May 31 22:00:56 2009 -0700
@@ -26,14 +26,10 @@
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
val crude_closure: Proof.context -> src -> src
- val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
- val syntax: attribute context_parser -> src -> attribute
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
theory -> theory
- val no_args: attribute -> src -> attribute
val add_del: attribute -> attribute -> attribute context_parser
- val add_del_args: attribute -> attribute -> src -> attribute
val thm_sel: Facts.interval list parser
val thm: thm context_parser
val thms: thm list context_parser
@@ -89,6 +85,10 @@
|> Pretty.chunks |> Pretty.writeln
end;
+fun add_attribute name att comment thy = thy |> Attributes.map (fn atts =>
+ #2 (NameSpace.define (Sign.naming_of thy) (name, ((att, comment), stamp ())) atts)
+ handle Symtab.DUP dup => error ("Duplicate declaration of attribute " ^ quote dup));
+
(* name space *)
@@ -149,24 +149,13 @@
Args.closure src);
-(* add_attributes *)
-
-fun add_attributes raw_attrs thy =
- let
- val new_attrs =
- raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
- fun add attrs = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_attrs attrs
- handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
- in Attributes.map add thy end;
-
-
(* attribute setup *)
-fun syntax scan src (context, th) =
- let val (f: attribute, context') = Args.syntax "attribute" scan src context
- in f (context', th) end;
+fun syntax scan = Args.syntax "attribute" scan;
-fun setup name scan comment = add_attributes [(Binding.name_of name, syntax scan, comment)];
+fun setup name scan =
+ add_attribute name
+ (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end);
fun attribute_setup name (txt, pos) cmt =
Context.theory_map (ML_Context.expression pos
@@ -175,12 +164,9 @@
("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
-(* basic syntax *)
+(* add/del syntax *)
-fun no_args x = syntax (Scan.succeed x);
-
-fun add_del add del = (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
-fun add_del_args add del = syntax (add_del add del);
+fun add_del add del = Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add);
@@ -237,113 +223,99 @@
fun internal att = Args.src (("Pure.attribute", [T.mk_attribute att]), Position.none);
-val internal_att =
- syntax (Scan.lift Args.internal_attribute >> Morphism.form);
-
-
-(* tags *)
-
-val tagged = syntax (Scan.lift (Args.name -- Args.name) >> Thm.tag);
-val untagged = syntax (Scan.lift Args.name >> Thm.untag);
-
-val kind = syntax (Scan.lift Args.name >> Thm.kind);
-
(* rule composition *)
val COMP_att =
- syntax (Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
- >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B))));
+ Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
+ >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)));
val THEN_att =
- syntax (Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
- >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B))));
+ Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
+ >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
val OF_att =
- syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
+ thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A));
(* rename_abs *)
-val rename_abs = syntax
- (Scan.lift (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')));
+val rename_abs = Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars');
(* unfold / fold definitions *)
fun unfolded_syntax rule =
- syntax (thms >>
- (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths)));
+ thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
val unfolded = unfolded_syntax LocalDefs.unfold;
val folded = unfolded_syntax LocalDefs.fold;
-(* rule cases *)
-
-val consumes = syntax (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes);
-val case_names = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names);
-val case_conclusion =
- syntax (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion);
-val params = syntax (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params);
-
-
(* rule format *)
-val rule_format = syntax (Args.mode "no_asm"
- >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format));
+val rule_format = Args.mode "no_asm"
+ >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format);
-val elim_format = no_args (Thm.rule_attribute (K Tactic.make_elim));
+val elim_format = Thm.rule_attribute (K Tactic.make_elim);
(* misc rules *)
-val standard = no_args (Thm.rule_attribute (K Drule.standard));
-
-val no_vars = no_args (Thm.rule_attribute (fn context => fn th =>
+val no_vars = Thm.rule_attribute (fn context => fn th =>
let
val ctxt = Variable.set_body false (Context.proof_of context);
val ((_, [th']), _) = Variable.import_thms true [th] ctxt;
- in th' end));
+ in th' end);
val eta_long =
- no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion)));
+ Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion));
-val rotated = syntax
- (Scan.lift (Scan.optional P.int 1) >> (fn n => Thm.rule_attribute (K (rotate_prems n))));
-
-val abs_def = no_args (Thm.rule_attribute (K Drule.abs_def));
+val rotated = Scan.optional P.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
(* theory setup *)
val _ = Context.>> (Context.map_theory
- (add_attributes
- [("attribute", internal_att, "internal attribute"),
- ("tagged", tagged, "tagged theorem"),
- ("untagged", untagged, "untagged theorem"),
- ("kind", kind, "theorem kind"),
- ("COMP", COMP_att, "direct composition with rules (no lifting)"),
- ("THEN", THEN_att, "resolution with rule"),
- ("OF", OF_att, "rule applied to facts"),
- ("rename_abs", rename_abs, "rename bound variables in abstractions"),
- ("unfolded", unfolded, "unfolded definitions"),
- ("folded", folded, "folded definitions"),
- ("standard", standard, "result put into standard form"),
- ("elim_format", elim_format, "destruct rule turned into elimination rule format"),
- ("no_vars", no_vars, "frozen schematic vars"),
- ("eta_long", eta_long, "put theorem into eta long beta normal form"),
- ("consumes", consumes, "number of consumed facts"),
- ("case_names", case_names, "named rule cases"),
- ("case_conclusion", case_conclusion, "named conclusion of rule cases"),
- ("params", params, "named rule parameters"),
- ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"),
- ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"),
- ("rule_format", rule_format, "result put into standard rule format"),
- ("rotated", rotated, "rotated theorem premises"),
- ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
- "declaration of definitional transformations"),
- ("abs_def", abs_def, "abstract over free variables of a definition")]));
+ (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
+ "internal attribute" #>
+ setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
+ setup (Binding.name "untagged") (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
+ setup (Binding.name "kind") (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
+ setup (Binding.name "COMP") COMP_att "direct composition with rules (no lifting)" #>
+ setup (Binding.name "THEN") THEN_att "resolution with rule" #>
+ setup (Binding.name "OF") OF_att "rule applied to facts" #>
+ setup (Binding.name "rename_abs") (Scan.lift rename_abs)
+ "rename bound variables in abstractions" #>
+ setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
+ setup (Binding.name "folded") folded "folded definitions" #>
+ setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes)
+ "number of consumed facts" #>
+ setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names)
+ "named rule cases" #>
+ setup (Binding.name "case_conclusion")
+ (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion)
+ "named conclusion of rule cases" #>
+ setup (Binding.name "params")
+ (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params)
+ "named rule parameters" #>
+ setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
+ "result put into standard form (legacy)" #>
+ setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
+ setup (Binding.name "elim_format") (Scan.succeed elim_format)
+ "destruct rule turned into elimination rule format" #>
+ setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
+ setup (Binding.name "eta_long") (Scan.succeed eta_long)
+ "put theorem into eta long beta normal form" #>
+ setup (Binding.name "atomize") (Scan.succeed ObjectLogic.declare_atomize)
+ "declaration of atomize rule" #>
+ setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
+ "declaration of rulify rule" #>
+ setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
+ setup (Binding.name "defn") (add_del LocalDefs.defn_add LocalDefs.defn_del)
+ "declaration of definitional transformations" #>
+ setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
+ "abstract over free variables of a definition"));
@@ -397,8 +369,8 @@
val name = Sign.full_bname thy bname;
in
thy
- |> add_attributes [(bname, syntax (Scan.lift (scan_config thy config) >> Morphism.form),
- "configuration option")]
+ |> setup (Binding.name bname) (Scan.lift (scan_config thy config) >> Morphism.form)
+ "configuration option"
|> Configs.map (Symtab.update (name, config))
end;
--- a/src/Pure/Isar/method.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/Isar/method.ML Sun May 31 22:00:56 2009 -0700
@@ -75,30 +75,13 @@
val defined: theory -> string -> bool
val method: theory -> src -> Proof.context -> method
val method_i: theory -> src -> Proof.context -> method
- val add_methods: (bstring * (src -> Proof.context -> method) * string) list
- -> theory -> theory
- val add_method: bstring * (src -> Proof.context -> method) * string
- -> theory -> theory
val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
theory -> theory
- val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
- val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
type modifier = (Proof.context -> Proof.context) * attribute
val section: modifier parser list -> thm list context_parser
val sections: modifier parser list -> thm list list context_parser
- val sectioned_args: 'a context_parser -> modifier parser list ->
- ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b
- val bang_sectioned_args: modifier parser list ->
- (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
- val bang_sectioned_args': modifier parser list -> 'a context_parser ->
- ('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b
- val only_sectioned_args: modifier parser list -> (Proof.context -> 'a) -> src ->
- Proof.context -> 'a
- val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
- val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a
- val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a
val parse: text parser
end;
@@ -356,6 +339,10 @@
|> Pretty.chunks |> Pretty.writeln
end;
+fun add_method name meth comment thy = thy |> Methods.map (fn meths =>
+ #2 (NameSpace.define (Sign.naming_of thy) (name, ((meth, comment), stamp ())) meths)
+ handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup));
+
(* get methods *)
@@ -376,27 +363,13 @@
fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy)));
-(* add method *)
-
-fun add_methods raw_meths thy =
- let
- val new_meths = raw_meths |> map (fn (name, f, comment) =>
- (Binding.name name, ((f, comment), stamp ())));
-
- fun add meths = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_meths meths
- handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
- in Methods.map add thy end;
-
-val add_method = add_methods o Library.single;
-
-
(* method setup *)
fun syntax scan = Args.context_syntax "method" scan;
-fun setup name scan comment =
- add_methods [(Binding.name_of name,
- fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end, comment)];
+fun setup name scan =
+ add_method name
+ (fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end);
fun method_setup name (txt, pos) cmt =
Context.theory_map (ML_Context.expression pos
@@ -411,15 +384,6 @@
structure P = OuterParse;
-(* basic *)
-
-fun simple_args scan f src ctxt : method =
- fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
-
-fun ctxt_args (f: Proof.context -> method) src ctxt =
- fst (syntax (Scan.succeed (f ctxt)) src ctxt);
-
-
(* sections *)
type modifier = (Proof.context -> Proof.context) * attribute;
@@ -436,19 +400,6 @@
fun sections ss = Scan.repeat (section ss);
-fun sectioned_args args ss f src ctxt =
- let val ((x, _), ctxt') = syntax (args -- sections ss) src ctxt
- in f x ctxt' end;
-
-fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
-fun bang_sectioned_args' ss scan f =
- sectioned_args (Args.bang_facts -- scan >> swap) ss (uncurry f);
-fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f);
-
-fun thms_ctxt_args f = sectioned_args (thms []) [] f;
-fun thms_args f = thms_ctxt_args (K o f);
-fun thm_args f = thms_args (fn [thm] => f thm | _ => error "Single theorem expected");
-
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Sun May 31 22:00:56 2009 -0700
@@ -0,0 +1,32 @@
+(* Title: Pure/ML-Systems/compiler_polyml-5.0.ML
+
+Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1.
+*)
+
+fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
+ let
+ val in_buffer = ref (explode (tune_source txt));
+ val out_buffer = ref ([]: string list);
+ fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
+
+ val current_line = ref line;
+ fun get () =
+ (case ! in_buffer of
+ [] => ""
+ | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
+ fun put s = out_buffer := s :: ! out_buffer;
+
+ fun exec () =
+ (case ! in_buffer of
+ [] => ()
+ | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
+ in
+ exec () handle exn => (error (output ()); raise exn);
+ if verbose then print (output ()) else ()
+ end;
+
+fun use_file context verbose name =
+ let
+ val instream = TextIO.openIn name;
+ val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+ in use_text context (1, name) verbose txt end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Sun May 31 22:00:56 2009 -0700
@@ -0,0 +1,51 @@
+(* Title: Pure/ML-Systems/compiler_polyml-5.2.ML
+
+Runtime compilation for Poly/ML 5.2 and 5.2.1.
+*)
+
+local
+
+fun drop_newline s =
+ if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
+ else s;
+
+in
+
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+ (start_line, name) verbose txt =
+ let
+ val current_line = ref start_line;
+ val in_buffer = ref (String.explode (tune_source txt));
+ val out_buffer = ref ([]: string list);
+ fun output () = drop_newline (implode (rev (! out_buffer)));
+
+ fun get () =
+ (case ! in_buffer of
+ [] => NONE
+ | c :: cs =>
+ (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
+ fun put s = out_buffer := s :: ! out_buffer;
+ fun message (msg, is_err, line) =
+ (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream put,
+ PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPErrorMessageProc (put o message),
+ PolyML.Compiler.CPNameSpace name_space];
+ val _ =
+ (while not (List.null (! in_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ error (output ()); raise exn);
+ in if verbose then print (output ()) else () end;
+
+fun use_file context verbose name =
+ let
+ val instream = TextIO.openIn name;
+ val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+ in use_text context (1, name) verbose txt end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Sun May 31 22:00:56 2009 -0700
@@ -0,0 +1,55 @@
+(* Title: Pure/ML-Systems/compiler_polyml-5.3.ML
+
+Runtime compilation for Poly/ML 5.3 (SVN experimental).
+*)
+
+local
+
+fun drop_newline s =
+ if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
+ else s;
+
+in
+
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+ (start_line, name) verbose txt =
+ let
+ val current_line = ref start_line;
+ val in_buffer = ref (String.explode (tune_source txt));
+ val out_buffer = ref ([]: string list);
+ fun output () = drop_newline (implode (rev (! out_buffer)));
+
+ fun get () =
+ (case ! in_buffer of
+ [] => NONE
+ | c :: cs =>
+ (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
+ fun put s = out_buffer := s :: ! out_buffer;
+ fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
+ (put (if hard then "Error: " else "Warning: ");
+ PolyML.prettyPrint (put, 76) msg1;
+ (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
+ put ("At" ^ str_of_pos line name ^ "\n"));
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream put,
+ PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPErrorMessageProc put_message,
+ PolyML.Compiler.CPNameSpace name_space,
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false];
+ val _ =
+ (while not (List.null (! in_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ error (output ()); raise exn);
+ in if verbose then print (output ()) else () end;
+
+fun use_file context verbose name =
+ let
+ val instream = TextIO.openIn name;
+ val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+ in use_text context (1, name) verbose txt end;
+
+end;
+
--- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML-Systems/install_pp_polyml-experimental.ML Sun May 31 22:00:56 2009 -0700
@@ -1,18 +1,17 @@
(* Title: Pure/ML-Systems/install_pp_polyml-experimental.ML
-Extra toplevel pretty-printing for Poly/ML; experimental version for
-Poly/ML 5.3.
+Extra toplevel pretty-printing for Poly/ML 5.3 (SVN experimental).
*)
-addPrettyPrinter (fn depth => fn pretty => fn x =>
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
(case Future.peek x of
- NONE => PrettyString "<future>"
- | SOME (Exn.Exn _) => PrettyString "<failed>"
+ NONE => PolyML.PrettyString "<future>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
| SOME (Exn.Result y) => pretty (y, depth)));
-addPrettyPrinter (fn depth => fn pretty => fn x =>
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
(case Lazy.peek x of
- NONE => PrettyString "<lazy>"
- | SOME (Exn.Exn _) => PrettyString "<failed>"
+ NONE => PolyML.PrettyString "<lazy>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
| SOME (Exn.Result y) => pretty (y, depth)));
--- a/src/Pure/ML-Systems/install_pp_polyml.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML Sun May 31 22:00:56 2009 -0700
@@ -3,15 +3,17 @@
Extra toplevel pretty-printing for Poly/ML.
*)
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
- (case Future.peek x of
- NONE => str "<future>"
- | SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Result y) => print (y, depth)));
+PolyML.install_pp
+ (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
+ (case Future.peek x of
+ NONE => str "<future>"
+ | SOME (Exn.Exn _) => str "<failed>"
+ | SOME (Exn.Result y) => print (y, depth)));
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
- (case Lazy.peek x of
- NONE => str "<lazy>"
- | SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Result y) => print (y, depth)));
+PolyML.install_pp
+ (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
+ (case Lazy.peek x of
+ NONE => str "<lazy>"
+ | SOME (Exn.Exn _) => str "<failed>"
+ | SOME (Exn.Result y) => print (y, depth)));
--- a/src/Pure/ML-Systems/mosml.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML-Systems/mosml.ML Sun May 31 22:00:56 2009 -0700
@@ -132,8 +132,6 @@
(*dummy implementation*)
fun exception_trace f = f ();
-(*dummy implementation*)
-fun print x = x;
(** Compiler-independent timing functions **)
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sun May 31 22:00:56 2009 -0700
@@ -1,7 +1,7 @@
(* Title: Pure/ML-Systems/multithreading_polyml.ML
Author: Makarius
-Multithreading in Poly/ML 5.2 or later (cf. polyml/basis/Thread.sml).
+Multithreading in Poly/ML 5.2.1 or later (cf. polyml/basis/Thread.sml).
*)
signature MULTITHREADING_POLYML =
--- a/src/Pure/ML-Systems/polyml-4.1.3.ML Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-4.1.3.ML
-
-Compatibility wrapper for Poly/ML 4.1.3.
-*)
-
-use "ML-Systems/polyml_old_basis.ML";
-use "ML-Systems/universal.ML";
-use "ML-Systems/thread_dummy.ML";
-use "ML-Systems/ml_name_space.ML";
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/polyml_old_compiler4.ML";
-use "ML-Systems/polyml_pp.ML";
-
-val pointer_eq = Address.wordEq;
-
--- a/src/Pure/ML-Systems/polyml-4.1.4.ML Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-4.1.4.ML
-
-Compatibility wrapper for Poly/ML 4.1.4.
-*)
-
-use "ML-Systems/polyml_old_basis.ML";
-use "ML-Systems/universal.ML";
-use "ML-Systems/thread_dummy.ML";
-use "ML-Systems/ml_name_space.ML";
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/polyml_old_compiler4.ML";
-use "ML-Systems/polyml_pp.ML";
-
-val pointer_eq = Address.wordEq;
-
--- a/src/Pure/ML-Systems/polyml-4.2.0.ML Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-4.2.0.ML
-
-Compatibility wrapper for Poly/ML 4.2.0.
-*)
-
-use "ML-Systems/universal.ML";
-use "ML-Systems/thread_dummy.ML";
-use "ML-Systems/ml_name_space.ML";
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/polyml_old_compiler4.ML";
-use "ML-Systems/polyml_pp.ML";
-
-val pointer_eq = Address.wordEq;
-
--- a/src/Pure/ML-Systems/polyml-5.0.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-5.0.ML Sun May 31 22:00:56 2009 -0700
@@ -7,8 +7,8 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/polyml_common.ML";
-use "ML-Systems/polyml_old_compiler5.ML";
-use "ML-Systems/polyml_pp.ML";
+use "ML-Systems/compiler_polyml-5.0.ML";
+use "ML-Systems/pp_polyml.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/ML-Systems/polyml-5.1.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-5.1.ML Sun May 31 22:00:56 2009 -0700
@@ -6,8 +6,8 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/polyml_common.ML";
-use "ML-Systems/polyml_old_compiler5.ML";
-use "ML-Systems/polyml_pp.ML";
+use "ML-Systems/compiler_polyml-5.0.ML";
+use "ML-Systems/pp_polyml.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/ML-Systems/polyml-experimental.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-experimental.ML Sun May 31 22:00:56 2009 -0700
@@ -1,6 +1,6 @@
-(* Title: Pure/ML-Systems/polyml.ML
+(* Title: Pure/ML-Systems/polyml-experimental.ML
-Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
+Compatibility wrapper for Poly/ML 5.3 (SVN experimental).
*)
open Thread;
@@ -19,92 +19,42 @@
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
-(* runtime compilation *)
-
-local
-
-fun drop_newline s =
- if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
- else s;
-
-in
-
-fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
- (start_line, name) verbose txt =
- let
- val current_line = ref start_line;
- val in_buffer = ref (String.explode (tune_source txt));
- val out_buffer = ref ([]: string list);
- fun output () = drop_newline (implode (rev (! out_buffer)));
-
- fun get () =
- (case ! in_buffer of
- [] => NONE
- | c :: cs =>
- (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
- fun put s = out_buffer := s :: ! out_buffer;
- fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
- (put (if hard then "Error: " else "Warning: ");
- PolyML.prettyPrint (put, 76) msg1;
- (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
- put ("At" ^ str_of_pos line name ^ "\n"));
-
- val parameters =
- [PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPLineNo (fn () => ! current_line),
- PolyML.Compiler.CPErrorMessageProc put_message,
- PolyML.Compiler.CPNameSpace name_space,
- PolyML.Compiler.CPPrintInAlphabeticalOrder false];
- val _ =
- (while not (List.null (! in_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); raise exn);
- in if verbose then print (output ()) else () end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
-
-end;
+use "ML-Systems/compiler_polyml-5.3.ML";
(* toplevel pretty printing *)
val pretty_ml =
let
- fun convert len (PrettyBlock (ind, _, context, prts)) =
+ fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
let
fun property name default =
- (case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of
- SOME (ContextProperty (_, b)) => b
+ (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
+ SOME (PolyML.ContextProperty (_, b)) => b
| NONE => default);
val bg = property "begin" "";
val en = property "end" "";
val len' = property "length" len;
in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
- | convert len (PrettyString s) =
+ | convert len (PolyML.PrettyString s) =
ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
- | convert _ (PrettyBreak (wd, _)) =
+ | convert _ (PolyML.PrettyBreak (wd, _)) =
ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
in convert "" end;
fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
let val context =
- (if bg = "" then [] else [ContextProperty ("begin", bg)]) @
- (if en = "" then [] else [ContextProperty ("end", en)])
- in PrettyBlock (ind, false, context, map ml_pretty prts) end
+ (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
+ (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
+ in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
| ml_pretty (ML_Pretty.String (s, len)) =
- if len = size s then PrettyString s
- else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s])
- | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
- | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
+ if len = size s then PolyML.PrettyString s
+ else PolyML.PrettyBlock
+ (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s])
+ | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
+ | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0);
fun toplevel_pp context (_: string list) pp =
use_text context (1, "pp") false
- ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+ ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
--- a/src/Pure/ML-Systems/polyml.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML-Systems/polyml.ML Sun May 31 22:00:56 2009 -0700
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/polyml.ML
-Compatibility wrapper for Poly/ML 5.2 or later.
+Compatibility wrapper for Poly/ML 5.2 and 5.2.1.
*)
open Thread;
@@ -22,54 +22,6 @@
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
-(* runtime compilation *)
-
-local
-
-fun drop_newline s =
- if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
- else s;
-
-in
-
-fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
- (start_line, name) verbose txt =
- let
- val current_line = ref start_line;
- val in_buffer = ref (String.explode (tune_source txt));
- val out_buffer = ref ([]: string list);
- fun output () = drop_newline (implode (rev (! out_buffer)));
+use "ML-Systems/compiler_polyml-5.2.ML";
+use "ML-Systems/pp_polyml.ML";
- fun get () =
- (case ! in_buffer of
- [] => NONE
- | c :: cs =>
- (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
- fun put s = out_buffer := s :: ! out_buffer;
- fun message (msg, is_err, line) =
- (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
-
- val parameters =
- [PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPLineNo (fn () => ! current_line),
- PolyML.Compiler.CPErrorMessageProc (put o message),
- PolyML.Compiler.CPNameSpace name_space];
- val _ =
- (while not (List.null (! in_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); raise exn);
- in if verbose then print (output ()) else () end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
-
-end;
-
-use "ML-Systems/polyml_pp.ML";
-
--- a/src/Pure/ML-Systems/polyml_common.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML-Systems/polyml_common.ML Sun May 31 22:00:56 2009 -0700
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/polyml_common.ML
-Compatibility file for Poly/ML -- common part for 4.x and 5.x.
+Compatibility file for Poly/ML -- common part for 5.x.
*)
exception Interrupt = SML90.Interrupt;
@@ -28,13 +28,7 @@
(* old Poly/ML emulation *)
-local
- val orig_exit = exit;
-in
- open PolyML;
- val exit = orig_exit;
- fun quit () = exit 0;
-end;
+fun quit () = exit 0;
(* restore old-style character / string functions *)
@@ -83,6 +77,8 @@
fun print_depth n = (depth := n; PolyML.print_depth n);
end;
+val error_depth = PolyML.error_depth;
+
(** interrupts **)
@@ -134,7 +130,12 @@
| SOME txt => txt);
-(* profile execution *)
+
+(** Runtime system **)
+
+val exception_trace = PolyML.exception_trace;
+val timing = PolyML.timing;
+val profiling = PolyML.profiling;
fun profile 0 f x = f x
| profile n f x =
--- a/src/Pure/ML-Systems/polyml_old_basis.ML Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Title: Pure/ML-Systems/polyml_old_basis.ML
-
-Fixes for the old SML basis library (before Poly/ML 4.2.0).
-*)
-
-structure String =
-struct
- fun isSuffix s1 s2 =
- let val n1 = size s1 and n2 = size s2
- in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
- fun isSubstring s1 s2 =
- String.isPrefix s1 s2 orelse
- size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE));
- open String;
-end;
-
-structure Substring =
-struct
- open Substring;
- val full = all;
-end;
-
-structure TextIO =
-struct
- open TextIO;
- fun inputLine is =
- let val s = TextIO.inputLine is
- in if s = "" then NONE else SOME s end;
-end;
--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: Pure/ML-Systems/polyml_old_compiler4.ML
-
-Runtime compilation -- for old PolyML.compiler (version 4.x).
-*)
-
-fun use_text ({tune_source, print, error, ...}: use_context) (line: int, name) verbose txt =
- let
- val in_buffer = ref (explode (tune_source txt));
- val out_buffer = ref ([]: string list);
- fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
-
- fun get () =
- (case ! in_buffer of
- [] => ""
- | c :: cs => (in_buffer := cs; c));
- fun put s = out_buffer := s :: ! out_buffer;
-
- fun exec () =
- (case ! in_buffer of
- [] => ()
- | _ => (PolyML.compiler (get, put) (); exec ()));
- in
- exec () handle exn =>
- (error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
- if verbose then print (output ()) else ()
- end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: Pure/ML-Systems/polyml_old_compiler5.ML
-
-Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
-*)
-
-fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
- let
- val in_buffer = ref (explode (tune_source txt));
- val out_buffer = ref ([]: string list);
- fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
-
- val current_line = ref line;
- fun get () =
- (case ! in_buffer of
- [] => ""
- | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
- fun put s = out_buffer := s :: ! out_buffer;
-
- fun exec () =
- (case ! in_buffer of
- [] => ()
- | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
- in
- exec () handle exn => (error (output ()); raise exn);
- if verbose then print (output ()) else ()
- end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
--- a/src/Pure/ML-Systems/polyml_pp.ML Sun May 31 21:59:33 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: Pure/ML-Systems/polyml_pp.ML
-
-Toplevel pretty printing for Poly/ML before 5.3.
-*)
-
-fun ml_pprint (print, begin_blk, brk, end_blk) =
- let
- fun str "" = ()
- | str s = print s;
- fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
- (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
- | pprint (ML_Pretty.String (s, _)) = str s
- | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
- | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
- in pprint end;
-
-fun toplevel_pp context (_: string list) pp =
- use_text context (1, "pp") false
- ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/pp_polyml.ML Sun May 31 22:00:56 2009 -0700
@@ -0,0 +1,20 @@
+(* Title: Pure/ML-Systems/pp_polyml.ML
+
+Toplevel pretty printing for Poly/ML before 5.3.
+*)
+
+fun ml_pprint (print, begin_blk, brk, end_blk) =
+ let
+ fun str "" = ()
+ | str s = print s;
+ fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
+ (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
+ | pprint (ML_Pretty.String (s, _)) = str s
+ | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
+ | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
+ in pprint end;
+
+fun toplevel_pp context (_: string list) pp =
+ use_text context (1, "pp") false
+ ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
+
--- a/src/Pure/ML-Systems/smlnj.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML-Systems/smlnj.ML Sun May 31 22:00:56 2009 -0700
@@ -92,12 +92,6 @@
(*dummy implementation*)
fun exception_trace f = f ();
-(*dummy implementation*)
-fun print x = x;
-
-(*dummy implementation*)
-fun makestring x = "dummy string for SML New Jersey";
-
(* ML command execution *)
--- a/src/Pure/ML/ml_test.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/ML/ml_test.ML Sun May 31 22:00:56 2009 -0700
@@ -35,7 +35,7 @@
in (regs, context') end;
fun position_of ctxt
- ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) =
+ ({file, startLine = line, startPosition = i, endPosition = j, ...}: PolyML.location) =
(case pairself (Inttab.lookup (Extra_Env.get (Context.Proof ctxt))) (i, j) of
(SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
| (SOME pos, NONE) => pos
@@ -47,15 +47,15 @@
fun report_parse_tree context depth space =
let
val pos_of = position_of (Context.proof_of context);
- fun report loc (PTtype types) =
+ fun report loc (PolyML.PTtype types) =
PolyML.NameSpace.displayTypeExpression (types, depth, space)
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of
|> Position.report_text Markup.ML_typing (pos_of loc)
- | report loc (PTdeclaredAt decl) =
+ | report loc (PolyML.PTdeclaredAt decl) =
Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
|> Position.report_text Markup.ML_ref (pos_of loc)
- | report _ (PTnextSibling tree) = report_tree (tree ())
- | report _ (PTfirstChild tree) = report_tree (tree ())
+ | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
+ | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
| report _ _ = ()
and report_tree (loc, props) = List.app (report loc) props;
in report_tree end;
--- a/src/Pure/meta_simplifier.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/meta_simplifier.ML Sun May 31 22:00:56 2009 -0700
@@ -158,11 +158,6 @@
Thm.eq_thm_prop (thm1, thm2);
-(* congruences *)
-
-val eq_cong = Thm.eq_thm_prop
-
-
(* simplification sets, procedures, and solvers *)
(*A simpset contains data required during conversion:
@@ -785,7 +780,7 @@
val prems' = merge Thm.eq_thm_prop (prems1, prems2);
val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
- val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
+ val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
val weak' = merge (op =) (weak1, weak2);
val procs' = Net.merge eq_proc (procs1, procs2);
val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
--- a/src/Pure/mk Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/mk Sun May 31 22:00:56 2009 -0700
@@ -114,7 +114,7 @@
-e "val ml_platform = \"$ML_PLATFORM\";" \
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
-e "ml_prompts \"ML> \" \"ML# \";" \
- -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
+ -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
RC="$?"
fi
--- a/src/Pure/simplifier.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Pure/simplifier.ML Sun May 31 22:00:56 2009 -0700
@@ -348,16 +348,7 @@
-(** proof methods **)
-
-(* simplification *)
-
-val simp_options =
- (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
- Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
- Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
- Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
- Scan.succeed asm_full_simp_tac);
+(** method syntax **)
val cong_modifiers =
[Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
@@ -379,25 +370,33 @@
>> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
@ cong_modifiers;
-fun simp_args more_mods =
- Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options)
- (more_mods @ simp_modifiers');
+val simp_options =
+ (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
+ Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
+ Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
+ Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
+ Scan.succeed asm_full_simp_tac);
-fun simp_method (prems, tac) ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac (prems @ facts)) THEN
- (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
-
-fun simp_method' (prems, tac) ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN'
- ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
+fun simp_method more_mods meth =
+ Args.bang_facts -- Scan.lift simp_options --|
+ Method.sections (more_mods @ simp_modifiers') >>
+ (fn (prems, tac) => fn ctxt => METHOD (fn facts => meth ctxt tac (prems @ facts)));
(** setup **)
-fun method_setup more_mods = Method.add_methods
- [(simpN, simp_args more_mods simp_method', "simplification"),
- ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
+fun method_setup more_mods =
+ Method.setup (Binding.name simpN)
+ (simp_method more_mods (fn ctxt => fn tac => fn facts =>
+ HEADGOAL (Method.insert_tac facts THEN'
+ (CHANGED_PROP oo tac) (local_simpset_of ctxt))))
+ "simplification" #>
+ Method.setup (Binding.name "simp_all")
+ (simp_method more_mods (fn ctxt => fn tac => fn facts =>
+ ALLGOALS (Method.insert_tac facts) THEN
+ (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt)))
+ "simplification (all goals)";
fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>
let
--- a/src/Tools/Compute_Oracle/am_sml.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Tools/Compute_Oracle/am_sml.ML Sun May 31 22:00:56 2009 -0700
@@ -320,7 +320,7 @@
val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa)
val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs
val right = (indexed "C" c)^" "^(string_of_tuple xs)
- val message = "(\"unresolved lazy call: "^(string_of_int c)^", \"^(makestring x"^(string_of_int (strict_args - 1))^"))"
+ val message = "(\"unresolved lazy call: " ^ string_of_int c ^ "\")"
val right = if strict_args < the (arity_of c) then "raise AM_SML.Run "^message else right
in
(indexed "c" c)^(if gnum > 0 then "_"^(str gnum) else "")^leftargs^" = "^right
--- a/src/Tools/Compute_Oracle/compute.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Tools/Compute_Oracle/compute.ML Sun May 31 22:00:56 2009 -0700
@@ -379,7 +379,11 @@
fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
- val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
+ val _ =
+ if not (null shyps) then
+ raise Compute ("dangling sort hypotheses: " ^
+ commas (map (Syntax.string_of_sort_global thy) shyps))
+ else ()
in
Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
end)));
@@ -610,7 +614,8 @@
case match_aterms varsubst b' a' of
NONE =>
let
- fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s)
+ fun mk s = Syntax.string_of_term_global Pure.thy
+ (infer_types (naming_of computer) (encoding_of computer) ty s)
val left = "computed left side: "^(mk a')
val right = "computed right side: "^(mk b')
in
--- a/src/Tools/eqsubst.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Tools/eqsubst.ML Sun May 31 22:00:56 2009 -0700
@@ -20,25 +20,25 @@
* Zipper.T (* focusterm to search under *)
exception eqsubst_occL_exp of
- string * int list * Thm.thm list * int * Thm.thm
+ string * int list * thm list * int * thm
(* low level substitution functions *)
val apply_subst_in_asm :
int ->
- Thm.thm ->
- Thm.thm ->
- (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq
+ thm ->
+ thm ->
+ (cterm list * int * 'a * thm) * match -> thm Seq.seq
val apply_subst_in_concl :
int ->
- Thm.thm ->
- Thm.cterm list * Thm.thm ->
- Thm.thm -> match -> Thm.thm Seq.seq
+ thm ->
+ cterm list * thm ->
+ thm -> match -> thm Seq.seq
(* matching/unification within zippers *)
val clean_match_z :
- Context.theory -> Term.term -> Zipper.T -> match option
+ theory -> term -> Zipper.T -> match option
val clean_unify_z :
- Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq
+ theory -> int -> term -> Zipper.T -> match Seq.seq
(* skipping things in seq seq's *)
@@ -57,65 +57,64 @@
(* tactics *)
val eqsubst_asm_tac :
Proof.context ->
- int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
+ int list -> thm list -> int -> tactic
val eqsubst_asm_tac' :
Proof.context ->
- (searchinfo -> int -> Term.term -> match skipseq) ->
- int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
+ (searchinfo -> int -> term -> match skipseq) ->
+ int -> thm -> int -> tactic
val eqsubst_tac :
Proof.context ->
int list -> (* list of occurences to rewrite, use [0] for any *)
- Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
+ thm list -> int -> tactic
val eqsubst_tac' :
Proof.context -> (* proof context *)
- (searchinfo -> Term.term -> match Seq.seq) (* search function *)
- -> Thm.thm (* equation theorem to rewrite with *)
+ (searchinfo -> term -> match Seq.seq) (* search function *)
+ -> thm (* equation theorem to rewrite with *)
-> int (* subgoal number in goal theorem *)
- -> Thm.thm (* goal theorem *)
- -> Thm.thm Seq.seq (* rewritten goal theorem *)
+ -> thm (* goal theorem *)
+ -> thm Seq.seq (* rewritten goal theorem *)
val fakefree_badbounds :
- (string * Term.typ) list ->
- Term.term ->
- (string * Term.typ) list * (string * Term.typ) list * Term.term
+ (string * typ) list ->
+ term ->
+ (string * typ) list * (string * typ) list * term
val mk_foo_match :
- (Term.term -> Term.term) ->
- ('a * Term.typ) list -> Term.term -> Term.term
+ (term -> term) ->
+ ('a * typ) list -> term -> term
(* preparing substitution *)
- val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list
+ val prep_meta_eq : Proof.context -> thm -> thm list
val prep_concl_subst :
- int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo
+ int -> thm -> (cterm list * thm) * searchinfo
val prep_subst_in_asm :
- int -> Thm.thm -> int ->
- (Thm.cterm list * int * int * Thm.thm) * searchinfo
+ int -> thm -> int ->
+ (cterm list * int * int * thm) * searchinfo
val prep_subst_in_asms :
- int -> Thm.thm ->
- ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list
+ int -> thm ->
+ ((cterm list * int * int * thm) * searchinfo) list
val prep_zipper_match :
- Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term)
+ Zipper.T -> term * ((string * typ) list * (string * typ) list * term)
(* search for substitutions *)
val valid_match_start : Zipper.T -> bool
val search_lr_all : Zipper.T -> Zipper.T Seq.seq
val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
val searchf_lr_unify_all :
- searchinfo -> Term.term -> match Seq.seq Seq.seq
+ searchinfo -> term -> match Seq.seq Seq.seq
val searchf_lr_unify_valid :
- searchinfo -> Term.term -> match Seq.seq Seq.seq
+ searchinfo -> term -> match Seq.seq Seq.seq
val searchf_bt_unify_valid :
- searchinfo -> Term.term -> match Seq.seq Seq.seq
+ searchinfo -> term -> match Seq.seq Seq.seq
(* syntax tools *)
val ith_syntax : int list parser
val options_syntax : bool parser
(* Isar level hooks *)
- val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
- val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
- val subst_meth : Method.src -> Proof.context -> Proof.method
+ val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
+ val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
val setup : theory -> theory
end;
@@ -560,15 +559,13 @@
Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
(* combination method that takes a flag (true indicates that subst
-should be done to an assumption, false = apply to the conclusion of
-the goal) as well as the theorems to use *)
-fun subst_meth src =
- Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
- #> (fn (((asmflag, occL), inthms), ctxt) =>
- (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
-
-
+ should be done to an assumption, false = apply to the conclusion of
+ the goal) as well as the theorems to use *)
val setup =
- Method.add_method ("subst", subst_meth, "single-step substitution");
+ Method.setup @{binding subst}
+ (Scan.lift (options_syntax -- ith_syntax) -- Attrib.thms >>
+ (fn ((asmflag, occL), inthms) => fn ctxt =>
+ (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
+ "single-step substitution";
end;
--- a/src/Tools/intuitionistic.ML Sun May 31 21:59:33 2009 -0700
+++ b/src/Tools/intuitionistic.ML Sun May 31 22:00:56 2009 -0700
@@ -7,7 +7,7 @@
signature INTUITIONISTIC =
sig
val prover_tac: Proof.context -> int option -> int -> tactic
- val method_setup: bstring -> theory -> theory
+ val method_setup: binding -> theory -> theory
end;
structure Intuitionistic: INTUITIONISTIC =
@@ -84,15 +84,16 @@
modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
-val method =
- Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat))
- (fn n => fn prems => fn ctxt => METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN'
- ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));
-
in
-fun method_setup name = Method.add_method (name, method, "intuitionistic proof search");
+fun method_setup name =
+ Method.setup name
+ (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
+ Method.sections modifiers >>
+ (fn (prems, n) => fn ctxt => METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac (prems @ facts) THEN'
+ ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n))))
+ "intuitionistic proof search";
end;