1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed May 19 18:24:08 2010 +0200
1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed May 19 18:24:09 2010 +0200
1.3 @@ -26,7 +26,7 @@
1.4 val modes_of: compilation -> Proof.context -> string -> mode list
1.5 val all_modes_of : compilation -> Proof.context -> (string * mode list) list
1.6 val all_random_modes_of : Proof.context -> (string * mode list) list
1.7 - val intros_of : theory -> string -> thm list
1.8 + val intros_of : Proof.context -> string -> thm list
1.9 val add_intro : thm -> theory -> theory
1.10 val set_elim : thm -> theory -> theory
1.11 val register_alternative_function : string -> mode -> string -> theory -> theory
1.12 @@ -39,7 +39,7 @@
1.13 val force_modes_and_compilations : string ->
1.14 (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
1.15 val preprocess_intro : theory -> thm -> thm
1.16 - val print_stored_rules : theory -> unit
1.17 + val print_stored_rules : Proof.context -> unit
1.18 val print_all_modes : compilation -> Proof.context -> unit
1.19 val mk_casesrule : Proof.context -> term -> thm list -> term
1.20 val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
1.21 @@ -230,27 +230,27 @@
1.22
1.23 (* queries *)
1.24
1.25 -fun lookup_pred_data thy name =
1.26 - Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name)
1.27 +fun lookup_pred_data ctxt name =
1.28 + Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name)
1.29
1.30 -fun the_pred_data thy name = case lookup_pred_data thy name
1.31 +fun the_pred_data ctxt name = case lookup_pred_data ctxt name
1.32 of NONE => error ("No such predicate " ^ quote name)
1.33 | SOME data => data;
1.34
1.35 -val is_registered = is_some oo lookup_pred_data o ProofContext.theory_of
1.36 +val is_registered = is_some oo lookup_pred_data
1.37
1.38 val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
1.39
1.40 -fun intros_of thy = #intros o the_pred_data thy
1.41 +val intros_of = #intros oo the_pred_data
1.42
1.43 -fun the_elim_of thy name = case #elim (the_pred_data thy name)
1.44 +fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
1.45 of NONE => error ("No elimination rule for predicate " ^ quote name)
1.46 - | SOME thm => Thm.transfer thy thm
1.47 + | SOME thm => thm
1.48
1.49 -val has_elim = is_some o #elim oo the_pred_data;
1.50 +val has_elim = is_some o #elim oo the_pred_data
1.51
1.52 fun function_names_of compilation ctxt name =
1.53 - case AList.lookup (op =) (#function_names (the_pred_data (ProofContext.theory_of ctxt) name)) compilation of
1.54 + case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
1.55 NONE => error ("No " ^ string_of_compilation compilation
1.56 ^ "functions defined for predicate " ^ quote name)
1.57 | SOME fun_names => fun_names
1.58 @@ -270,30 +270,30 @@
1.59
1.60 val all_random_modes_of = all_modes_of Random
1.61
1.62 -fun defined_functions compilation ctxt name = case lookup_pred_data (ProofContext.theory_of ctxt) name of
1.63 +fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
1.64 NONE => false
1.65 | SOME data => AList.defined (op =) (#function_names data) compilation
1.66
1.67 fun needs_random ctxt s m =
1.68 - member (op =) (#needs_random (the_pred_data (ProofContext.theory_of ctxt) s)) m
1.69 + member (op =) (#needs_random (the_pred_data ctxt s)) m
1.70
1.71 -fun lookup_predfun_data thy name mode =
1.72 +fun lookup_predfun_data ctxt name mode =
1.73 Option.map rep_predfun_data
1.74 - (AList.lookup (op =) (#predfun_data (the_pred_data thy name)) mode)
1.75 + (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)
1.76
1.77 -fun the_predfun_data thy name mode =
1.78 - case lookup_predfun_data thy name mode of
1.79 +fun the_predfun_data ctxt name mode =
1.80 + case lookup_predfun_data ctxt name mode of
1.81 NONE => error ("No function defined for mode " ^ string_of_mode mode ^
1.82 " of predicate " ^ name)
1.83 | SOME data => data;
1.84
1.85 -val predfun_definition_of = #definition ooo the_predfun_data o ProofContext.theory_of
1.86 +val predfun_definition_of = #definition ooo the_predfun_data
1.87
1.88 -val predfun_intro_of = #intro ooo the_predfun_data o ProofContext.theory_of
1.89 +val predfun_intro_of = #intro ooo the_predfun_data
1.90
1.91 -val predfun_elim_of = #elim ooo the_predfun_data o ProofContext.theory_of
1.92 +val predfun_elim_of = #elim ooo the_predfun_data
1.93
1.94 -val predfun_neg_intro_of = #neg_intro ooo the_predfun_data o ProofContext.theory_of
1.95 +val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
1.96
1.97 (* diagnostic display functions *)
1.98
1.99 @@ -331,17 +331,17 @@
1.100 print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt)
1.101 else K ()
1.102
1.103 -fun print_stored_rules thy =
1.104 +fun print_stored_rules ctxt =
1.105 let
1.106 - val preds = (Graph.keys o PredData.get) thy
1.107 + val preds = Graph.keys (PredData.get (ProofContext.theory_of ctxt))
1.108 fun print pred () = let
1.109 val _ = writeln ("predicate: " ^ pred)
1.110 val _ = writeln ("introrules: ")
1.111 - val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
1.112 - (rev (intros_of thy pred)) ()
1.113 + val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm))
1.114 + (rev (intros_of ctxt pred)) ()
1.115 in
1.116 - if (has_elim thy pred) then
1.117 - writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
1.118 + if (has_elim ctxt pred) then
1.119 + writeln ("elimrule: " ^ Display.string_of_thm ctxt (the_elim_of ctxt pred))
1.120 else
1.121 writeln ("no elimrule defined")
1.122 end
1.123 @@ -613,21 +613,21 @@
1.124
1.125 val no_compilation = ([], ([], []))
1.126
1.127 -fun fetch_pred_data thy name =
1.128 - case try (Inductive.the_inductive (ProofContext.init_global thy)) name of
1.129 +fun fetch_pred_data ctxt name =
1.130 + case try (Inductive.the_inductive ctxt) name of
1.131 SOME (info as (_, result)) =>
1.132 let
1.133 fun is_intro_of intro =
1.134 let
1.135 val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
1.136 - in (fst (dest_Const const) = name) end;
1.137 + in (fst (dest_Const const) = name) end;
1.138 + val thy = ProofContext.theory_of ctxt
1.139 val intros =
1.140 (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result)))
1.141 val index = find_index (fn s => s = name) (#names (fst info))
1.142 val pre_elim = nth (#elims result) index
1.143 val pred = nth (#preds result) index
1.144 val nparams = length (Inductive.params_of (#raw_induct result))
1.145 - val ctxt = ProofContext.init_global thy
1.146 val elim_t = mk_casesrule ctxt pred intros
1.147 val elim =
1.148 prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
1.149 @@ -2409,10 +2409,9 @@
1.150
1.151 fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
1.152 let
1.153 - val thy = ProofContext.theory_of ctxt
1.154 val T = the (AList.lookup (op =) preds pred)
1.155 val nargs = length (binder_types T)
1.156 - val pred_case_rule = the_elim_of thy pred
1.157 + val pred_case_rule = the_elim_of ctxt pred
1.158 in
1.159 REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
1.160 THEN print_tac options "before applying elim rule"
1.161 @@ -2519,7 +2518,7 @@
1.162
1.163 fun prove_clause2 options ctxt pred mode (ts, ps) i =
1.164 let
1.165 - val pred_intro_rule = nth (intros_of (ProofContext.theory_of ctxt) pred) (i - 1)
1.166 + val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
1.167 val (in_ts, clause_out_ts) = split_mode mode ts;
1.168 fun prove_prems2 out_ts [] =
1.169 print_tac options "before prove_match2 - last call:"
1.170 @@ -2762,9 +2761,8 @@
1.171
1.172 (* create code equation *)
1.173
1.174 -fun add_code_equations thy preds result_thmss =
1.175 +fun add_code_equations ctxt preds result_thmss =
1.176 let
1.177 - val ctxt = ProofContext.init_global thy
1.178 fun add_code_equation (predname, T) (pred, result_thms) =
1.179 let
1.180 val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
1.181 @@ -2801,7 +2799,7 @@
1.182 define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory,
1.183 prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list
1.184 -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
1.185 - add_code_equations : theory -> (string * typ) list
1.186 + add_code_equations : Proof.context -> (string * typ) list
1.187 -> (string * thm list) list -> (string * thm list) list,
1.188 comp_modifiers : Comp_Mod.comp_modifiers,
1.189 use_random : bool,
1.190 @@ -2812,6 +2810,7 @@
1.191 let
1.192 fun dest_steps (Steps s) = s
1.193 val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
1.194 + val ctxt = ProofContext.init_global thy
1.195 val _ = print_step options
1.196 ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation
1.197 ^ ") for predicates " ^ commas prednames ^ "...")
1.198 @@ -2819,10 +2818,10 @@
1.199 (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
1.200 val _ =
1.201 if show_intermediate_results options then
1.202 - tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
1.203 + tracing (commas (map (Display.string_of_thm ctxt) (maps (intros_of ctxt) prednames)))
1.204 else ()
1.205 val (preds, all_vs, param_vs, all_modes, clauses) =
1.206 - prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames)
1.207 + prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames)
1.208 val _ = print_step options "Infering modes..."
1.209 val ((moded_clauses, errors), thy') =
1.210 Output.cond_timeit true "Infering modes"
1.211 @@ -2848,7 +2847,7 @@
1.212 val result_thms =
1.213 Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
1.214 #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
1.215 - val result_thms' = #add_code_equations (dest_steps steps) thy'' preds
1.216 + val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
1.217 (maps_modes result_thms)
1.218 val qname = #qname (dest_steps steps)
1.219 val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
1.220 @@ -2883,7 +2882,7 @@
1.221 val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
1.222 val ctxt = ProofContext.init_global thy
1.223 val thy' = thy
1.224 - |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of ctxt)) names)
1.225 + |> PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names)
1.226 |> Theory.checkpoint;
1.227 fun strong_conn_of gr keys =
1.228 Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
1.229 @@ -3036,14 +3035,15 @@
1.230 val const = prep_const thy raw_const
1.231 val ctxt = ProofContext.init_global thy
1.232 val lthy' = Local_Theory.theory (PredData.map
1.233 - (extend (fetch_pred_data thy) (depending_preds_of ctxt) const)) lthy
1.234 + (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy
1.235 val thy' = ProofContext.theory_of lthy'
1.236 - val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy')
1.237 + val ctxt' = ProofContext.init_global thy'
1.238 + val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt')
1.239 fun mk_cases const =
1.240 let
1.241 val T = Sign.the_const_type thy const
1.242 val pred = Const (const, T)
1.243 - val intros = intros_of thy' const
1.244 + val intros = intros_of ctxt' const
1.245 in mk_casesrule lthy' pred intros end
1.246 val cases_rules = map mk_cases preds
1.247 val cases =
2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed May 19 18:24:08 2010 +0200
2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed May 19 18:24:09 2010 +0200
2.3 @@ -253,8 +253,9 @@
2.4
2.5 fun obtain_specification_graph options thy t =
2.6 let
2.7 + val ctxt = ProofContext.init_global thy
2.8 fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
2.9 - fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of thy) c
2.10 + fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of ctxt) c
2.11 fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
2.12 fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
2.13 fun defiants_of specs =
3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed May 19 18:24:08 2010 +0200
3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed May 19 18:24:09 2010 +0200
3.3 @@ -181,7 +181,7 @@
3.4 if member (op =) ((map fst specs) @ black_list) pred_name then
3.5 thy
3.6 else
3.7 - (case try (Predicate_Compile_Core.intros_of thy) pred_name of
3.8 + (case try (Predicate_Compile_Core.intros_of (ProofContext.init_global thy)) pred_name of
3.9 NONE => thy
3.10 | SOME [] => thy
3.11 | SOME intros =>