# HG changeset patch # User huffman # Date 1325099152 -3600 # Node ID b4dcefaa17211c53c5d373cd4561c7acafe1e049 # Parent fad87bb608fcceb81a77fb42045c599738d26eba# Parent 493d9c4d7ed5b612db70aea6cc633f4ef55e0b5c merged diff -r fad87bb608fc -r b4dcefaa1721 Admin/PLATFORMS --- a/Admin/PLATFORMS Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/PLATFORMS Wed Dec 28 20:05:52 2011 +0100 @@ -61,21 +61,25 @@ 32 bit vs. 64 bit platforms --------------------------- -64 bit hardware becomes more and more important for many users. -Add-on tools need to work seamlessly without manual user -configuration, although it is often sufficient to fall back on 32 bit -executables. +Most users already have 64 bit hardware, and many of them are running +a 64 bit operating system. Native 64 bit support for ML and Scala/JVM +is increasingly important for big Isabelle applications, but 32 bit is +often the default to get started. Add-on executables need to work +seamlessly without manual user configuration, either as native 64 bit +executables or in 32 bit mode on a 64 bit platform. The ISABELLE_PLATFORM setting variable refers to the 32 bit version of -the platform, even on 64 bit hardware. Power-tools need to indicate -64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64 -setting. The following bash expression prefers the 64 bit platform, -if that is available: +the platform, even on 64 bit hardware. Tools need to indicate 64 bit +support explicitly via the (optional) ISABELLE_PLATFORM64 setting, if +this is really required. The following bash expression prefers the 64 +bit platform, if that is available: "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}" Note that ML and JVM may have a different idea of the platform, -depending on the respective binaries that are actually run. +depending on the respective binaries that are actually run. The +"uname" Unix tool usually only tells about its own executable format, +not the underlying platform. Dependable system tools diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/isatest-makeall --- a/Admin/isatest/isatest-makeall Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/isatest-makeall Wed Dec 28 20:05:52 2011 +0100 @@ -71,12 +71,6 @@ macbroy2) MFLAGS="-k" - TARGETS=full - NICE="" - ;; - - macbroy5) - MFLAGS="-k -j 2" NICE="" ;; @@ -102,7 +96,6 @@ macbroy30) MFLAGS="-k" - TARGETS=full NICE="" ;; @@ -124,8 +117,13 @@ TARGETS="$2" shift 2 ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)" - DIR="$ISABELLE_HOME/src/$LOGIC" - TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS" + if [ "$LOGIC" = "." ]; then + DIR="." + TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS" + else + DIR="$ISABELLE_HOME/src/$LOGIC" + TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS" + fi else DIR="." TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/isatest-makedist Wed Dec 28 20:05:52 2011 +0100 @@ -107,9 +107,11 @@ sleep 15 $SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly" sleep 15 -$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8; $MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8" -sleep 15 -$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly" +$SSH macbroy2 " + $MAKEALL $HOME/settings/mac-poly64-M4 -l . full; + $MAKEALL $HOME/settings/mac-poly64-M8 -l . full; + $MAKEALL $HOME/settings/mac-poly-M4; + $MAKEALL $HOME/settings/mac-poly-M8" sleep 15 $SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2" sleep 15 diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/afp-poly --- a/Admin/isatest/settings/afp-poly Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/afp-poly Wed Dec 28 20:05:52 2011 +0100 @@ -28,4 +28,4 @@ ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2" -init_component "$CONTRIB/kodkodi" +#init_component "$CONTRIB/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/at-poly --- a/Admin/isatest/settings/at-poly Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/at-poly Wed Dec 28 20:05:52 2011 +0100 @@ -24,5 +24,5 @@ ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true" -init_component "$HOME/contrib_devel/kodkodi" +#init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/at-poly-e --- a/Admin/isatest/settings/at-poly-e Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/at-poly-e Wed Dec 28 20:05:52 2011 +0100 @@ -24,4 +24,4 @@ ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true" -init_component "$HOME/contrib_devel/kodkodi" +#init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/at-poly-test --- a/Admin/isatest/settings/at-poly-test Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/at-poly-test Wed Dec 28 20:05:52 2011 +0100 @@ -28,4 +28,4 @@ ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml" ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl" -init_component "$HOME/contrib_devel/kodkodi" +#init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/at64-poly --- a/Admin/isatest/settings/at64-poly Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/at64-poly Wed Dec 28 20:05:52 2011 +0100 @@ -24,4 +24,4 @@ ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" -init_component "$HOME/contrib_devel/kodkodi" +#init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/cygwin-poly-e --- a/Admin/isatest/settings/cygwin-poly-e Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/cygwin-poly-e Wed Dec 28 20:05:52 2011 +0100 @@ -24,4 +24,4 @@ ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false" -init_component "$HOME/contrib/kodkodi" +#init_component "$HOME/contrib/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly --- a/Admin/isatest/settings/mac-poly Wed Dec 28 20:05:28 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - - POLYML_HOME="/home/polyml/polyml-5.2.1" - ML_SYSTEM="polyml-5.2.1" - ML_PLATFORM="ppc-darwin" - ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="-H 500" - -ISABELLE_HOME_USER=~/isabelle-mac-poly - -# 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 -g false" - -init_component "$HOME/contrib_devel/kodkodi" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly-M2 --- a/Admin/isatest/settings/mac-poly-M2 Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/mac-poly-M2 Wed Dec 28 20:05:52 2011 +0100 @@ -25,5 +25,5 @@ ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 2 -q 2" -init_component "$HOME/contrib_devel/kodkodi" +#init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly-M4 --- a/Admin/isatest/settings/mac-poly-M4 Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/mac-poly-M4 Wed Dec 28 20:05:52 2011 +0100 @@ -25,4 +25,4 @@ ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2" -init_component "$HOME/contrib_devel/kodkodi" +#init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly-M8 --- a/Admin/isatest/settings/mac-poly-M8 Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/mac-poly-M8 Wed Dec 28 20:05:52 2011 +0100 @@ -25,5 +25,5 @@ ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2" -init_component "$HOME/contrib_devel/kodkodi" +#init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly64-M2 --- a/Admin/isatest/settings/mac-poly64-M2 Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/mac-poly64-M2 Wed Dec 28 20:05:52 2011 +0100 @@ -25,5 +25,5 @@ ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 2 -q 2" -init_component "$HOME/contrib_devel/kodkodi" +#init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly64-M4 --- a/Admin/isatest/settings/mac-poly64-M4 Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/mac-poly64-M4 Wed Dec 28 20:05:52 2011 +0100 @@ -25,4 +25,4 @@ ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2" -init_component "$HOME/contrib_devel/kodkodi" +#init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly64-M8 --- a/Admin/isatest/settings/mac-poly64-M8 Wed Dec 28 20:05:28 2011 +0100 +++ b/Admin/isatest/settings/mac-poly64-M8 Wed Dec 28 20:05:52 2011 +0100 @@ -25,5 +25,5 @@ ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2" -init_component "$HOME/contrib_devel/kodkodi" +#init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r fad87bb608fc -r b4dcefaa1721 src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Wed Dec 28 20:05:28 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Wed Dec 28 20:05:52 2011 +0100 @@ -12,6 +12,7 @@ val make_case : Proof.context -> config -> string list -> term -> (term * term) list -> term val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option val case_tr: bool -> Proof.context -> term list -> term + val show_cases: bool Config.T val case_tr': string -> Proof.context -> term list -> term val add_case_tr' : string list -> theory -> theory val setup: theory -> theory @@ -414,27 +415,31 @@ (* print translation *) +val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true); + fun case_tr' cname ctxt ts = - let - fun mk_clause (pat, rhs) = - let val xs = Term.add_frees pat [] in - Syntax.const @{syntax_const "_case1"} $ - map_aterms - (fn Free p => Syntax_Trans.mark_boundT p - | Const (s, _) => Syntax.const (Lexicon.mark_const s) - | t => t) pat $ - map_aterms - (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x - | t => t) rhs - end; - in - (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of - SOME (x, clauses) => - Syntax.const @{syntax_const "_case_syntax"} $ x $ - foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u) - (map mk_clause clauses) - | NONE => raise Match) - end; + if Config.get ctxt show_cases then + let + fun mk_clause (pat, rhs) = + let val xs = Term.add_frees pat [] in + Syntax.const @{syntax_const "_case1"} $ + map_aterms + (fn Free p => Syntax_Trans.mark_boundT p + | Const (s, _) => Syntax.const (Lexicon.mark_const s) + | t => t) pat $ + map_aterms + (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x + | t => t) rhs + end; + in + (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of + SOME (x, clauses) => + Syntax.const @{syntax_const "_case_syntax"} $ x $ + foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u) + (map mk_clause clauses) + | NONE => raise Match) + end + else raise Match; fun add_case_tr' case_names thy = Sign.add_advanced_trfuns ([], [],