# HG changeset patch # User wenzelm # Date 1460201312 -7200 # Node ID 96691631c1ebaa1a25d9ef8e44791ba6447dcd16 # Parent 499a63c30d55a47db7418c04ff4784652701f37e clarified context; avoid Unsynchronized.ref; diff -r 499a63c30d55 -r 96691631c1eb src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Sat Apr 09 12:36:25 2016 +0200 +++ b/src/Doc/Implementation/Logic.thy Sat Apr 09 13:28:32 2016 +0200 @@ -1188,8 +1188,8 @@ @{index_ML_type proof_body} \\ @{index_ML proofs: "int Unsynchronized.ref"} \\ @{index_ML Reconstruct.reconstruct_proof: - "theory -> term -> proof -> proof"} \\ - @{index_ML Reconstruct.expand_proof: "theory -> + "Proof.context -> term -> proof -> proof"} \\ + @{index_ML Reconstruct.expand_proof: "Proof.context -> (string * term option) list -> proof -> proof"} \\ @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\ @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\ @@ -1221,7 +1221,7 @@ records full proof terms. Officially named theorems that contribute to a result are recorded in any case. - \<^descr> @{ML Reconstruct.reconstruct_proof}~\thy prop prf\ turns the implicit + \<^descr> @{ML Reconstruct.reconstruct_proof}~\ctxt prop prf\ turns the implicit proof term \prf\ into a full proof of the given proposition. Reconstruction may fail if \prf\ is not a proof of \prop\, or if it does not @@ -1229,7 +1229,7 @@ for proofs that are constructed manually, but not for those produced automatically by the inference kernel. - \<^descr> @{ML Reconstruct.expand_proof}~\thy [thm\<^sub>1, \, thm\<^sub>n] prf\ expands and + \<^descr> @{ML Reconstruct.expand_proof}~\ctxt [thm\<^sub>1, \, thm\<^sub>n] prf\ expands and reconstructs the proofs of all specified theorems, with the given (full) proof. Theorems that are not unique specified via their name may be disambiguated by giving their proposition. diff -r 499a63c30d55 -r 96691631c1eb src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Sat Apr 09 12:36:25 2016 +0200 +++ b/src/HOL/Extraction.thy Sat Apr 09 13:28:32 2016 +0200 @@ -16,12 +16,14 @@ Extraction.add_types [("bool", ([], NONE))] #> Extraction.set_preprocessor (fn thy => + let val ctxt = Proof_Context.init_global thy in Proofterm.rewrite_proof_notypes ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o Proofterm.rewrite_proof thy (RewriteHOLProof.rews, - ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o - ProofRewriteRules.elim_vars (curry Const @{const_name default})) + ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class ctxt]) o + ProofRewriteRules.elim_vars (curry Const @{const_name default}) + end) \ lemmas [extraction_expand] = diff -r 499a63c30d55 -r 96691631c1eb src/HOL/Proofs/ex/Proof_Terms.thy --- a/src/HOL/Proofs/ex/Proof_Terms.thy Sat Apr 09 12:36:25 2016 +0200 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy Sat Apr 09 13:28:32 2016 +0200 @@ -46,6 +46,7 @@ ML_val \ val thy = @{theory}; + val ctxt = @{context}; val prf = Proof_Syntax.read_proof thy true false "impI \ _ \ _ \ \ @@ -54,7 +55,7 @@ \ (\<^bold>\(H: _) Ha: _. conjI \ _ \ _ \ Ha \ H))"; val thm = prf - |> Reconstruct.reconstruct_proof thy @{prop "A \ B \ B \ A"} + |> Reconstruct.reconstruct_proof ctxt @{prop "A \ B \ B \ A"} |> Proof_Checker.thm_of_proof thy |> Drule.export_without_context; \ diff -r 499a63c30d55 -r 96691631c1eb src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy Sat Apr 09 12:36:25 2016 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Sat Apr 09 13:28:32 2016 +0200 @@ -12,15 +12,16 @@ subsection \Export and re-import of global proof terms\ ML \ - fun export_proof thy thm = + fun export_proof ctxt thm = let + val thy = Proof_Context.theory_of ctxt; val (_, prop) = Logic.unconstrainT (Thm.shyps_of thm) (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); val prf = Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |> - Reconstruct.reconstruct_proof thy prop |> - Reconstruct.expand_proof thy [("", NONE)] |> + Reconstruct.reconstruct_proof ctxt prop |> + Reconstruct.expand_proof ctxt [("", NONE)] |> Proofterm.rew_proof thy |> Proofterm.no_thm_proofs; in Proofterm.encode prf end; @@ -40,24 +41,24 @@ lemma ex: "A \ A" .. ML_val \ - val xml = export_proof @{theory} @{thm ex}; + val xml = export_proof @{context} @{thm ex}; val thm = import_proof thy1 xml; \ ML_val \ - val xml = export_proof @{theory} @{thm de_Morgan}; + val xml = export_proof @{context} @{thm de_Morgan}; val thm = import_proof thy1 xml; \ ML_val \ - val xml = export_proof @{theory} @{thm Drinker's_Principle}; + val xml = export_proof @{context} @{thm Drinker's_Principle}; val thm = import_proof thy1 xml; \ text \Some fairly large proof:\ ML_val \ - val xml = export_proof @{theory} @{thm abs_less_iff}; + val xml = export_proof @{context} @{thm abs_less_iff}; val thm = import_proof thy1 xml; @{assert} (size (YXML.string_of_body xml) > 1000000); \ diff -r 499a63c30d55 -r 96691631c1eb src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Sat Apr 09 12:36:25 2016 +0200 +++ b/src/HOL/Tools/datatype_realizer.ML Sat Apr 09 13:28:32 2016 +0200 @@ -129,6 +129,7 @@ |> Global_Theory.store_thm (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm) ||> Sign.restore_naming thy; + val ctxt' = Proof_Context.init_global thy'; val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []); val rvs = rev (Thm.fold_terms Term.add_vars thm' []); @@ -147,7 +148,7 @@ | _ => AbsP ("H", SOME p, prf))) (rec_fns ~~ Thm.prems_of thm) (Proofterm.proof_combP - (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0)))); + (Reconstruct.proof_of ctxt' thm', map PBound (length prems - 1 downto 0)))); val r' = if null is then r @@ -203,6 +204,7 @@ |> Sign.root_path |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm) ||> Sign.restore_naming thy; + val ctxt' = Proof_Context.init_global thy'; val P = Var (("P", 0), rT' --> HOLogic.boolT); val prf = @@ -212,10 +214,10 @@ (AbsP ("H", SOME (Logic.varify_global p), prf))) (prems ~~ rs) (Proofterm.proof_combP - (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0)))); + (Reconstruct.proof_of ctxt' thm', map PBound (length prems - 1 downto 0)))); val prf' = Extraction.abs_corr_shyps thy' exhaust [] - (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of thy' exhaust); + (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of ctxt' exhaust); val r' = Logic.varify_global (Abs ("y", T, (fold_rev (Term.abs o dest_Free) rs diff -r 499a63c30d55 -r 96691631c1eb src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sat Apr 09 12:36:25 2016 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Sat Apr 09 13:28:32 2016 +0200 @@ -19,9 +19,9 @@ [name] => name | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm])); -fun prf_of thy thm = - Reconstruct.proof_of thy thm - |> Reconstruct.expand_proof thy [("", NONE)]; (* FIXME *) +fun prf_of ctxt thm = + Reconstruct.proof_of ctxt thm + |> Reconstruct.expand_proof ctxt [("", NONE)]; (* FIXME *) fun subsets [] = [[]] | subsets (x::xs) = @@ -257,6 +257,7 @@ fun mk_realizer thy vs (name, rule, rrule, rlz, rt) = let + val ctxt = Proof_Context.init_global thy; val rvs = map fst (relevant_vars (Thm.prop_of rule)); val xs = rev (Term.add_vars (Thm.prop_of rule) []); val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs); @@ -268,7 +269,7 @@ if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt, Extraction.abs_corr_shyps thy rule vs vs2 (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz) - (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule))))) + (fold_rev Proofterm.forall_intr_proof' rs (prf_of ctxt rrule))))) end; fun rename tab = map (fn x => the_default x (AList.lookup op = tab x)); diff -r 499a63c30d55 -r 96691631c1eb src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Apr 09 12:36:25 2016 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sat Apr 09 13:28:32 2016 +0200 @@ -250,13 +250,12 @@ NONE => let val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state); - val thy = Proof_Context.theory_of ctxt; val prf = Thm.proof_of thm; val prop = Thm.full_prop_of thm; val prf' = Proofterm.rewrite_proof_notypes ([], []) prf; in Proof_Syntax.pretty_proof ctxt - (if full then Reconstruct.reconstruct_proof thy prop prf' else prf') + (if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf') end | SOME srcs => let val ctxt = Toplevel.context_of state diff -r 499a63c30d55 -r 96691631c1eb src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Sat Apr 09 12:36:25 2016 +0200 +++ b/src/Pure/Proof/extraction.ML Sat Apr 09 13:28:32 2016 +0200 @@ -164,13 +164,13 @@ | _ => error "get_var_type: not a variable" end; -fun read_term thy T s = +fun read_term ctxt T s = let - val ctxt = Proof_Context.init_global thy + val ctxt' = ctxt |> Config.put Type_Infer_Context.const_sorts false |> Proof_Context.set_defsort []; val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term; - in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end; + in parse ctxt' s |> Type.constraint T |> Syntax.check_term ctxt' end; (**** theory data ****) @@ -214,9 +214,9 @@ ); fun read_condeq thy = - let val thy' = add_syntax thy + let val ctxt' = Proof_Context.init_global (add_syntax thy) in fn s => - let val t = Logic.varify_global (read_term thy' propT s) + let val t = Logic.varify_global (read_term ctxt' propT s) in (map Logic.dest_equals (Logic.strip_imp_prems t), Logic.dest_equals (Logic.strip_imp_concl t)) @@ -314,6 +314,7 @@ val rtypes = map fst types; val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); val thy' = add_syntax thy; + val ctxt' = Proof_Context.init_global thy'; val rd = Proof_Syntax.read_proof thy' true false; in fn (thm, (vs, s1, s2)) => let @@ -331,14 +332,14 @@ val T = etype_of thy' vs [] prop; val (T', thw) = Type.legacy_freeze_thaw_type (if T = nullT then nullT else map fastype_of vars' ---> T); - val t = map_types thw (read_term thy' T' s1); + val t = map_types thw (read_term ctxt' T' s1); val r' = freeze_thaw (condrew thy' eqns (procs @ [typeof_proc [] vs, rlz_proc])) (Const ("realizes", T --> propT --> propT) $ (if T = nullT then t else list_comb (t, vars')) $ prop); val r = Logic.list_implies (shyps, fold_rev Logic.all (map (get_var_type r') vars) r'); - val prf = Reconstruct.reconstruct_proof thy' r (rd s2); + val prf = Reconstruct.reconstruct_proof ctxt' r (rd s2); in (name, (vs, (t, prf))) end end; @@ -481,14 +482,16 @@ fun extract thm_vss thy = let val thy' = add_syntax thy; + val ctxt' = Proof_Context.init_global thy'; + val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} = ExtractionData.get thy; val procs = maps (rev o fst o snd) types; val rtypes = map fst types; val typroc = typeof_proc []; val prep = the_default (K I) prep thy' o - ProofRewriteRules.elim_defs thy' false (map (Thm.transfer thy) defs) o - Reconstruct.expand_proof thy' (map (rpair NONE) ("" :: expand)); + ProofRewriteRules.elim_defs ctxt' false (map (Thm.transfer thy) defs) o + Reconstruct.expand_proof ctxt' (map (rpair NONE) ("" :: expand)); val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); fun find_inst prop Ts ts vs = @@ -511,7 +514,7 @@ Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye; fun mk_sprfs cs tye = maps (fn (_, T) => - ProofRewriteRules.mk_of_sort_proof thy (map SOME cs) + ProofRewriteRules.mk_of_sort_proof ctxt' (map SOME cs) (T, Sign.defaultS thy)) tye; fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst); @@ -612,7 +615,7 @@ val _ = msg d ("Building correctness proof for " ^ quote name ^ (if null vs' then "" else " (relevant variables: " ^ commas_quote vs' ^ ")")); - val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf); + val prf' = prep (Reconstruct.reconstruct_proof ctxt' prop prf); val (corr_prf0, defs'') = corr (d + 1) vs' [] [] [] (rev shyps) NONE prf' prf' defs'; val corr_prf = mkabsp shyps corr_prf0; @@ -636,7 +639,7 @@ | SOME rs => (case find vs' rs of SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs') | NONE => error ("corr: no realizer for instance of theorem " ^ - quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm + quote name ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))) end @@ -651,7 +654,7 @@ SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye), defs) | NONE => error ("corr: no realizer for instance of axiom " ^ - quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm + quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))) end @@ -704,7 +707,7 @@ val _ = msg d ("Extracting " ^ quote s ^ (if null vs' then "" else " (relevant variables: " ^ commas_quote vs' ^ ")")); - val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf); + val prf' = prep (Reconstruct.reconstruct_proof ctxt' prop prf); val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs; val (corr_prf, defs'') = corr (d + 1) vs' [] [] [] (rev shyps) (SOME t) prf' prf' defs'; @@ -752,7 +755,7 @@ | SOME rs => (case find vs' rs of SOME (t, _) => (subst_TVars tye' t, defs) | NONE => error ("extr: no realizer for instance of theorem " ^ - quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm + quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))) end @@ -764,7 +767,7 @@ case find vs' (Symtab.lookup_list realizers s) of SOME (t, _) => (subst_TVars tye' t, defs) | NONE => error ("extr: no realizer for instance of axiom " ^ - quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm + quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))) end @@ -779,7 +782,7 @@ val _ = name <> "" orelse error "extraction: unnamed theorem"; val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^ quote name ^ " has no computational content") - in Reconstruct.reconstruct_proof thy prop prf end; + in Reconstruct.reconstruct_proof ctxt' prop prf end; val defs = fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm) diff -r 499a63c30d55 -r 96691631c1eb src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Sat Apr 09 12:36:25 2016 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Sat Apr 09 13:28:32 2016 +0200 @@ -10,12 +10,12 @@ val rprocs : bool -> (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof - val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof + val elim_defs : Proof.context -> bool -> thm list -> Proofterm.proof -> Proofterm.proof val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof - val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list - val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof -> + val mk_of_sort_proof : Proof.context -> term option list -> typ * sort -> Proofterm.proof list + val expand_of_class : Proof.context -> typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option end; @@ -250,7 +250,7 @@ | (_, []) => (prf, false) | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false)); -fun elim_defs thy r defs prf = +fun elim_defs ctxt r defs prf = let val defs' = map (Logic.dest_equals o map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs; @@ -265,9 +265,9 @@ then I else cons (name, SOME prop) | _ => I) [prf] []; - in Reconstruct.expand_proof thy thms end; + in Reconstruct.expand_proof ctxt thms end; in - rewrite_terms (Pattern.rewrite_term thy defs' []) + rewrite_terms (Pattern.rewrite_term (Proof_Context.theory_of ctxt) defs' []) (fst (insert_refl defnames [] (f prf))) end; @@ -340,7 +340,7 @@ (**** expand OfClass proofs ****) -fun mk_of_sort_proof thy hs (T, S) = +fun mk_of_sort_proof ctxt hs (T, S) = let val hs' = map (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE) @@ -354,18 +354,19 @@ ~1 => error "expand_of_class: missing class hypothesis" | i => PBound i; fun reconstruct prf prop = prf |> - Reconstruct.reconstruct_proof thy prop |> - Reconstruct.expand_proof thy [("", NONE)] |> + Reconstruct.reconstruct_proof ctxt prop |> + Reconstruct.expand_proof ctxt [("", NONE)] |> Same.commit (Proofterm.map_proof_same Same.same Same.same hyp) in map2 reconstruct - (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S)) + (Proofterm.of_sort_proof (Proof_Context.theory_of ctxt) + (OfClass o apfst Type.strip_sorts) (subst T, S)) (Logic.mk_of_sort (T, S)) end; -fun expand_of_class thy Ts hs (OfClass (T, c)) = - mk_of_sort_proof thy hs (T, [c]) |> +fun expand_of_class ctxt Ts hs (OfClass (T, c)) = + mk_of_sort_proof ctxt hs (T, [c]) |> hd |> rpair Proofterm.no_skel |> SOME - | expand_of_class thy Ts hs _ = NONE; + | expand_of_class ctxt Ts hs _ = NONE; end; diff -r 499a63c30d55 -r 96691631c1eb src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sat Apr 09 12:36:25 2016 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Sat Apr 09 13:28:32 2016 +0200 @@ -14,7 +14,7 @@ val read_term: theory -> bool -> typ -> string -> term val read_proof: theory -> bool -> bool -> string -> Proofterm.proof val proof_syntax: Proofterm.proof -> theory -> theory - val proof_of: theory -> bool -> thm -> Proofterm.proof + val proof_of: Proof.context -> bool -> thm -> Proofterm.proof val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T end; @@ -239,9 +239,9 @@ (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) end; -fun proof_of thy full raw_thm = +fun proof_of ctxt full raw_thm = let - val thm = Thm.transfer thy raw_thm; + val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm; val prop = Thm.full_prop_of thm; val prf = Thm.proof_of thm; val prf' = @@ -249,7 +249,7 @@ (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then Proofterm.join_proof body else prf | _ => prf) - in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end; + in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end; fun pretty_proof ctxt prf = Proof_Context.pretty_term_abbrev @@ -257,6 +257,6 @@ (term_of_proof prf); fun pretty_proof_of ctxt full th = - pretty_proof ctxt (proof_of (Proof_Context.theory_of ctxt) full th); + pretty_proof ctxt (proof_of ctxt full th); end; diff -r 499a63c30d55 -r 96691631c1eb src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Sat Apr 09 12:36:25 2016 +0200 +++ b/src/Pure/Proof/reconstruct.ML Sat Apr 09 13:28:32 2016 +0200 @@ -6,20 +6,23 @@ signature RECONSTRUCT = sig - val quiet_mode : bool Unsynchronized.ref - val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof + val quiet_mode : bool Config.T + val reconstruct_proof : Proof.context -> term -> Proofterm.proof -> Proofterm.proof val prop_of' : term list -> Proofterm.proof -> term val prop_of : Proofterm.proof -> term - val proof_of : theory -> thm -> Proofterm.proof - val expand_proof : theory -> (string * term option) list -> + val proof_of : Proof.context -> thm -> Proofterm.proof + val expand_proof : Proof.context -> (string * term option) list -> Proofterm.proof -> Proofterm.proof end; structure Reconstruct : RECONSTRUCT = struct -val quiet_mode = Unsynchronized.ref true; -fun message s = if !quiet_mode then () else writeln s; +val quiet_mode = + Config.bool (Config.declare ("Reconstruct.quiet_mode", @{here}) (K (Config.Bool true))); + +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 [])); @@ -43,10 +46,10 @@ val mk_abs = fold (fn T => fn u => Abs ("", T, u)); -fun unifyT thy env T U = +fun unifyT ctxt env T U = let val Envir.Envir {maxidx, tenv, tyenv} = env; - val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx); + val (tyenv', maxidx') = Sign.typ_unify (Proof_Context.theory_of ctxt) (T, U) (tyenv, maxidx); in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end; fun chaseT env (T as TVar v) = @@ -55,9 +58,9 @@ | SOME T' => chaseT env T') | chaseT _ T = T; -fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) Ts vTs +fun infer_type ctxt (env as Envir.Envir {maxidx, tenv, tyenv}) Ts vTs (t as Const (s, T)) = if T = dummyT then - (case Sign.const_type thy s of + (case Sign.const_type (Proof_Context.theory_of ctxt) s of NONE => error ("reconstruct_proof: No such constant: " ^ quote s) | SOME T => let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) @@ -65,68 +68,69 @@ Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}) end) else (t, T, vTs, env) - | infer_type thy env Ts vTs (t as Free (s, T)) = + | infer_type ctxt env Ts vTs (t as Free (s, T)) = if T = dummyT then (case Symtab.lookup vTs s of NONE => let val (T, env') = mk_tvar [] env in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end | SOME T => (Free (s, T), T, vTs, env)) else (t, T, vTs, env) - | infer_type thy env Ts vTs (Var _) = error "reconstruct_proof: internal error" - | infer_type thy env Ts vTs (Abs (s, T, t)) = + | infer_type ctxt env Ts vTs (Var _) = error "reconstruct_proof: internal error" + | infer_type ctxt env Ts vTs (Abs (s, T, t)) = let val (T', env') = if T = dummyT then mk_tvar [] env else (T, env); - val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t + val (t', U, vTs', env'') = infer_type ctxt env' (T' :: Ts) vTs t in (Abs (s, T', t'), T' --> U, vTs', env'') end - | infer_type thy env Ts vTs (t $ u) = + | infer_type ctxt env Ts vTs (t $ u) = let - val (t', T, vTs1, env1) = infer_type thy env Ts vTs t; - val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u; + val (t', T, vTs1, env1) = infer_type ctxt env Ts vTs t; + val (u', U, vTs2, env2) = infer_type ctxt env1 Ts vTs1 u; in (case chaseT env2 T of - Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') + Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT ctxt env2 U U') | _ => let val (V, env3) = mk_tvar [] env2 - in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) + in (t' $ u', V, vTs2, unifyT ctxt env3 T (U --> V)) end) end - | infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env) + | infer_type ctxt env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env) handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i)); -fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^ - Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u); +fun cantunify ctxt (t, u) = + error ("Non-unifiable terms:\n" ^ + Syntax.string_of_term ctxt t ^ "\n\n" ^ Syntax.string_of_term ctxt u); -fun decompose thy Ts (p as (t, u)) env = +fun decompose ctxt Ts (p as (t, u)) env = let fun rigrig (a, T) (b, U) uT ts us = - if a <> b then cantunify thy p - else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U)) + if a <> b then cantunify ctxt p + else apfst flat (fold_map (decompose ctxt Ts) (ts ~~ us) (uT env T U)) in case apply2 (strip_comb o Envir.head_norm env) p of - ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us - | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us + ((Const c, ts), (Const d, us)) => rigrig c d (unifyT ctxt) ts us + | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT ctxt) ts us | ((Bound i, ts), (Bound j, us)) => rigrig (i, dummyT) (j, dummyT) (K o K) ts us | ((Abs (_, T, t), []), (Abs (_, U, u), [])) => - decompose thy (T::Ts) (t, u) (unifyT thy env T U) + decompose ctxt (T::Ts) (t, u) (unifyT ctxt env T U) | ((Abs (_, T, t), []), _) => - decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env + decompose ctxt (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env | (_, (Abs (_, T, u), [])) => - decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env + decompose ctxt (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env | _ => ([(mk_abs Ts t, mk_abs Ts u)], env) end; -fun make_constraints_cprf thy env cprf = +fun make_constraints_cprf ctxt env cprf = let fun add_cnstrt Ts prop prf cs env vTs (t, u) = let val t' = mk_abs Ts t; val u' = mk_abs Ts u in - (prop, prf, cs, Pattern.unify (Context.Theory thy) (t', u') env, vTs) + (prop, prf, cs, Pattern.unify (Context.Proof ctxt) (t', u') env, vTs) handle Pattern.Pattern => - let val (cs', env') = decompose thy [] (t', u') env + let val (cs', env') = decompose ctxt [] (t', u') env in (prop, prf, cs @ cs', env', vTs) end | Pattern.Unif => - cantunify thy (Envir.norm_term env t', Envir.norm_term env u') + cantunify ctxt (Envir.norm_term env t', Envir.norm_term env u') end; fun mk_cnstrts_atom env vTs prop opTs prf = @@ -155,12 +159,13 @@ | SOME T => (T, env)); val (t, prf, cnstrts, env'', vTs') = mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; - in (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), - cnstrts, env'', vTs') + in + (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), + cnstrts, env'', vTs') end | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) = let - val (t', _, vTs', env') = infer_type thy env Ts vTs t; + val (t', _, vTs', env') = infer_type ctxt env Ts vTs t; val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf; in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'') end @@ -183,11 +188,11 @@ end) end | mk_cnstrts env Ts Hs vTs (cprf % SOME t) = - let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t + let val (t', U, vTs1, env1) = infer_type ctxt env Ts vTs t in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, prf, cnstrts, env2, vTs2) => - let val env3 = unifyT thy env2 T U + let val env3 = unifyT ctxt env2 T U in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) end | (u, prf, cnstrts, env2, vTs2) => @@ -250,12 +255,11 @@ (**** solution of constraints ****) fun solve _ [] bigenv = bigenv - | solve thy cs bigenv = + | solve ctxt cs bigenv = let fun search env [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => - Thm.pretty_flexpair (Syntax.init_pretty_global thy) - (apply2 (Envir.norm_term bigenv) p)) cs))) + Thm.pretty_flexpair ctxt (apply2 (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then let @@ -263,10 +267,10 @@ val tn2 = Envir.norm_term bigenv t2 in if Pattern.pattern tn1 andalso Pattern.pattern tn2 then - (Pattern.unify (Context.Theory thy) (tn1, tn2) env, ps) handle Pattern.Unif => - cantunify thy (tn1, tn2) + (Pattern.unify (Context.Proof ctxt) (tn1, tn2) env, ps) handle Pattern.Unif => + cantunify ctxt (tn1, tn2) else - let val (cs', env') = decompose thy [] (tn1, tn2) env + let val (cs', env') = decompose ctxt [] (tn1, tn2) env in if cs' = [(tn1, tn2)] then apsnd (cons (false, (tn1, tn2), vs)) (search env ps) else search env' (map (fn q => (true, q, vs)) cs' @ ps) @@ -276,23 +280,25 @@ val Envir.Envir {maxidx, ...} = bigenv; val (env, cs') = search (Envir.empty maxidx) cs; in - solve thy (upd_constrs env cs') (Envir.merge (bigenv, env)) + solve ctxt (upd_constrs env cs') (Envir.merge (bigenv, env)) end; (**** reconstruction of proofs ****) -fun reconstruct_proof thy prop cprf = +fun reconstruct_proof ctxt prop cprf = let val (cprf' % SOME prop', thawf) = Proofterm.freeze_thaw_prf (cprf % SOME prop); - val _ = message "Collecting constraints..."; - val (t, prf, cs, env, _) = make_constraints_cprf thy + val _ = message ctxt (fn _ => "Collecting constraints ..."); + val (t, prf, cs, env, _) = make_constraints_cprf ctxt (Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf'; val cs' = map (apply2 (Envir.norm_term env)) ((t, prop') :: cs) |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) []))); - val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ..."); - val env' = solve thy cs' env + val _ = + message ctxt + (fn () => "Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ..."); + val env' = solve ctxt cs' env in thawf (Proofterm.norm_proof env' prf) end; @@ -324,15 +330,15 @@ val prop_of' = Envir.beta_eta_contract oo prop_of0; val prop_of = prop_of' []; -fun proof_of thy raw_thm = - let val thm = Thm.transfer thy raw_thm - in reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm) end; +fun proof_of ctxt raw_thm = + let val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm + in reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end; (**** expand and reconstruct subproofs ****) -fun expand_proof thy thms prf = +fun expand_proof ctxt thms prf = let fun expand maxidx prfs (AbsP (s, t, prf)) = let val (maxidx', prfs', prf') = expand maxidx prfs prf @@ -359,10 +365,10 @@ NONE => let val _ = - message ("Reconstructing proof of " ^ a ^ "\n" ^ - Syntax.string_of_term_global thy prop); + message ctxt (fn () => + "Reconstructing proof of " ^ a ^ "\n" ^ Syntax.string_of_term ctxt prop); val prf' = forall_intr_vfs_prf prop - (reconstruct_proof thy prop (Proofterm.join_proof body)); + (reconstruct_proof ctxt prop (Proofterm.join_proof body)); val (maxidx', prfs', prf) = expand (Proofterm.maxidx_proof prf' ~1) prfs prf' in (maxidx' + maxidx + 1, Proofterm.incr_indexes (maxidx + 1) prf,