--- a/NEWS Wed Jun 02 22:06:14 2010 +0200
+++ b/NEWS Wed Jun 02 22:45:50 2010 +0200
@@ -86,6 +86,9 @@
'hide_fact' replace the former 'hide' KIND command. Minor
INCOMPATIBILITY.
+* Improved parallelism of proof term normalization: usedir -p2 -q0 is
+more efficient than combinations with -q1 or -q2.
+
*** Pure ***
--- a/src/HOL/Extraction/ROOT.ML Wed Jun 02 22:06:14 2010 +0200
+++ b/src/HOL/Extraction/ROOT.ML Wed Jun 02 22:45:50 2010 +0200
@@ -1,6 +1,4 @@
(* Examples for program extraction in Higher-Order Logic *)
-Proofterm.proofs := 2;
-
no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"];
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
--- a/src/HOL/Import/ROOT.ML Wed Jun 02 22:06:14 2010 +0200
+++ b/src/HOL/Import/ROOT.ML Wed Jun 02 22:45:50 2010 +0200
@@ -1,8 +1,5 @@
(* Title: HOL/Import/ROOT.ML
- ID: $Id$
Author: Sebastian Skalberg (TU Muenchen)
*)
-Proofterm.proofs := 0;
-use_thy "HOL4Compat";
-use_thy "HOL4Syntax";
+use_thys ["HOL4Compat", "HOL4Syntax"];
--- a/src/HOL/IsaMakefile Wed Jun 02 22:06:14 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Jun 02 22:45:50 2010 +0200
@@ -506,7 +506,7 @@
HOL-Import: HOL $(LOG)/HOL-Import.gz
$(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
- @$(ISABELLE_TOOL) usedir $(OUT)/HOL Import
+ @$(ISABELLE_TOOL) usedir -p 0 $(OUT)/HOL Import
## HOL-Generate-HOL
@@ -857,7 +857,7 @@
Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy \
Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy \
Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex
- @$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL-Proofs Lambda
+ @$(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
## HOL-Prolog
@@ -942,7 +942,7 @@
Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML \
Extraction/Util.thy Extraction/Warshall.thy \
Extraction/document/root.tex Extraction/document/root.bib
- @$(ISABELLE_TOOL) usedir $(OUT)/HOL-Proofs Extraction
+ @$(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
## HOL-IOA
--- a/src/HOL/Lambda/ROOT.ML Wed Jun 02 22:06:14 2010 +0200
+++ b/src/HOL/Lambda/ROOT.ML Wed Jun 02 22:45:50 2010 +0200
@@ -1,5 +1,4 @@
Syntax.ambiguity_level := 100;
-Proofterm.proofs := 2;
no_document use_thys ["Code_Integer"];
use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];
--- a/src/Pure/Proof/reconstruct.ML Wed Jun 02 22:06:14 2010 +0200
+++ b/src/Pure/Proof/reconstruct.ML Wed Jun 02 22:45:50 2010 +0200
@@ -140,8 +140,7 @@
| SOME Ts => (Ts, env));
val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
(forall_intr_vfs prop) handle Library.UnequalLengths =>
- error ("Wrong number of type arguments for " ^
- quote (get_name [] prop prf))
+ error ("Wrong number of type arguments for " ^ quote (guess_name prf))
in (prop', change_type (SOME Ts) prf, [], env', vTs) end;
fun head_norm (prop, prf, cnstrts, env, vTs) =
--- a/src/Pure/proofterm.ML Wed Jun 02 22:06:14 2010 +0200
+++ b/src/Pure/proofterm.ML Wed Jun 02 22:45:50 2010 +0200
@@ -136,13 +136,11 @@
val promise_proof: theory -> serial -> term -> proof
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
- val unconstrain_thm_proofs: bool Unsynchronized.ref
val thm_proof: theory -> string -> sort list -> term list -> term ->
(serial * proof_body future) list -> proof_body -> pthm * proof
val unconstrain_thm_proof: theory -> sort list -> term ->
(serial * proof_body future) list -> proof_body -> pthm * proof
- val get_name: term list -> term -> proof -> string
- val get_name_unconstrained: sort list -> term list -> term -> proof -> string
+ val get_name: sort list -> term list -> term -> proof -> string
val guess_name: proof -> string
end
@@ -1422,7 +1420,7 @@
(***** theorems *****)
-fun prepare_thm_proof do_unconstrain thy name shyps hyps concl promises body =
+fun prepare_thm_proof thy name shyps hyps concl promises body =
let
val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
val prop = Logic.list_implies (hyps, concl);
@@ -1431,18 +1429,12 @@
if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
map SOME (frees_of prop);
- val (postproc, ofclasses, prop1, args1) =
- if do_unconstrain then
- let
- val ((atyp_map, constraints, outer_constraints), prop1) =
- Logic.unconstrainT shyps prop;
- val postproc = unconstrainT_body thy (atyp_map, constraints);
- val args1 =
- (map o Option.map o Term.map_types o Term.map_atyps)
- (Type.strip_sorts o atyp_map) args;
- in (postproc, map OfClass outer_constraints, prop1, args1) end
- else (I, [], prop, args);
- val argsP = ofclasses @ map Hyp hyps;
+ val ((atyp_map, constraints, outer_constraints), prop1) = Logic.unconstrainT shyps prop;
+ val postproc = unconstrainT_body thy (atyp_map, constraints);
+ val args1 =
+ (map o Option.map o Term.map_types o Term.map_atyps)
+ (Type.strip_sorts o atyp_map) args;
+ val argsP = map OfClass outer_constraints @ map Hyp hyps;
fun full_proof0 () =
#4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
@@ -1464,28 +1456,17 @@
val head = PThm (i, ((name, prop1, NONE), body'));
in ((i, (name, prop1, body')), head, args, argsP, args1) end;
-val unconstrain_thm_proofs = Unsynchronized.ref true;
-
fun thm_proof thy name shyps hyps concl promises body =
- let val (pthm, head, args, argsP, _) =
- prepare_thm_proof (! unconstrain_thm_proofs) thy name shyps hyps concl promises body
+ let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body
in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
fun unconstrain_thm_proof thy shyps concl promises body =
let
- val (pthm, head, _, _, args) =
- prepare_thm_proof true thy "" shyps [] concl promises body
+ val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
in (pthm, proof_combt' (head, args)) end;
-fun get_name hyps prop prf =
- let val prop = Logic.list_implies (hyps, prop) in
- (case strip_combt (fst (strip_combP prf)) of
- (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
- | _ => "")
- end;
-
-fun get_name_unconstrained shyps hyps prop prf =
+fun get_name shyps hyps prop prf =
let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
(case strip_combt (fst (strip_combP prf)) of
(PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
--- a/src/Pure/thm.ML Wed Jun 02 22:06:14 2010 +0200
+++ b/src/Pure/thm.ML Wed Jun 02 22:45:50 2010 +0200
@@ -584,8 +584,8 @@
(* closed derivations with official name *)
-fun derivation_name thm =
- Pt.guess_name (Pt.proof_of (raw_body thm)); (* FIXME tmp *)
+fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
+ Pt.get_name shyps hyps prop (Pt.proof_of body);
fun name_derivation name (thm as Thm (der, args)) =
let