# HG changeset patch # User blanchet # Date 1284574061 -7200 # Node ID f5320aba6750a72793c91ddf098adff22848d5bd # Parent 84647a469fda2a782b12fed961d991d3240d1b28# Parent afb4d5c672bdcd1eafda959af150706a2f0e3fb2 merged diff -r 84647a469fda -r f5320aba6750 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 ([], []))) diff -r 84647a469fda -r f5320aba6750 src/Tools/Metis/README --- /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 diff -r 84647a469fda -r f5320aba6750 src/Tools/Metis/make_metis --- 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) diff -r 84647a469fda -r f5320aba6750 src/Tools/Metis/metis.ML --- 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. *) diff -r 84647a469fda -r f5320aba6750 src/Tools/Metis/src/Portable.sig --- 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. *) (* ------------------------------------------------------------------------- *) diff -r 84647a469fda -r f5320aba6750 src/Tools/Metis/src/PortableMlton.sml --- 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. *) (* ------------------------------------------------------------------------- *) diff -r 84647a469fda -r f5320aba6750 src/Tools/Metis/src/PortableMosml.sml --- 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. *) (* ------------------------------------------------------------------------- *) diff -r 84647a469fda -r f5320aba6750 src/Tools/Metis/src/PortablePolyml.sml --- 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. *) diff -r 84647a469fda -r f5320aba6750 src/Tools/Metis/src/Random.sig --- 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 diff -r 84647a469fda -r f5320aba6750 src/Tools/Metis/src/Random.sml --- 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;