--- 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)
--- 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,