# HG changeset patch # User wenzelm # Date 1572630217 -3600 # Node ID 6178ecf357a03653c9af75487095404e37b0c976 # Parent a7a52ba0717d60e514a56ccec43b24a7a52207eb# Parent d8a7df9fdd03d2ef13389aa822586a38a5d5b9ec merged diff -r a7a52ba0717d -r 6178ecf357a0 src/Pure/Admin/build_polyml.scala --- a/src/Pure/Admin/build_polyml.scala Thu Oct 31 09:02:02 2019 +0000 +++ b/src/Pure/Admin/build_polyml.scala Fri Nov 01 18:43:37 2019 +0100 @@ -74,6 +74,10 @@ case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode) } + if (Platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) { + error("""Missing "chrpath" executable on Linux""") + } + /* bash */ diff -r a7a52ba0717d -r 6178ecf357a0 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Oct 31 09:02:02 2019 +0000 +++ b/src/Pure/PIDE/document.scala Fri Nov 01 18:43:37 2019 +0100 @@ -408,6 +408,7 @@ } yield cmd).toList def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names) + def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds(names).reverse def topological_order: List[Node.Name] = graph.topological_order override def toString: String = topological_order.mkString("Nodes(", ",", ")") diff -r a7a52ba0717d -r 6178ecf357a0 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Thu Oct 31 09:02:02 2019 +0000 +++ b/src/Pure/Proof/proof_syntax.ML Fri Nov 01 18:43:37 2019 +0100 @@ -7,6 +7,7 @@ signature PROOF_SYNTAX = sig val add_proof_syntax: theory -> theory + val term_of_proof: proof -> term val proof_of_term: theory -> bool -> term -> Proofterm.proof val read_term: theory -> bool -> typ -> string -> term val read_proof: theory -> bool -> bool -> string -> Proofterm.proof @@ -14,6 +15,7 @@ val proof_of: bool -> thm -> Proofterm.proof val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T + val pretty_proof_boxes_of: Proof.context -> bool -> thm -> Pretty.T end; structure Proof_Syntax : PROOF_SYNTAX = @@ -21,7 +23,7 @@ (**** add special syntax for embedding proof terms ****) -val proofT = Proofterm.proofT; +val proofT = Type ("Pure.proof", []); local @@ -79,7 +81,60 @@ |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); -(**** translation between proof terms and pure terms ****) + +(** proof terms as pure terms **) + +(* term_of_proof *) + +local + +val AbsPt = Const ("Pure.AbsP", propT --> (proofT --> proofT) --> proofT); +val AppPt = Const ("Pure.AppP", proofT --> proofT --> proofT); +val Hypt = Const ("Pure.Hyp", propT --> proofT); +val Oraclet = Const ("Pure.Oracle", propT --> proofT); +val MinProoft = Const ("Pure.MinProof", proofT); + +fun AppT T prf = + Const ("Pure.Appt", proofT --> Term.itselfT T --> proofT) $ prf $ Logic.mk_type T; + +fun OfClasst (T, c) = + let val U = Term.itselfT T --> propT + in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end; + +fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) = + fold AppT (these Ts) + (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT)) + | term_of _ (PAxm (name, _, Ts)) = + fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT)) + | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c)) + | term_of _ (PBound i) = Bound i + | term_of Ts (Abst (s, opT, prf)) = + let val T = the_default dummyT opT in + Const ("Pure.Abst", (T --> proofT) --> proofT) $ + Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf)) + end + | term_of Ts (AbsP (s, t, prf)) = + AbsPt $ the_default Term.dummy_prop t $ + Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf)) + | term_of Ts (prf1 %% prf2) = + AppPt $ term_of Ts prf1 $ term_of Ts prf2 + | term_of Ts (prf % opt) = + let + val t = the_default Term.dummy opt; + val T = fastype_of1 (Ts, t) handle TERM _ => dummyT; + in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end + | term_of _ (Hyp t) = Hypt $ t + | term_of _ (Oracle (_, t, _)) = Oraclet $ t + | term_of _ MinProof = MinProoft; + +in + +val term_of_proof = term_of []; + +end; + + +(* proof_of_term *) fun proof_of_term thy ty = let @@ -193,9 +248,33 @@ fun pretty_proof ctxt prf = Proof_Context.pretty_term_abbrev (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) - (Proofterm.term_of_proof prf); + (term_of_proof prf); fun pretty_standard_proof_of ctxt full thm = pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm); +fun pretty_proof_boxes_of ctxt full thm = + let + val thy = Proof_Context.theory_of ctxt; + val selection = + {included = Proofterm.this_id (Thm.derivation_id thm), + excluded = is_some o Global_Theory.lookup_thm_id thy} + in + Proofterm.proof_boxes selection [Thm.proof_of thm] + |> map (fn ({serial = i, pos, prop, ...}, proof) => + let + val proof' = proof + |> full ? Proofterm.reconstruct_proof thy prop + |> Proofterm.forall_intr_variables prop; + val prop' = prop + |> Proofterm.forall_intr_variables_term; + val name = Long_Name.append "thm" (string_of_int i); + in + Pretty.item + [Pretty.str (name ^ Position.here_list pos ^ ":"), Pretty.brk 1, + Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof'] + end) + |> Pretty.chunks + end; + end; diff -r a7a52ba0717d -r 6178ecf357a0 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Thu Oct 31 09:02:02 2019 +0000 +++ b/src/Pure/Thy/export_theory.ML Fri Nov 01 18:43:37 2019 +0100 @@ -248,18 +248,19 @@ (* theorems and proof terms *) - val export_standard_proofs = Options.default_bool @{system_option export_standard_proofs}; - val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; val lookup_thm_id = Global_Theory.lookup_thm_id thy; - fun proof_boxes_of thm thm_id = + fun proof_boxes thm thm_id = let - val dep_boxes = - thm |> Thm_Deps.proof_boxes (fn thm_id' => - if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id')); - in dep_boxes @ [thm_id] end; + val selection = + {included = Proofterm.this_id (SOME thm_id), + excluded = is_some o lookup_thm_id}; + val boxes = + map (Proofterm.thm_header_id o #1) (Proofterm.proof_boxes selection [Thm.proof_of thm]) + handle Proofterm.MIN_PROOF () => Thm_Deps.thm_boxes selection [thm] + in boxes @ [thm_id] end; fun expand_name thm_id (header: Proofterm.thm_header) = if #serial header = #serial thm_id then "" @@ -279,16 +280,18 @@ let val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); val thm = clean_thm (Thm.unconstrainT raw_thm); - val boxes = proof_boxes_of thm thm_id; + val boxes = proof_boxes thm thm_id; val proof0 = - if export_standard_proofs then + if Proofterm.export_standard_enabled () then Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof; val (prop, SOME proof) = standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0); - val _ = Proofterm.commit_proof proof; + val _ = + if Proofterm.export_proof_boxes_required thy + then Proofterm.export_proof_boxes [proof] else (); in (prop, (deps, (boxes, proof))) |> let diff -r a7a52ba0717d -r 6178ecf357a0 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Thu Oct 31 09:02:02 2019 +0000 +++ b/src/Pure/global_theory.ML Fri Nov 01 18:43:37 2019 +0100 @@ -288,10 +288,17 @@ fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy); fun apply_facts name_flags1 name_flags2 (b, facts) thy = - if Binding.is_empty b then app_facts facts thy |-> register_proofs + if Binding.is_empty b then + let + val (thms, thy') = app_facts facts thy; + val _ = + if Proofterm.export_proof_boxes_required thy' then + Proofterm.export_proof_boxes (map Thm.proof_of thms) + else (); + in register_proofs thms thy' end else let - val name_pos= bind_name thy b; + val name_pos = bind_name thy b; val (thms', thy') = thy |> app_facts (map (apfst (name_thms name_flags1 name_pos)) facts) |>> name_thms name_flags2 name_pos |-> register_proofs; diff -r a7a52ba0717d -r 6178ecf357a0 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Oct 31 09:02:02 2019 +0000 +++ b/src/Pure/proofterm.ML Fri Nov 01 18:43:37 2019 +0100 @@ -31,6 +31,7 @@ proof: proof} type oracle = string * term option type thm = serial * thm_node + exception MIN_PROOF of unit val proof_of: proof_body -> proof val join_proof: proof_body future -> proof val map_proof_of: (proof -> proof) -> proof_body -> proof_body @@ -102,8 +103,6 @@ val prf_subst_bounds: term list -> proof -> proof val prf_subst_pbounds: proof list -> proof -> proof val freeze_thaw_prf: proof -> proof * (proof -> proof) - val proofT: typ - val term_of_proof: proof -> term (*proof terms for specific inference rules*) val trivial_proof: proof @@ -152,6 +151,8 @@ val add_prf_rrule: proof * proof -> theory -> theory val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory val set_preproc: (theory -> proof -> proof) -> theory -> theory + val forall_intr_variables_term: term -> term + val forall_intr_variables: term -> proof -> proof val no_skel: proof val normal_skel: proof val rewrite_proof: theory -> (proof * proof) list * @@ -172,8 +173,10 @@ val add_standard_vars_term: term -> (string * typ) list -> (string * typ) list val export_enabled: unit -> bool + val export_standard_enabled: unit -> bool + val export_proof_boxes_required: theory -> bool + val export_proof_boxes: proof list -> unit val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body - val commit_proof: proof -> unit val thm_proof: theory -> (class * class -> proof) -> (string * class list list * class -> proof) -> string * Position.T -> sort list -> term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof @@ -188,6 +191,9 @@ val thm_header_id: thm_header -> thm_id val thm_id: thm -> thm_id val get_id: sort list -> term list -> term -> proof -> thm_id option + val this_id: thm_id option -> thm_id -> bool + val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} -> + proof list -> (thm_header * proof) list (*exception MIN_PROOF*) end structure Proofterm : PROOFTERM = @@ -228,6 +234,8 @@ val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i); +exception MIN_PROOF of unit; + fun proof_of (PBody {proof, ...}) = proof; val join_proof = Future.join #> proof_of; @@ -827,58 +835,6 @@ -(** proof terms as pure terms **) - -val proofT = Type ("Pure.proof", []); - -local - -val AbsPt = Const ("Pure.AbsP", propT --> (proofT --> proofT) --> proofT); -val AppPt = Const ("Pure.AppP", proofT --> proofT --> proofT); -val Hypt = Const ("Pure.Hyp", propT --> proofT); -val Oraclet = Const ("Pure.Oracle", propT --> proofT); -val MinProoft = Const ("Pure.MinProof", proofT); - -fun AppT T prf = - Const ("Pure.Appt", proofT --> Term.itselfT T --> proofT) $ prf $ Logic.mk_type T; - -fun OfClasst (T, c) = - let val U = Term.itselfT T --> propT - in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end; - -fun term_of _ (PThm ({name, types = Ts, ...}, _)) = - fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT)) - | term_of _ (PAxm (name, _, Ts)) = - fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT)) - | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c)) - | term_of _ (PBound i) = Bound i - | term_of Ts (Abst (s, opT, prf)) = - let val T = the_default dummyT opT in - Const ("Pure.Abst", (T --> proofT) --> proofT) $ - Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf)) - end - | term_of Ts (AbsP (s, t, prf)) = - AbsPt $ the_default Term.dummy_prop t $ - Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf)) - | term_of Ts (prf1 %% prf2) = - AppPt $ term_of Ts prf1 $ term_of Ts prf2 - | term_of Ts (prf % opt) = - let - val t = the_default Term.dummy opt; - val T = fastype_of1 (Ts, t) handle TERM _ => dummyT; - in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end - | term_of _ (Hyp t) = Hypt $ t - | term_of _ (Oracle (_, t, _)) = Oraclet $ t - | term_of _ MinProof = MinProoft; - -in - -val term_of_proof = term_of []; - -end; - - - (** inference rules **) (* trivial implication *) @@ -1628,12 +1584,10 @@ (** reconstruction of partial proof terms **) -local +fun forall_intr_variables_term prop = fold_rev Logic.all (variables_of prop) prop; +fun forall_intr_variables prop prf = fold_rev forall_intr_proof' (variables_of prop) prf; -exception MIN_PROOF of unit; - -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; +local fun app_types shift prop Ts prf = let @@ -1759,7 +1713,7 @@ NONE => fold_map (mk_tvar o Type.sort_of_atyp) prop_types env | SOME Ts => (Ts, env)); val prop' = subst_atomic_types (prop_types ~~ Ts) - (forall_intr_vfs prop) handle ListPair.UnequalLengths => + (forall_intr_variables_term prop) handle ListPair.UnequalLengths => error ("Wrong number of type arguments for " ^ quote (guess_name prf)) in (prop', change_types (SOME Ts) prf, [], env', vTs) end; @@ -1919,7 +1873,7 @@ in thawf (norm_proof env' prf) end handle MIN_PROOF () => MinProof; fun prop_of_atom prop Ts = - subst_atomic_types (type_variables_of prop ~~ Ts) (forall_intr_vfs prop); + subst_atomic_types (type_variables_of prop ~~ Ts) (forall_intr_variables_term prop); val head_norm = Envir.head_norm Envir.init; @@ -1978,7 +1932,7 @@ val prf1 = thm_body_proof_open thm_body |> reconstruct_proof thy prop - |> forall_intr_vfs_prf prop; + |> forall_intr_variables prop; val (seen1, maxidx1, prf2) = expand_init seen prf1 val seen2 = seen1 |> Inttab.update (serial, (maxidx1, prf2)); in (seen2, maxidx1, prf2) end @@ -2136,23 +2090,29 @@ (* PThm nodes *) fun export_enabled () = Options.default_bool "export_proofs"; +fun export_standard_enabled () = Options.default_bool "export_standard_proofs"; -fun commit_proof proof = +fun export_proof_boxes_required thy = + Context.theory_name thy = Context.PureN orelse + (export_enabled () andalso not (export_standard_enabled ())); + +fun export_proof_boxes proofs = let fun export_boxes (AbsP (_, _, prf)) = export_boxes prf | export_boxes (Abst (_, _, prf)) = export_boxes prf | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2 | export_boxes (prf % _) = export_boxes prf - | export_boxes (PThm ({serial = i, name = "", ...}, thm_body)) = + | export_boxes (PThm ({serial = i, ...}, thm_body)) = (fn boxes => if Inttab.defined boxes i then boxes else let - val prf = thm_body_proof_raw thm_body; - val boxes' = Inttab.update (i, thm_body_export_proof thm_body) boxes; - in export_boxes prf boxes' end) + val prf' = thm_body_proof_raw thm_body; + val export = thm_body_export_proof thm_body; + val boxes' = boxes |> not (Lazy.is_finished export) ? Inttab.update (i, export); + in export_boxes prf' boxes' end) | export_boxes _ = I; - val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest; + val boxes = (proofs, Inttab.empty) |-> fold export_boxes |> Inttab.dest; in List.app (Lazy.force o #2) boxes end; local @@ -2203,7 +2163,7 @@ fun export thy i prop prf = if export_enabled () then let - val _ = commit_proof prf; + val _ = export_proof_boxes [prf]; val _ = export_proof thy i prop prf; in () end else (); @@ -2320,6 +2280,33 @@ | SOME {name = "", ...} => NONE | SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name))); +fun this_id NONE _ = false + | this_id (SOME (thm_id: thm_id)) (thm_id': thm_id) = #serial thm_id = #serial thm_id'; + + +(* proof boxes: intermediate PThm nodes *) + +fun proof_boxes {included, excluded} proofs = + let + fun boxes_of (Abst (_, _, prf)) = boxes_of prf + | boxes_of (AbsP (_, _, prf)) = boxes_of prf + | boxes_of (prf % _) = boxes_of prf + | boxes_of (prf1 %% prf2) = boxes_of prf1 #> boxes_of prf2 + | boxes_of (PThm (header as {serial = i, ...}, thm_body)) = + (fn boxes => + let val thm_id = thm_header_id header in + if Inttab.defined boxes i orelse (excluded thm_id andalso not (included thm_id)) + then boxes + else + let + val prf' = thm_body_proof_open thm_body; + val boxes' = Inttab.update (i, (header, prf')) boxes; + in boxes_of prf' boxes' end + end) + | boxes_of MinProof = raise MIN_PROOF () + | boxes_of _ = I; + in Inttab.fold_rev (cons o #2) (fold boxes_of proofs Inttab.empty) [] end; + end; structure Basic_Proofterm = diff -r a7a52ba0717d -r 6178ecf357a0 src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Thu Oct 31 09:02:02 2019 +0000 +++ b/src/Pure/thm_deps.ML Fri Nov 01 18:43:37 2019 +0100 @@ -12,7 +12,8 @@ val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list val pretty_thm_deps: theory -> thm list -> Pretty.T - val proof_boxes: (Proofterm.thm_id -> bool) -> thm -> Proofterm.thm_id list + val thm_boxes: {included: Proofterm.thm_id -> bool, excluded: Proofterm.thm_id -> bool} -> + thm list -> Proofterm.thm_id list val unused_thms_cmd: theory list * theory list -> (string * thm) list end; @@ -80,18 +81,19 @@ in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; -(* proof boxes: undefined PThm nodes *) +(* thm boxes: intermediate PThm nodes *) -fun proof_boxes defined thm = +fun thm_boxes {included, excluded} thms = let fun boxes (i, thm_node) res = let val thm_id = Proofterm.thm_id (i, thm_node) in - if defined thm_id orelse Inttab.defined res i then res + if Inttab.defined res i orelse (excluded thm_id andalso not (included thm_id)) + then res else Inttab.update (i, thm_id) res |> fold boxes (Proofterm.thm_node_thms thm_node) end; - in Inttab.fold_rev (cons o #2) (fold boxes (Thm.thm_deps thm) Inttab.empty) [] end; + in Inttab.fold_rev (cons o #2) (fold (fold boxes o Thm.thm_deps) thms Inttab.empty) [] end; (* unused_thms_cmd *)