# HG changeset patch # User wenzelm # Date 1563901496 -7200 # Node ID 65bbef66e2ec82161f3ae5781eddec27ab825fc6 # Parent ac570c179ee9cd524c29e19f3459caab5e67c9ef clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named; added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof; diff -r ac570c179ee9 -r 65bbef66e2ec src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Tue Jul 23 12:16:02 2019 +0200 +++ b/src/Pure/Proof/reconstruct.ML Tue Jul 23 19:04:56 2019 +0200 @@ -24,15 +24,6 @@ fun message ctxt msg = if Config.get ctxt quiet_mode then () else writeln (msg ()); -fun vars_of t = map Var (rev (Term.add_vars t [])); -fun frees_of t = map Free (rev (Term.add_frees t [])); - -fun forall_intr_vfs prop = fold_rev Logic.all - (vars_of prop @ frees_of prop) prop; - -fun forall_intr_vfs_prf prop prf = fold_rev Proofterm.forall_intr_proof' - (vars_of prop @ frees_of prop) prf; - (* generate constraints for proof term *) @@ -142,7 +133,7 @@ NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env | SOME Ts => (Ts, env)); val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) - (forall_intr_vfs prop) handle ListPair.UnequalLengths => + (Proofterm.forall_intr_vfs prop) handle ListPair.UnequalLengths => error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf)) in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end; @@ -305,7 +296,7 @@ fun prop_of_atom prop Ts = subst_atomic_types (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts) - (forall_intr_vfs prop); + (Proofterm.forall_intr_vfs prop); val head_norm = Envir.head_norm Envir.init; @@ -366,7 +357,7 @@ val _ = message ctxt (fn () => "Reconstructing proof of " ^ a ^ "\n" ^ Syntax.string_of_term ctxt prop); - val prf' = forall_intr_vfs_prf prop + val prf' = Proofterm.forall_intr_vfs_prf prop (reconstruct_proof ctxt prop (Proofterm.join_proof body)); val (maxidx', prfs', prf) = expand (Proofterm.maxidx_proof prf' ~1) prfs prf' diff -r ac570c179ee9 -r 65bbef66e2ec src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Jul 23 12:16:02 2019 +0200 +++ b/src/Pure/proofterm.ML Tue Jul 23 19:04:56 2019 +0200 @@ -149,6 +149,10 @@ (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof val rew_proof: theory -> proof -> proof + val forall_intr_vfs: term -> term + val forall_intr_vfs_prf: term -> proof -> proof + val clean_proof: proof -> proof + val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body val thm_proof: theory -> string -> sort list -> term list -> term -> (serial * proof_body future) list -> proof_body -> pthm * proof @@ -1567,6 +1571,62 @@ fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p)); +(* clean proof: expand unnamed PThm nodes *) + +local + +fun vars_of t = map Var (rev (Term.add_vars t [])); +fun frees_of t = map Free (rev (Term.add_frees t [])); +fun variables_of t = vars_of t @ frees_of t; + +in + +fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop; +fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf; + +end; + +fun clean_proof prf = + let + fun clean maxidx prfs (AbsP (s, t, prf)) = + let val (maxidx', prfs', prf') = clean maxidx prfs prf + in (maxidx', prfs', AbsP (s, t, prf')) end + | clean maxidx prfs (Abst (s, T, prf)) = + let val (maxidx', prfs', prf') = clean maxidx prfs prf + in (maxidx', prfs', Abst (s, T, prf')) end + | clean maxidx prfs (prf1 %% prf2) = + let + val (maxidx', prfs', prf1') = clean maxidx prfs prf1; + val (maxidx'', prfs'', prf2') = clean maxidx' prfs' prf2; + in (maxidx'', prfs'', prf1' %% prf2') end + | clean maxidx prfs (prf % t) = + let val (maxidx', prfs', prf') = clean maxidx prfs prf + in (maxidx', prfs', prf' % t) end + | clean maxidx prfs (PThm (_, (("", prop, SOME Ts), body))) = + let + val (maxidx', prf, prfs') = + (case AList.lookup (op =) prfs prop of + NONE => + let + val prf' = forall_intr_vfs_prf prop (join_proof body); + val (maxidx', prfs', prf) = clean (maxidx_proof prf' ~1) prfs prf'; + val prfs'' = (prop, (maxidx', prf)) :: prfs'; + in (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs'') end + | SOME (maxidx', prf) => (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs)); + val tfrees = Term.add_tfrees prop [] |> rev; + val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j)) + (Term.add_tvars prop [] |> rev) @ map (rpair ~1 o fst) tfrees ~~ Ts; + val varify = map_type_tfree (fn p as (a, S) => + if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p) + in + (maxidx', prfs', map_proof_types (typ_subst_TVars tye o varify) prf) + end + | clean maxidx prfs prf = (maxidx, prfs, prf); + + val maxidx = maxidx_proof prf ~1; + in norm_proof (Envir.empty maxidx) (#3 (clean maxidx [] prf)) end; + + (** promises **) @@ -1657,19 +1717,22 @@ (fn () => make_body0 (rew prf0)) end; + fun export i prf1 = + (if Options.default_bool "export_proofs" then + Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i])) + (Buffer.chunks + (YXML.buffer_body (Term_XML.Encode.term (term_of_proof prf1)) Buffer.empty)) + else (); + if Options.default_bool "prune_proofs" then MinProof else prf1); + + fun publish i = clean_proof #> export i #> shrink_proof; + fun new_prf () = let val i = serial (); - fun export prf1 = - (if Options.default_bool "export_proofs" then - Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i])) - (Buffer.chunks - (YXML.buffer_body (Term_XML.Encode.term (term_of_proof prf1)) Buffer.empty)) - else (); - if Options.default_bool "prune_proofs" then MinProof else prf1); val postproc = unconstrainT_body thy (atyp_map, constraints) #> - map_proof_of (export #> shrink_proof); + name <> "" ? map_proof_of (publish i); in (i, fulfill_proof_future thy promises postproc body0) end; val (i, body') = @@ -1677,7 +1740,7 @@ (case strip_combt (fst (strip_combP prf)) of (PThm (i, ((old_name, prop', NONE), body')), args') => if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args' - then (i, body') + then (i, body' |> name <> "" ? Future.map (map_proof_of (publish i))) else new_prf () | _ => new_prf ()); val head = PThm (i, ((name, prop1, NONE), body'));