--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Sep 15 19:20:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Sep 15 20:07:41 2010 +0200
@@ -62,6 +62,9 @@
| mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
+fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
+
datatype raw_step_name = Str of string * string | Num of string
fun raw_step_num (Str (num, _)) = num
@@ -454,12 +457,11 @@
| do_term (t1 $ t2) = do_term t1 $ do_term t2
in t |> not (Vartab.is_empty tvar_tab) ? do_term end
-(* ### TODO: looks broken; see forall_of below *)
-fun quantify_over_free quant_s free_s body_t =
- case Term.add_frees body_t [] |> filter (curry (op =) free_s o fst) of
- [] => body_t
- | frees as (_, free_T) :: _ =>
- Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t)
+fun quantify_over_var quant_of var_s t =
+ let
+ val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
+ |> map Var
+ in fold_rev quant_of vars t end
(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
appear in the formula. *)
@@ -470,10 +472,10 @@
AQuant (_, [], phi) => do_formula pos phi
| AQuant (q, x :: xs, phi') =>
do_formula pos (AQuant (q, xs, phi'))
- #>> quantify_over_free (case q of
- AForall => @{const_name All}
- | AExists => @{const_name Ex})
- (repair_atp_variable_name Char.toLower x)
+ #>> quantify_over_var (case q of
+ AForall => forall_of
+ | AExists => exists_of)
+ (repair_atp_variable_name Char.toLower x)
| AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
| AConn (c, [phi1, phi2]) =>
do_formula (pos |> c = AImplies ? not) phi1
@@ -731,15 +733,13 @@
else
apfst (insert (op =) (raw_label_for_name conjecture_shape name))
-fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
-fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
-
fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
| step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
Assume (raw_label_for_name conjecture_shape name, t)
| step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
Have (if j = 1 then [Show] else [],
- raw_label_for_name conjecture_shape name, forall_vars t,
+ raw_label_for_name conjecture_shape name,
+ fold_rev forall_of (map Var (Term.add_vars t [])) t,
ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
deps ([], [])))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/README Wed Sep 15 20:07:41 2010 +0200
@@ -0,0 +1,70 @@
+It's a good idea to update the Metis source code regularly, to benefit
+from the latest developments, to avoid a permanent fork, and to detect
+Metis problems early. This file explains how to update the source code
+for Metis with the latest Metis package. The procedure is
+unfortunately somewhat involved and frustrating, and hopefully
+temporary.
+
+ 1. The directories "src/" and "script/" were initially copied from
+ Joe Hurd's Metis package. (His "script/" directory has many files
+ in it, but we only need "mlpp".) The package that was used when
+ these notes where written was an unnumbered version of Metis, more
+ recent than 2.2 and dated 19 July 2010.
+
+ 2. The license in each source file will probably not be something we
+ can use in Isabelle. Lawrence C. Paulson's command
+
+ perl -p -i~ -w -e 's/MIT license/BSD License/g' *sig *sml
+
+ run in the "src/" directory should do the trick. In a 13 Sept.
+ 2010 email to Gerwin Klein, Joe Hurd, the sole copyright holder of
+ Metis, wrote:
+
+ I hereby give permission to the Isabelle team to release Metis as part
+ of Isabelle, with the Metis code covered under the Isabelle BSD license.
+
+ 3. Some modifications have to be done manually to the source files.
+ Some of these are necessary so that the sources compile at all
+ with Isabelle, some are necessary to avoid race conditions in a
+ multithreaded environment, and some affect the defaults of Metis's
+ heuristics and are needed for backward compatibility with older
+ Isabelle proofs and for performance reasons. These changes should
+ be identified by a comment
+
+ (* MODIFIED by ?Joe ?Blow *)
+
+ but the ultimate way to track them down is to use Mercurial. The
+ command
+
+ hg diff -r2d0a4361c3ef: src
+
+ should do the trick. (You might need to specify a different
+ revision number if somebody updated the Metis sources without
+ updating these instructions.)
+
+ 4. Isabelle itself only cares about "metis.ML", which is generated
+ from the files in "src/" by the script "make_metis". The script
+ relies on "src/", "scripts/", and a hand-crafted "FILES" file
+ listing all the files needed to be included in "metis.ML". The
+ "FILES" file should be updated to reflect the contents of "src/",
+ although a few files in "src/" are not necessary. Also, the order
+ of the file names in "FILES" matters; X must appear before Y if Y
+ depends on X.
+
+ 5. The output of "make_metis" should then work as is with Isabelle,
+ but there are of course no guarantees. The script "make_metis" has
+ a few evil regex hacks that could go wrong.
+
+ 6. Once you have successfully regenerated "metis.ML", build all of
+ Isabelle and keep an eye on the time taken by Metis.
+ "HOL-Metis_Examples" is a good test case. Running the Judgement
+ Day suite at this point is also a good idea.
+
+ 7. Once everything is fine and you are ready to push your changes to
+ the main Isabelle repository, take the time to update these
+ instructions, especially points 1 and 3 above.
+
+Good luck!
+
+ Jasmin Blanchette
+ 15 Sept. 2010
--- a/src/Tools/Metis/make_metis Wed Sep 15 19:20:50 2010 +0200
+++ b/src/Tools/Metis/make_metis Wed Sep 15 20:07:41 2010 +0200
@@ -2,9 +2,9 @@
#
# make_metis - turn original Metis files into Isabelle ML source.
#
-# Structure declarations etc. are made local by wrapping into a
-# collective structure Metis. Signature and functor definitions are
-# global!
+# Signatures, structures, and functors are renamed to have a "Metis_" prefix.
+# A few other ad hoc transformations are performed to ensure that the sources
+# compile within Isabelle on Poly/ML and SML/NJ.
THIS=$(cd "$(dirname "$0")"; echo $PWD)
--- a/src/Tools/Metis/metis.ML Wed Sep 15 19:20:50 2010 +0200
+++ b/src/Tools/Metis/metis.ML Wed Sep 15 20:07:41 2010 +0200
@@ -29,8 +29,6 @@
signature Metis_Random =
sig
- val CRITICAL: (unit -> 'a) -> 'a (* MODIFIED by Jasmin Blanchette *)
-
val nextWord : unit -> word
val nextBool : unit -> bool
@@ -54,9 +52,6 @@
structure Metis_Random :> Metis_Random =
struct
-(* MODIFIED by Jasmin Blanchette *)
-fun CRITICAL e = NAMED_CRITICAL "metis" e;
-
(* random words: 0w0 <= result <= max_word *)
(*minimum length of unboxed words on all supported ML platforms*)
@@ -73,8 +68,7 @@
fun change r f = r := f (!r);
local val rand = (*Unsynchronized.*)Unsynchronized.ref 0w1
-(* MODIFIED by Jasmin Blanchette *)
-in fun nextWord () = CRITICAL (fn () => ((*Unsynchronized.*)change rand step; ! rand)) end;
+in fun nextWord () = ((*Unsynchronized.*)change rand step; ! rand) end;
(*NB: higher bits are more random than lower ones*)
fun nextBool () = Word.andb (nextWord (), top_bit) = 0w0;
@@ -125,6 +119,13 @@
val time : ('a -> 'b) -> 'a -> 'b
(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+(* MODIFIED by Jasmin Blanchette *)
+val CRITICAL: (unit -> 'a) -> 'a
+
+(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
@@ -198,6 +199,13 @@
y
end;
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+(* MODIFIED by Jasmin Blanchette *)
+fun CRITICAL e = NAMED_CRITICAL "metis" e;
+
(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
--- a/src/Tools/Metis/src/Portable.sig Wed Sep 15 19:20:50 2010 +0200
+++ b/src/Tools/Metis/src/Portable.sig Wed Sep 15 20:07:41 2010 +0200
@@ -25,6 +25,13 @@
val time : ('a -> 'b) -> 'a -> 'b
(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+(* MODIFIED by Jasmin Blanchette *)
+val CRITICAL: (unit -> 'a) -> 'a
+
+(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/PortableMlton.sml Wed Sep 15 19:20:50 2010 +0200
+++ b/src/Tools/Metis/src/PortableMlton.sml Wed Sep 15 20:07:41 2010 +0200
@@ -57,6 +57,13 @@
end;
(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+(* MODIFIED by Jasmin Blanchette *)
+fun CRITICAL e = e (); (*dummy*)
+
+(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/PortableMosml.sml Wed Sep 15 19:20:50 2010 +0200
+++ b/src/Tools/Metis/src/PortableMosml.sml Wed Sep 15 20:07:41 2010 +0200
@@ -29,6 +29,13 @@
val time = Mosml.time;
(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+(* MODIFIED by Jasmin Blanchette *)
+fun CRITICAL e = e (); (*dummy*)
+
+(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/PortablePolyml.sml Wed Sep 15 19:20:50 2010 +0200
+++ b/src/Tools/Metis/src/PortablePolyml.sml Wed Sep 15 20:07:41 2010 +0200
@@ -56,6 +56,13 @@
y
end;
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+(* MODIFIED by Jasmin Blanchette *)
+fun CRITICAL e = NAMED_CRITICAL "metis" e;
+
(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
--- a/src/Tools/Metis/src/Random.sig Wed Sep 15 19:20:50 2010 +0200
+++ b/src/Tools/Metis/src/Random.sig Wed Sep 15 20:07:41 2010 +0200
@@ -8,8 +8,6 @@
signature Random =
sig
- val CRITICAL: (unit -> 'a) -> 'a (* MODIFIED by Jasmin Blanchette *)
-
val nextWord : unit -> word
val nextBool : unit -> bool
--- a/src/Tools/Metis/src/Random.sml Wed Sep 15 19:20:50 2010 +0200
+++ b/src/Tools/Metis/src/Random.sml Wed Sep 15 20:07:41 2010 +0200
@@ -9,9 +9,6 @@
structure Random :> Random =
struct
-(* MODIFIED by Jasmin Blanchette *)
-fun CRITICAL e = NAMED_CRITICAL "metis" e;
-
(* random words: 0w0 <= result <= max_word *)
(*minimum length of unboxed words on all supported ML platforms*)
@@ -28,8 +25,7 @@
fun change r f = r := f (!r);
local val rand = (*Unsynchronized.*)ref 0w1
-(* MODIFIED by Jasmin Blanchette *)
-in fun nextWord () = CRITICAL (fn () => ((*Unsynchronized.*)change rand step; ! rand)) end;
+in fun nextWord () = ((*Unsynchronized.*)change rand step; ! rand) end;
(*NB: higher bits are more random than lower ones*)
fun nextBool () = Word.andb (nextWord (), top_bit) = 0w0;