# HG changeset patch # User bulwahn # Date 1274286249 -7200 # Node ID 1166704995300fef5606f3ba9261f571e3dceed4 # Parent 25fdef26b460ede499dd52f1ff66617bb3bdb433 changing operations for accessing data to work with contexts diff -r 25fdef26b460 -r 116670499530 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed May 19 18:24:08 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed May 19 18:24:09 2010 +0200 @@ -26,7 +26,7 @@ val modes_of: compilation -> Proof.context -> string -> mode list val all_modes_of : compilation -> Proof.context -> (string * mode list) list val all_random_modes_of : Proof.context -> (string * mode list) list - val intros_of : theory -> string -> thm list + val intros_of : Proof.context -> string -> thm list val add_intro : thm -> theory -> theory val set_elim : thm -> theory -> theory val register_alternative_function : string -> mode -> string -> theory -> theory @@ -39,7 +39,7 @@ val force_modes_and_compilations : string -> (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory val preprocess_intro : theory -> thm -> thm - val print_stored_rules : theory -> unit + val print_stored_rules : Proof.context -> unit val print_all_modes : compilation -> Proof.context -> unit val mk_casesrule : Proof.context -> term -> thm list -> term val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref @@ -230,27 +230,27 @@ (* queries *) -fun lookup_pred_data thy name = - Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name) +fun lookup_pred_data ctxt name = + Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name) -fun the_pred_data thy name = case lookup_pred_data thy name +fun the_pred_data ctxt name = case lookup_pred_data ctxt name of NONE => error ("No such predicate " ^ quote name) | SOME data => data; -val is_registered = is_some oo lookup_pred_data o ProofContext.theory_of +val is_registered = is_some oo lookup_pred_data val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of -fun intros_of thy = #intros o the_pred_data thy +val intros_of = #intros oo the_pred_data -fun the_elim_of thy name = case #elim (the_pred_data thy name) +fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name) of NONE => error ("No elimination rule for predicate " ^ quote name) - | SOME thm => Thm.transfer thy thm + | SOME thm => thm -val has_elim = is_some o #elim oo the_pred_data; +val has_elim = is_some o #elim oo the_pred_data fun function_names_of compilation ctxt name = - case AList.lookup (op =) (#function_names (the_pred_data (ProofContext.theory_of ctxt) name)) compilation of + case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of NONE => error ("No " ^ string_of_compilation compilation ^ "functions defined for predicate " ^ quote name) | SOME fun_names => fun_names @@ -270,30 +270,30 @@ val all_random_modes_of = all_modes_of Random -fun defined_functions compilation ctxt name = case lookup_pred_data (ProofContext.theory_of ctxt) name of +fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of NONE => false | SOME data => AList.defined (op =) (#function_names data) compilation fun needs_random ctxt s m = - member (op =) (#needs_random (the_pred_data (ProofContext.theory_of ctxt) s)) m + member (op =) (#needs_random (the_pred_data ctxt s)) m -fun lookup_predfun_data thy name mode = +fun lookup_predfun_data ctxt name mode = Option.map rep_predfun_data - (AList.lookup (op =) (#predfun_data (the_pred_data thy name)) mode) + (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode) -fun the_predfun_data thy name mode = - case lookup_predfun_data thy name mode of +fun the_predfun_data ctxt name mode = + case lookup_predfun_data ctxt name mode of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name) | SOME data => data; -val predfun_definition_of = #definition ooo the_predfun_data o ProofContext.theory_of +val predfun_definition_of = #definition ooo the_predfun_data -val predfun_intro_of = #intro ooo the_predfun_data o ProofContext.theory_of +val predfun_intro_of = #intro ooo the_predfun_data -val predfun_elim_of = #elim ooo the_predfun_data o ProofContext.theory_of +val predfun_elim_of = #elim ooo the_predfun_data -val predfun_neg_intro_of = #neg_intro ooo the_predfun_data o ProofContext.theory_of +val predfun_neg_intro_of = #neg_intro ooo the_predfun_data (* diagnostic display functions *) @@ -331,17 +331,17 @@ print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt) else K () -fun print_stored_rules thy = +fun print_stored_rules ctxt = let - val preds = (Graph.keys o PredData.get) thy + val preds = Graph.keys (PredData.get (ProofContext.theory_of ctxt)) fun print pred () = let val _ = writeln ("predicate: " ^ pred) val _ = writeln ("introrules: ") - val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm)) - (rev (intros_of thy pred)) () + val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm)) + (rev (intros_of ctxt pred)) () in - if (has_elim thy pred) then - writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred)) + if (has_elim ctxt pred) then + writeln ("elimrule: " ^ Display.string_of_thm ctxt (the_elim_of ctxt pred)) else writeln ("no elimrule defined") end @@ -613,21 +613,21 @@ val no_compilation = ([], ([], [])) -fun fetch_pred_data thy name = - case try (Inductive.the_inductive (ProofContext.init_global thy)) name of +fun fetch_pred_data ctxt name = + case try (Inductive.the_inductive ctxt) name of SOME (info as (_, result)) => let fun is_intro_of intro = let val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) - in (fst (dest_Const const) = name) end; + in (fst (dest_Const const) = name) end; + val thy = ProofContext.theory_of ctxt val intros = (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result))) val index = find_index (fn s => s = name) (#names (fst info)) val pre_elim = nth (#elims result) index val pred = nth (#preds result) index val nparams = length (Inductive.params_of (#raw_induct result)) - val ctxt = ProofContext.init_global thy val elim_t = mk_casesrule ctxt pred intros val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t @@ -2409,10 +2409,9 @@ fun prove_one_direction options ctxt clauses preds pred mode moded_clauses = let - val thy = ProofContext.theory_of ctxt val T = the (AList.lookup (op =) preds pred) val nargs = length (binder_types T) - val pred_case_rule = the_elim_of thy pred + val pred_case_rule = the_elim_of ctxt pred in REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})) THEN print_tac options "before applying elim rule" @@ -2519,7 +2518,7 @@ fun prove_clause2 options ctxt pred mode (ts, ps) i = let - val pred_intro_rule = nth (intros_of (ProofContext.theory_of ctxt) pred) (i - 1) + val pred_intro_rule = nth (intros_of ctxt pred) (i - 1) val (in_ts, clause_out_ts) = split_mode mode ts; fun prove_prems2 out_ts [] = print_tac options "before prove_match2 - last call:" @@ -2762,9 +2761,8 @@ (* create code equation *) -fun add_code_equations thy preds result_thmss = +fun add_code_equations ctxt preds result_thmss = let - val ctxt = ProofContext.init_global thy fun add_code_equation (predname, T) (pred, result_thms) = let val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool @@ -2801,7 +2799,7 @@ define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory, prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table, - add_code_equations : theory -> (string * typ) list + add_code_equations : Proof.context -> (string * typ) list -> (string * thm list) list -> (string * thm list) list, comp_modifiers : Comp_Mod.comp_modifiers, use_random : bool, @@ -2812,6 +2810,7 @@ let fun dest_steps (Steps s) = s val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps)) + val ctxt = ProofContext.init_global thy val _ = print_step options ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation ^ ") for predicates " ^ commas prednames ^ "...") @@ -2819,10 +2818,10 @@ (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) val _ = if show_intermediate_results options then - tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames))) + tracing (commas (map (Display.string_of_thm ctxt) (maps (intros_of ctxt) prednames))) else () val (preds, all_vs, param_vs, all_modes, clauses) = - prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames) + prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames) val _ = print_step options "Infering modes..." val ((moded_clauses, errors), thy') = Output.cond_timeit true "Infering modes" @@ -2848,7 +2847,7 @@ val result_thms = Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ => #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) - val result_thms' = #add_code_equations (dest_steps steps) thy'' preds + val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds (maps_modes result_thms) val qname = #qname (dest_steps steps) val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute @@ -2883,7 +2882,7 @@ val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps))) val ctxt = ProofContext.init_global thy val thy' = thy - |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of ctxt)) names) + |> PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names) |> Theory.checkpoint; fun strong_conn_of gr keys = Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) @@ -3036,14 +3035,15 @@ val const = prep_const thy raw_const val ctxt = ProofContext.init_global thy val lthy' = Local_Theory.theory (PredData.map - (extend (fetch_pred_data thy) (depending_preds_of ctxt) const)) lthy + (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy val thy' = ProofContext.theory_of lthy' - val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy') + val ctxt' = ProofContext.init_global thy' + val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt') fun mk_cases const = let val T = Sign.the_const_type thy const val pred = Const (const, T) - val intros = intros_of thy' const + val intros = intros_of ctxt' const in mk_casesrule lthy' pred intros end val cases_rules = map mk_cases preds val cases = diff -r 25fdef26b460 -r 116670499530 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed May 19 18:24:08 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed May 19 18:24:09 2010 +0200 @@ -253,8 +253,9 @@ fun obtain_specification_graph options thy t = let + val ctxt = ProofContext.init_global thy fun is_nondefining_const (c, T) = member (op =) logic_operator_names c - fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of thy) c + fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of ctxt) c fun case_consts (c, T) = is_some (Datatype.info_of_case thy c) fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T)) fun defiants_of specs = diff -r 25fdef26b460 -r 116670499530 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed May 19 18:24:08 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed May 19 18:24:09 2010 +0200 @@ -181,7 +181,7 @@ if member (op =) ((map fst specs) @ black_list) pred_name then thy else - (case try (Predicate_Compile_Core.intros_of thy) pred_name of + (case try (Predicate_Compile_Core.intros_of (ProofContext.init_global thy)) pred_name of NONE => thy | SOME [] => thy | SOME intros =>