src/Pure/Proof/extraction.ML
changeset 62922 96691631c1eb
parent 61865 6dcc9e4f1aa6
child 62958 b41c1cb5e251
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Apr 09 12:36:25 2016 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Apr 09 13:28:32 2016 +0200
     1.3 @@ -164,13 +164,13 @@
     1.4      | _ => error "get_var_type: not a variable"
     1.5    end;
     1.6  
     1.7 -fun read_term thy T s =
     1.8 +fun read_term ctxt T s =
     1.9    let
    1.10 -    val ctxt = Proof_Context.init_global thy
    1.11 +    val ctxt' = ctxt
    1.12        |> Config.put Type_Infer_Context.const_sorts false
    1.13        |> Proof_Context.set_defsort [];
    1.14      val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    1.15 -  in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
    1.16 +  in parse ctxt' s |> Type.constraint T |> Syntax.check_term ctxt' end;
    1.17  
    1.18  
    1.19  (**** theory data ****)
    1.20 @@ -214,9 +214,9 @@
    1.21  );
    1.22  
    1.23  fun read_condeq thy =
    1.24 -  let val thy' = add_syntax thy
    1.25 +  let val ctxt' = Proof_Context.init_global (add_syntax thy)
    1.26    in fn s =>
    1.27 -    let val t = Logic.varify_global (read_term thy' propT s)
    1.28 +    let val t = Logic.varify_global (read_term ctxt' propT s)
    1.29      in
    1.30        (map Logic.dest_equals (Logic.strip_imp_prems t),
    1.31          Logic.dest_equals (Logic.strip_imp_concl t))
    1.32 @@ -314,6 +314,7 @@
    1.33      val rtypes = map fst types;
    1.34      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    1.35      val thy' = add_syntax thy;
    1.36 +    val ctxt' = Proof_Context.init_global thy';
    1.37      val rd = Proof_Syntax.read_proof thy' true false;
    1.38    in fn (thm, (vs, s1, s2)) =>
    1.39      let
    1.40 @@ -331,14 +332,14 @@
    1.41        val T = etype_of thy' vs [] prop;
    1.42        val (T', thw) = Type.legacy_freeze_thaw_type
    1.43          (if T = nullT then nullT else map fastype_of vars' ---> T);
    1.44 -      val t = map_types thw (read_term thy' T' s1);
    1.45 +      val t = map_types thw (read_term ctxt' T' s1);
    1.46        val r' = freeze_thaw (condrew thy' eqns
    1.47          (procs @ [typeof_proc [] vs, rlz_proc]))
    1.48            (Const ("realizes", T --> propT --> propT) $
    1.49              (if T = nullT then t else list_comb (t, vars')) $ prop);
    1.50        val r = Logic.list_implies (shyps,
    1.51          fold_rev Logic.all (map (get_var_type r') vars) r');
    1.52 -      val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
    1.53 +      val prf = Reconstruct.reconstruct_proof ctxt' r (rd s2);
    1.54      in (name, (vs, (t, prf))) end
    1.55    end;
    1.56  
    1.57 @@ -481,14 +482,16 @@
    1.58  fun extract thm_vss thy =
    1.59    let
    1.60      val thy' = add_syntax thy;
    1.61 +    val ctxt' = Proof_Context.init_global thy';
    1.62 +
    1.63      val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
    1.64        ExtractionData.get thy;
    1.65      val procs = maps (rev o fst o snd) types;
    1.66      val rtypes = map fst types;
    1.67      val typroc = typeof_proc [];
    1.68      val prep = the_default (K I) prep thy' o
    1.69 -      ProofRewriteRules.elim_defs thy' false (map (Thm.transfer thy) defs) o
    1.70 -      Reconstruct.expand_proof thy' (map (rpair NONE) ("" :: expand));
    1.71 +      ProofRewriteRules.elim_defs ctxt' false (map (Thm.transfer thy) defs) o
    1.72 +      Reconstruct.expand_proof ctxt' (map (rpair NONE) ("" :: expand));
    1.73      val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    1.74  
    1.75      fun find_inst prop Ts ts vs =
    1.76 @@ -511,7 +514,7 @@
    1.77        Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
    1.78  
    1.79      fun mk_sprfs cs tye = maps (fn (_, T) =>
    1.80 -      ProofRewriteRules.mk_of_sort_proof thy (map SOME cs)
    1.81 +      ProofRewriteRules.mk_of_sort_proof ctxt' (map SOME cs)
    1.82          (T, Sign.defaultS thy)) tye;
    1.83  
    1.84      fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
    1.85 @@ -612,7 +615,7 @@
    1.86                      val _ = msg d ("Building correctness proof for " ^ quote name ^
    1.87                        (if null vs' then ""
    1.88                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
    1.89 -                    val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
    1.90 +                    val prf' = prep (Reconstruct.reconstruct_proof ctxt' prop prf);
    1.91                      val (corr_prf0, defs'') = corr (d + 1) vs' [] [] []
    1.92                        (rev shyps) NONE prf' prf' defs';
    1.93                      val corr_prf = mkabsp shyps corr_prf0;
    1.94 @@ -636,7 +639,7 @@
    1.95              | SOME rs => (case find vs' rs of
    1.96                  SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
    1.97                | NONE => error ("corr: no realizer for instance of theorem " ^
    1.98 -                  quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
    1.99 +                  quote name ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
   1.100                      (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))))
   1.101            end
   1.102  
   1.103 @@ -651,7 +654,7 @@
   1.104                SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
   1.105                  defs)
   1.106              | NONE => error ("corr: no realizer for instance of axiom " ^
   1.107 -                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.108 +                quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
   1.109                    (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
   1.110            end
   1.111  
   1.112 @@ -704,7 +707,7 @@
   1.113                      val _ = msg d ("Extracting " ^ quote s ^
   1.114                        (if null vs' then ""
   1.115                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   1.116 -                    val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   1.117 +                    val prf' = prep (Reconstruct.reconstruct_proof ctxt' prop prf);
   1.118                      val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs;
   1.119                      val (corr_prf, defs'') = corr (d + 1) vs' [] [] []
   1.120                        (rev shyps) (SOME t) prf' prf' defs';
   1.121 @@ -752,7 +755,7 @@
   1.122              | SOME rs => (case find vs' rs of
   1.123                  SOME (t, _) => (subst_TVars tye' t, defs)
   1.124                | NONE => error ("extr: no realizer for instance of theorem " ^
   1.125 -                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.126 +                  quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
   1.127                      (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
   1.128            end
   1.129  
   1.130 @@ -764,7 +767,7 @@
   1.131              case find vs' (Symtab.lookup_list realizers s) of
   1.132                SOME (t, _) => (subst_TVars tye' t, defs)
   1.133              | NONE => error ("extr: no realizer for instance of axiom " ^
   1.134 -                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   1.135 +                quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
   1.136                    (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
   1.137            end
   1.138  
   1.139 @@ -779,7 +782,7 @@
   1.140          val _ = name <> "" orelse error "extraction: unnamed theorem";
   1.141          val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
   1.142            quote name ^ " has no computational content")
   1.143 -      in Reconstruct.reconstruct_proof thy prop prf end;
   1.144 +      in Reconstruct.reconstruct_proof ctxt' prop prf end;
   1.145  
   1.146      val defs =
   1.147        fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)