clarified context, notably for internal use of Simplifier;
authorwenzelm
Mon May 09 14:37:47 2016 +0200 (2016-05-09 ago)
changeset 63073413184c7a2a2
parent 63071 3ca3bc795908
child 63074 c60730295599
clarified context, notably for internal use of Simplifier;
src/Doc/more_antiquote.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/record.ML
src/Pure/Isar/code.ML
src/Pure/axclass.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Doc/more_antiquote.ML	Wed May 04 10:19:01 2016 +0200
     1.2 +++ b/src/Doc/more_antiquote.ML	Mon May 09 14:37:47 2016 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4        |> snd
     1.5        |> these
     1.6        |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
     1.7 -      |> map (holize o no_vars ctxt o Axclass.overload thy);
     1.8 +      |> map (holize o no_vars ctxt o Axclass.overload ctxt);
     1.9    in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt source thms) end;
    1.10  
    1.11  in
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Wed May 04 10:19:01 2016 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon May 09 14:37:47 2016 +0200
     2.3 @@ -23,11 +23,11 @@
     2.4  val reflN = "refl"
     2.5  val simpsN = "simps"
     2.6  
     2.7 -fun mk_case_certificate thy raw_thms =
     2.8 +fun mk_case_certificate ctxt raw_thms =
     2.9    let
    2.10      val thms as thm1 :: _ = raw_thms
    2.11        |> Conjunction.intr_balanced
    2.12 -      |> Thm.unvarify_global thy
    2.13 +      |> Thm.unvarify_global (Proof_Context.theory_of ctxt)
    2.14        |> Conjunction.elim_balanced (length raw_thms)
    2.15        |> map Simpdata.mk_meta_eq
    2.16        |> map Drule.zero_var_indexes;
    2.17 @@ -36,14 +36,14 @@
    2.18        |> Thm.prop_of |> Logic.dest_equals |> fst |> Term.strip_comb
    2.19        ||> fst o split_last |> list_comb;
    2.20      val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
    2.21 -    val assum = Thm.global_cterm_of thy (Logic.mk_equals (lhs, rhs));
    2.22 +    val assum = Thm.cterm_of ctxt (Logic.mk_equals (lhs, rhs));
    2.23    in
    2.24      thms
    2.25      |> Conjunction.intr_balanced
    2.26 -    |> rewrite_rule (Proof_Context.init_global thy) [Thm.symmetric (Thm.assume assum)]
    2.27 +    |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
    2.28      |> Thm.implies_intr assum
    2.29      |> Thm.generalize ([], params) 0
    2.30 -    |> Axclass.unoverload thy
    2.31 +    |> Axclass.unoverload ctxt
    2.32      |> Thm.varifyT_global
    2.33    end;
    2.34  
    2.35 @@ -128,7 +128,7 @@
    2.36        thy
    2.37        |> Code.add_datatype ctrs
    2.38        |> fold_rev Code.add_default_eqn case_thms
    2.39 -      |> Code.add_case (mk_case_certificate thy case_thms)
    2.40 +      |> Code.add_case (mk_case_certificate (Proof_Context.init_global thy) case_thms)
    2.41        |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
    2.42          ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
    2.43      else
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed May 04 10:19:01 2016 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon May 09 14:37:47 2016 +0200
     3.3 @@ -112,7 +112,9 @@
     3.4        val intross5 = map_specs (map (remove_equalities thy2)) intross4
     3.5        val _ = print_intross options thy2 "After removing equality premises:" intross5
     3.6        val intross6 =
     3.7 -        map (fn (s, ths) => (overload_const thy2 s, map (Axclass.overload thy2) ths)) intross5
     3.8 +        map (fn (s, ths) =>
     3.9 +            (overload_const thy2 s, map (Axclass.overload (Proof_Context.init_global thy2)) ths))
    3.10 +          intross5
    3.11        val intross7 = map_specs (map (expand_tuples thy2)) intross6
    3.12        val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7
    3.13        val _ = (case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ()))
     4.1 --- a/src/HOL/Tools/record.ML	Wed May 04 10:19:01 2016 +0200
     4.2 +++ b/src/HOL/Tools/record.ML	Mon May 09 14:37:47 2016 +0200
     4.3 @@ -1764,14 +1764,14 @@
     4.4          Class.intro_classes_tac ctxt []
     4.5          THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
     4.6          THEN ALLGOALS (resolve_tac ctxt @{thms refl});
     4.7 -      fun mk_eq thy eq_def =
     4.8 -        rewrite_rule (Proof_Context.init_global thy)
     4.9 -          [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
    4.10 -      fun mk_eq_refl thy =
    4.11 +      fun mk_eq ctxt eq_def =
    4.12 +        rewrite_rule ctxt
    4.13 +          [Axclass.unoverload ctxt (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
    4.14 +      fun mk_eq_refl ctxt =
    4.15          @{thm equal_refl}
    4.16          |> Thm.instantiate
    4.17 -          ([((("'a", 0), @{sort equal}), Thm.global_ctyp_of thy (Logic.varifyT_global extT))], [])
    4.18 -        |> Axclass.unoverload thy;
    4.19 +          ([((("'a", 0), @{sort equal}), Thm.ctyp_of ctxt (Logic.varifyT_global extT))], [])
    4.20 +        |> Axclass.unoverload ctxt;
    4.21        val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
    4.22        val ensure_exhaustive_record =
    4.23          ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
    4.24 @@ -1785,8 +1785,10 @@
    4.25        |-> (fn (_, (_, eq_def)) =>
    4.26           Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
    4.27        |-> (fn eq_def => fn thy =>
    4.28 -            thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
    4.29 -      |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
    4.30 +            thy
    4.31 +            |> Code.del_eqn eq_def
    4.32 +            |> Code.add_default_eqn (mk_eq (Proof_Context.init_global thy) eq_def))
    4.33 +      |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl (Proof_Context.init_global thy)) thy)
    4.34        |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
    4.35        |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
    4.36      end
     5.1 --- a/src/Pure/Isar/code.ML	Wed May 04 10:19:01 2016 +0200
     5.2 +++ b/src/Pure/Isar/code.ML	Mon May 09 14:37:47 2016 +0200
     5.3 @@ -655,7 +655,7 @@
     5.4  
     5.5  fun check_abstype_cert thy proto_thm =
     5.6    let
     5.7 -    val thm = (Axclass.unoverload thy o meta_rewrite thy) proto_thm;
     5.8 +    val thm = (Axclass.unoverload (Proof_Context.init_global thy) o meta_rewrite thy) proto_thm;
     5.9      val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
    5.10        handle TERM _ => bad_thm "Not an equation"
    5.11             | THM _ => bad_thm "Not a proper equation";
    5.12 @@ -888,12 +888,15 @@
    5.13  fun pretty_cert thy (cert as Nothing _) =
    5.14        [Pretty.str "(not implemented)"]
    5.15    | pretty_cert thy (cert as Equations _) =
    5.16 -      (map_filter (Option.map (Thm.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
    5.17 +      (map_filter
    5.18 +        (Option.map (Thm.pretty_thm_global thy o
    5.19 +            Axclass.overload (Proof_Context.init_global thy)) o fst o snd)
    5.20           o these o snd o equations_of_cert thy) cert
    5.21    | pretty_cert thy (Projection (t, _)) =
    5.22        [Syntax.pretty_term_global thy (Logic.varify_types_global t)]
    5.23    | pretty_cert thy (Abstract (abs_thm, _)) =
    5.24 -      [(Thm.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
    5.25 +      [(Thm.pretty_thm_global thy o
    5.26 +         Axclass.overload (Proof_Context.init_global thy) o Thm.varifyT_global) abs_thm];
    5.27  
    5.28  end;
    5.29  
    5.30 @@ -916,13 +919,9 @@
    5.31    singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt)
    5.32  
    5.33  fun preprocess conv ctxt =
    5.34 -  let
    5.35 -    val thy = Proof_Context.theory_of ctxt;
    5.36 -  in
    5.37 -    Thm.transfer thy
    5.38 -    #> rewrite_eqn conv ctxt
    5.39 -    #> Axclass.unoverload thy
    5.40 -  end;
    5.41 +  Thm.transfer (Proof_Context.theory_of ctxt)
    5.42 +  #> rewrite_eqn conv ctxt
    5.43 +  #> Axclass.unoverload ctxt;
    5.44  
    5.45  fun cert_of_eqns_preprocess ctxt functrans c =
    5.46    let
     6.1 --- a/src/Pure/axclass.ML	Wed May 04 10:19:01 2016 +0200
     6.2 +++ b/src/Pure/axclass.ML	Mon May 09 14:37:47 2016 +0200
     6.3 @@ -14,10 +14,10 @@
     6.4    val thynames_of_arity: theory -> string * class -> string list
     6.5    val param_of_inst: theory -> string * string -> string
     6.6    val inst_of_param: theory -> string -> (string * string) option
     6.7 -  val unoverload: theory -> thm -> thm
     6.8 -  val overload: theory -> thm -> thm
     6.9 -  val unoverload_conv: theory -> conv
    6.10 -  val overload_conv: theory -> conv
    6.11 +  val unoverload: Proof.context -> thm -> thm
    6.12 +  val overload: Proof.context -> thm -> thm
    6.13 +  val unoverload_conv: Proof.context -> conv
    6.14 +  val overload_conv: Proof.context -> conv
    6.15    val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
    6.16    val unoverload_const: theory -> string * typ -> string
    6.17    val cert_classrel: theory -> class * class -> class * class
    6.18 @@ -284,22 +284,17 @@
    6.19  val inst_of_param = Symtab.lookup o #2 o inst_params_of;
    6.20  val param_of_inst = #1 oo get_inst_param;
    6.21  
    6.22 -fun inst_thms thy =
    6.23 -  Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) [];
    6.24 +fun inst_thms ctxt =
    6.25 +  Symtab.fold
    6.26 +    (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of (Proof_Context.theory_of ctxt))) [];
    6.27  
    6.28  fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
    6.29  
    6.30 -fun unoverload thy =
    6.31 -  rewrite_rule (Proof_Context.init_global thy) (inst_thms thy);
    6.32 -
    6.33 -fun overload thy =
    6.34 -  rewrite_rule (Proof_Context.init_global thy) (map Thm.symmetric (inst_thms thy));
    6.35 +fun unoverload ctxt = rewrite_rule ctxt (inst_thms ctxt);
    6.36 +fun overload ctxt = rewrite_rule ctxt (map Thm.symmetric (inst_thms ctxt));
    6.37  
    6.38 -fun unoverload_conv thy =
    6.39 -  Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (inst_thms thy);
    6.40 -
    6.41 -fun overload_conv thy =
    6.42 -  Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (map Thm.symmetric (inst_thms thy));
    6.43 +fun unoverload_conv ctxt = Raw_Simplifier.rewrite ctxt true (inst_thms ctxt);
    6.44 +fun overload_conv ctxt = Raw_Simplifier.rewrite ctxt true (map Thm.symmetric (inst_thms ctxt));
    6.45  
    6.46  fun lookup_inst_param consts params (c, T) =
    6.47    (case get_inst_tyco consts (c, T) of
     7.1 --- a/src/Tools/Code/code_preproc.ML	Wed May 04 10:19:01 2016 +0200
     7.2 +++ b/src/Tools/Code/code_preproc.ML	Mon May 09 14:37:47 2016 +0200
     7.3 @@ -205,9 +205,9 @@
     7.4      val post = (#post o the_thmproc) thy;
     7.5      fun pre_conv ctxt' =
     7.6        Simplifier.rewrite (put_simpset pre ctxt')
     7.7 -      #> trans_conv_rule (Axclass.unoverload_conv (Proof_Context.theory_of ctxt'))
     7.8 +      #> trans_conv_rule (Axclass.unoverload_conv ctxt')
     7.9      fun post_conv ctxt' =
    7.10 -      Axclass.overload_conv (Proof_Context.theory_of ctxt')
    7.11 +      Axclass.overload_conv ctxt'
    7.12        #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt'))
    7.13    in fn ctxt' => pre_conv ctxt' #> pair (post_conv ctxt') end;
    7.14  
     8.1 --- a/src/Tools/Code/code_thingol.ML	Wed May 04 10:19:01 2016 +0200
     8.2 +++ b/src/Tools/Code/code_thingol.ML	Mon May 09 14:37:47 2016 +0200
     8.3 @@ -574,7 +574,7 @@
     8.4        let
     8.5          val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
     8.6          val dom_length = length (fst (strip_type ty))
     8.7 -        val thm = Axclass.unoverload_conv thy (Thm.cterm_of ctxt raw_const);
     8.8 +        val thm = Axclass.unoverload_conv ctxt (Thm.cterm_of ctxt raw_const);
     8.9          val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
    8.10            o Logic.dest_equals o Thm.prop_of) thm;
    8.11        in