# HG changeset patch # User wenzelm # Date 1273923085 -7200 # Node ID dbd39471211c048143e2a2fe66ffe18476d578d7 # Parent 4ef12072b94a657f25520a496e60af8d9735c1c1# Parent 4ed0d72def502a1e3373507555cb0aba3a71fdd8 merged diff -r 4ef12072b94a -r dbd39471211c src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Fri May 14 23:35:35 2010 +0200 +++ b/src/Pure/ML-Systems/polyml_common.ML Sat May 15 13:31:25 2010 +0200 @@ -6,7 +6,11 @@ exception Interrupt = SML90.Interrupt; use "General/exn.ML"; -use "ML-Systems/single_assignment_polyml.ML"; + +if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ()) +then () +else use "ML-Systems/single_assignment_polyml.ML"; + use "ML-Systems/multithreading.ML"; use "ML-Systems/time_limit.ML"; use "ML-Systems/timing.ML"; diff -r 4ef12072b94a -r dbd39471211c src/Pure/axclass.ML --- a/src/Pure/axclass.ML Fri May 14 23:35:35 2010 +0200 +++ b/src/Pure/axclass.ML Sat May 15 13:31:25 2010 +0200 @@ -196,9 +196,9 @@ fun the_classrel thy (c1, c2) = (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of - SOME thm => Thm.transfer thy thm + SOME thm => thm | NONE => error ("Unproven class relation " ^ - Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2])); + Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2])); (* FIXME stale thy (!?) *) fun put_trancl_classrel ((c1, c2), th) thy = let @@ -206,7 +206,7 @@ val classrels = proven_classrels_of thy; fun reflcl_classrel (c1', c2') = - if c1' = c2' then NONE else SOME (the_classrel thy (c1', c2')); + if c1' = c2' then NONE else SOME (Thm.transfer thy (the_classrel thy (c1', c2'))); fun gen_classrel (c1_pred, c2_succ) = let val th' = @@ -243,9 +243,9 @@ fun the_arity thy (a, Ss, c) = (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of - SOME (thm, _) => Thm.transfer thy thm + SOME (thm, _) => thm | NONE => error ("Unproven type arity " ^ - Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c]))); + Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c]))); (* FIXME stale thy (!?) *) fun thynames_of_arity thy (c, a) = Symtab.lookup_list (proven_arities_of thy) a @@ -267,7 +267,7 @@ val completions = super_class_completions |> map (fn c1 => let val th1 = - (th RS the_classrel thy (c, c1)) + (th RS Thm.transfer thy (the_classrel thy (c, c1))) |> Drule.instantiate' std_vars [] |> Thm.close_derivation; in ((th1, thy_name), c1) end); diff -r 4ef12072b94a -r dbd39471211c src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri May 14 23:35:35 2010 +0200 +++ b/src/Pure/proofterm.ML Sat May 15 13:31:25 2010 +0200 @@ -118,11 +118,6 @@ arity_proof: theory -> string * sort list * class -> proof} -> unit val axm_proof: string -> term -> proof val oracle_proof: string -> term -> oracle * proof - val promise_proof: theory -> serial -> term -> proof - val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body - val thm_proof: theory -> string -> term list -> term -> - (serial * proof_body future) list -> proof_body -> pthm * proof - val get_name: term list -> term -> proof -> string (** rewriting on proof terms **) val add_prf_rrule: proof * proof -> theory -> theory @@ -134,6 +129,17 @@ val rewrite_proof_notypes: (proof * proof) list * (typ list -> proof -> (proof * proof) option) list -> proof -> proof val rew_proof: theory -> proof -> proof + + 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 guess_name: proof -> string end structure Proofterm : PROOFTERM = @@ -344,7 +350,7 @@ fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs) | change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c) | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs) - | change_type opTs (Promise _) = error "change_type: unexpected promise" + | change_type opTs (Promise _) = raise Fail "change_type: unexpected promise" | change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body)) | change_type _ prf = prf; @@ -1071,7 +1077,7 @@ | Oracle (_, prop, _) => prop | Promise (_, prop, _) => prop | PThm (_, ((_, prop, _), _)) => prop - | _ => error "shrink: proof not in normal form"); + | _ => raise Fail "shrink: proof not in normal form"); val vs = vars_of prop; val (ts', ts'') = chop (length vs) ts; val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts'; @@ -1348,9 +1354,9 @@ let val _ = prop |> Term.exists_subterm (fn t => (Term.is_Free t orelse Term.is_Var t) andalso - error ("promise_proof: illegal variable " ^ Syntax.string_of_term_global thy t)); + raise Fail ("promise_proof: illegal variable " ^ Syntax.string_of_term_global thy t)); val _ = prop |> Term.exists_type (Term.exists_subtype - (fn TFree (a, _) => error ("promise_proof: illegal type variable " ^ quote a) + (fn TFree (a, _) => raise Fail ("promise_proof: illegal type variable " ^ quote a) | _ => false)); in Promise (i, prop, map TVar (Term.add_tvars prop [])) end; @@ -1370,15 +1376,40 @@ val proof = rewrite_prf fst (rules, K fill :: procs) proof0; in PBody {oracles = oracles, thms = thms, proof = proof} end; -fun fulfill_proof_future _ [] body = Future.value body - | fulfill_proof_future thy promises body = +fun fulfill_proof_future _ [] postproc body = Future.value (postproc body) + | fulfill_proof_future thy promises postproc body = Future.fork_deps (map snd promises) (fn () => - fulfill_norm_proof thy (map (apsnd Future.join) promises) body); + postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) body)); + + +(***** abstraction over sort constraints *****) + +fun unconstrainT_prf thy (atyp_map, constraints) = + let + fun hyp_map hyp = + (case AList.lookup (op =) constraints hyp of + SOME t => Hyp t + | NONE => raise Fail "unconstrainT_prf: missing constraint"); + + val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o atyp_map); + fun ofclass (ty, c) = + let val ty' = Term.map_atyps atyp_map ty; + in the_single (of_sort_proof thy hyp_map (ty', [c])) end; + in + Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass) + #> fold_rev (implies_intr_proof o snd) constraints + end; + +fun unconstrainT_body thy constrs (PBody {oracles, thms, proof}) = + PBody + {oracles = oracles, (* FIXME merge (!), unconstrain (!?!) *) + thms = thms, (* FIXME merge (!) *) + proof = unconstrainT_prf thy constrs proof}; (***** theorems *****) -fun thm_proof thy name hyps concl promises body = +fun prepare_thm_proof do_unconstrain thy name shyps hyps concl promises body = let val PBody {oracles = oracles0, thms = thms0, proof = prf} = body; val prop = Logic.list_implies (hyps, concl); @@ -1387,24 +1418,48 @@ 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), 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 o fst) constraints, prop1, args1) end + else (I, [], prop, args); + val argsP = ofclasses @ map Hyp hyps; + val proof0 = if ! proofs = 2 then #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf))) else MinProof; val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0}; - fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0); - val (i, name, prop, body') = + fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0); + val (i, body') = (case strip_combt (fst (strip_combP prf)) of (PThm (i, ((old_name, prop', NONE), body')), args') => - if (old_name = "" orelse old_name = name) andalso prop = prop' andalso args = args' - then (i, name, prop, body') + if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args' + then (i, body') else new_prf () | _ => new_prf ()); - val head = PThm (i, ((name, prop, NONE), body')); - in - ((i, (name, prop, body')), proof_combP (proof_combt' (head, args), map Hyp hyps)) - end; + val head = PThm (i, ((name, prop1, NONE), body')); + in ((i, (name, prop1, body')), head, args, argsP, args1) end; + +val unconstrain_thm_proofs = Unsynchronized.ref false; + +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 + 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 + in (pthm, proof_combt' (head, args)) end; + fun get_name hyps prop prf = let val prop = Logic.list_implies (hyps, prop) in @@ -1413,6 +1468,20 @@ | _ => "") end; +fun get_name_unconstrained 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 "" + | _ => "") + end; + +fun guess_name (PThm (_, ((name, _, _), _))) = name + | guess_name (prf %% Hyp _) = guess_name prf + | guess_name (prf %% OfClass _) = guess_name prf + | guess_name (prf % NONE) = guess_name prf + | guess_name (prf % SOME (Var _)) = guess_name prf + | guess_name _ = ""; + end; structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm; diff -r 4ef12072b94a -r dbd39471211c src/Pure/thm.ML --- a/src/Pure/thm.ML Fri May 14 23:35:35 2010 +0200 +++ b/src/Pure/thm.ML Sat May 15 13:31:25 2010 +0200 @@ -586,17 +586,17 @@ (* closed derivations with official name *) fun derivation_name thm = - Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm)); + Pt.guess_name (Pt.proof_of (raw_body thm)); (* FIXME tmp *) fun name_derivation name (thm as Thm (der, args)) = let val Deriv {promises, body} = der; - val {thy_ref, hyps, prop, tpairs, ...} = args; + val {thy_ref, shyps, hyps, prop, tpairs, ...} = args; val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]); val ps = map (apsnd (Future.map proof_body_of)) promises; val thy = Theory.deref thy_ref; - val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body; + val (pthm, proof) = Pt.thm_proof thy name shyps hyps prop ps body; val der' = make_deriv [] [] [pthm] proof; val _ = Theory.check_thy thy; in Thm (der', args) end; @@ -1222,24 +1222,30 @@ end; (*Internalize sort constraints of type variables*) -fun unconstrainT (thm as Thm (_, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = +fun unconstrainT (thm as Thm (der, args)) = let + val Deriv {promises, body} = der; + val {thy_ref, shyps, hyps, tpairs, prop, ...} = args; + fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); - val _ = null hyps orelse err "illegal hyps"; val _ = null tpairs orelse err "unsolved flex-flex constraints"; val tfrees = rev (Term.add_tfree_names prop []); val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); - val (_, prop') = Logic.unconstrainT shyps prop; + val ps = map (apsnd (Future.map proof_body_of)) promises; + val thy = Theory.deref thy_ref; + val (pthm as (_, (_, prop', _)), proof) = Pt.unconstrain_thm_proof thy shyps prop ps body; + val der' = make_deriv [] [] [pthm] proof; + val _ = Theory.check_thy thy; in - Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])), + Thm (der', {thy_ref = thy_ref, tags = [], maxidx = maxidx_of_term prop', shyps = [[]], (*potentially redundant*) - hyps = hyps, - tpairs = tpairs, + hyps = [], + tpairs = [], prop = prop'}) end;