# HG changeset patch # User wenzelm # Date 1441375318 -7200 # Node ID dcfc2814485821d5d74ef685e71c7347fe9f1453 # Parent 86049d52155ce36ac891f1f2803fbc74430f9140 tuned -- do not open ML structures; diff -r 86049d52155c -r dcfc28144858 src/HOL/Tools/Predicate_Compile/mode_inference.ML --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Fri Sep 04 14:00:13 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Fri Sep 04 16:01:58 2015 +0200 @@ -53,7 +53,7 @@ struct open Predicate_Compile_Aux; -open Core_Data; + (* derivation trees for modes of premises *) @@ -317,7 +317,7 @@ fun is_functional t mode = case try (fst o dest_Const o fst o strip_comb) t of NONE => false - | SOME c => is_some (alternative_compilation_of ctxt c mode) + | SOME c => is_some (Core_Data.alternative_compilation_of ctxt c mode) in case (is_functional t1 (head_mode_of deriv1), is_functional t2 (head_mode_of deriv2)) of (true, true) => EQUAL diff -r 86049d52155c -r dcfc28144858 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 04 14:00:13 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 04 16:01:58 2015 +0200 @@ -72,7 +72,6 @@ type random_seed = Random_Engine.seed open Predicate_Compile_Aux; -open Core_Data; open Mode_Inference; open Predicate_Compile_Proof; @@ -126,18 +125,19 @@ fun print_stored_rules ctxt = let - val preds = Graph.keys (PredData.get (Proof_Context.theory_of ctxt)) - fun print pred () = let - val _ = writeln ("predicate: " ^ pred) - val _ = writeln ("introrules: ") - val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm)) - (rev (intros_of ctxt pred)) () - in - if (has_elim ctxt pred) then - writeln ("elimrule: " ^ Display.string_of_thm ctxt (the_elim_of ctxt pred)) - else - writeln ("no elimrule defined") - end + val preds = Graph.keys (Core_Data.PredData.get (Proof_Context.theory_of ctxt)) + fun print pred () = + let + val _ = writeln ("predicate: " ^ pred) + val _ = writeln ("introrules: ") + val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm)) + (rev (Core_Data.intros_of ctxt pred)) () + in + if Core_Data.has_elim ctxt pred then + writeln ("elimrule: " ^ Display.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred)) + else + writeln ("no elimrule defined") + end in fold print preds () end; @@ -151,7 +151,7 @@ val _ = writeln ("modes: " ^ (commas (map string_of_mode modes))) in u end in - fold print (all_modes_of compilation ctxt) () + fold print (Core_Data.all_modes_of compilation ctxt) () end (* validity checks *) @@ -670,10 +670,10 @@ SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t) | (_, Term Output) => NONE | (Const (name, T), Context mode) => - (case alternative_compilation_of ctxt name mode of + (case Core_Data.alternative_compilation_of ctxt name mode of SOME alt_comp => SOME (alt_comp compfuns T) | NONE => - SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers) + SOME (Const (Core_Data.function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt name mode, Comp_Mod.funT_of compilation_modifiers mode T))) | (Free (s, T), Context m) => @@ -1014,7 +1014,7 @@ foldr1 (mk_plus compfuns) cl_ts) end val fun_const = - Const (function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt s mode, funT) + Const (Core_Data.function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt s mode, funT) in HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation)) @@ -1132,7 +1132,7 @@ val mode_cname = create_constname_of_mode options thy "" name T mode val mode_cbasename = Long_Name.base_name mode_cname val funT = funT_of compfuns mode T - val (args, _) = fold_map (mk_args true) ((strip_fun_mode mode) ~~ (binder_types T)) [] + val (args, _) = fold_map (mk_args true) (strip_fun_mode mode ~~ binder_types T) [] fun strip_eval _ t = let val t' = strip_split_abs t @@ -1152,13 +1152,13 @@ create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T)) in thy' - |> set_function_name Pred name mode mode_cname - |> add_predfun_data name mode (definition, rules) + |> Core_Data.set_function_name Pred name mode mode_cname + |> Core_Data.add_predfun_data name mode (definition, rules) |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd end; in - thy |> defined_function_of Pred name |> fold create_definition modes + thy |> Core_Data.defined_function_of Pred name |> fold create_definition modes end; fun define_functions comp_modifiers _ options preds (name, modes) thy = @@ -1171,11 +1171,11 @@ val funT = Comp_Mod.funT_of comp_modifiers mode T in thy |> Sign.add_consts [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] - |> set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname + |> Core_Data.set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname end; in thy - |> defined_function_of (Comp_Mod.compilation comp_modifiers) name + |> Core_Data.defined_function_of (Comp_Mod.compilation comp_modifiers) name |> fold create_definition modes end; @@ -1220,7 +1220,7 @@ Syntax.string_of_term ctxt (c $ t)) | Sidecond t => Sidecond (c $ t)) | (Const (s, _), _) => - if is_registered ctxt s then Prem t else Sidecond t + if Core_Data.is_registered ctxt s then Prem t else Sidecond t | _ => Sidecond t) fun prepare_intrs options ctxt prednames intros = @@ -1334,18 +1334,18 @@ let val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool in - if member eq_mode (modes_of Pred ctxt predname) full_mode then + if member eq_mode (Core_Data.modes_of Pred ctxt predname) full_mode then let val Ts = binder_types T val arg_names = Name.variant_list [] (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) val args = map2 (curry Free) arg_names Ts - val predfun = Const (function_name_of Pred ctxt predname full_mode, + val predfun = Const (Core_Data.function_name_of Pred ctxt predname full_mode, Ts ---> Predicate_Comp_Funs.mk_monadT @{typ unit}) val rhs = @{term Predicate.holds} $ (list_comb (predfun, args)) val eq_term = HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs)) - val def = predfun_definition_of ctxt predname full_mode + val def = Core_Data.predfun_definition_of ctxt predname full_mode val tac = fn _ => Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1 val eq = Goal.prove ctxt arg_names [] eq_term tac @@ -1387,18 +1387,18 @@ (*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 ctxt) (maps (intros_of ctxt) prednames))) + tracing (commas (map (Display.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames))) else () val (preds, all_vs, param_vs, all_modes, clauses) = - prepare_intrs options ctxt prednames (maps (intros_of ctxt) prednames) + prepare_intrs options ctxt prednames (maps (Core_Data.intros_of ctxt) prednames) val _ = print_step options "Infering modes..." - val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt, - modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt) + val (lookup_mode, lookup_neg_mode, needs_random) = (Core_Data.modes_of compilation ctxt, + Core_Data.modes_of (negative_compilation_of compilation) ctxt, Core_Data.needs_random ctxt) val ((moded_clauses, needs_random), errors) = cond_timeit (Config.get ctxt Quickcheck.timing) "Infering modes" (fn _ => infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses) - val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy + val thy' = fold (fn (s, ms) => Core_Data.set_needs_random s ms) needs_random thy val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses val _ = check_expected_modes options preds modes val _ = check_proposed_modes options preds modes errors @@ -1435,12 +1435,12 @@ fun gen_add_equations steps options names thy = let fun dest_steps (Steps s) = s - val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps))) - val thy' = extend_intro_graph names thy; + val defined = Core_Data.defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps))) + val thy' = Core_Data.extend_intro_graph names thy; fun strong_conn_of gr keys = Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr) - val scc = strong_conn_of (PredData.get thy') names - val thy'' = fold preprocess_intros (flat scc) thy' + val scc = strong_conn_of (Core_Data.PredData.get thy') names + val thy'' = fold Core_Data.preprocess_intros (flat scc) thy' val thy''' = fold_rev (fn preds => fn thy => if not (forall (defined (Proof_Context.init_global thy)) preds) then @@ -1601,7 +1601,7 @@ fun attrib' f opt_case_name = Thm.declaration_attribute (fn thm => Context.mapping (f (opt_case_name, thm)) I); -val code_pred_intro_attrib = attrib' add_intro NONE; +val code_pred_intro_attrib = attrib' Core_Data.add_intro NONE; (*FIXME - Naming of auxiliary rules necessary? @@ -1616,8 +1616,9 @@ val _ = Theory.setup - (PredData.put (Graph.empty) #> - Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro) + (Core_Data.PredData.put (Graph.empty) #> + Attrib.setup @{binding code_pred_intro} + (Scan.lift (Scan.option Args.name) >> attrib' Core_Data.add_intro) "adding alternative introduction rules for code generation of inductive predicates") (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *) @@ -1626,15 +1627,16 @@ let val thy = Proof_Context.theory_of lthy val const = prep_const thy raw_const - val lthy' = Local_Theory.background_theory (extend_intro_graph [const]) lthy + val lthy' = Local_Theory.background_theory (Core_Data.extend_intro_graph [const]) lthy val thy' = Proof_Context.theory_of lthy' val ctxt' = Proof_Context.init_global thy' - val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt') + val preds = + Graph.all_succs (Core_Data.PredData.get thy') [const] |> filter_out (Core_Data.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 ctxt' const + val intros = Core_Data.intros_of ctxt' const in mk_casesrule lthy' pred intros end val cases_rules = map mk_cases preds val cases = @@ -1644,7 +1646,7 @@ assumes = ("that", tl (Logic.strip_imp_prems case_rule)) :: map_filter (fn (fact_name, fact) => Option.map (fn a => (a, [fact])) fact_name) - ((SOME "prems" :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule), + ((SOME "prems" :: Core_Data.names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule), binds = [], cases = []}) preds cases_rules val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases val lthy'' = lthy' @@ -1655,7 +1657,7 @@ val global_thms = Proof_Context.export goal_ctxt (Proof_Context.init_global (Proof_Context.theory_of goal_ctxt)) (map the_single thms) in - goal_ctxt |> Local_Theory.background_theory (fold set_elim global_thms #> + goal_ctxt |> Local_Theory.background_theory (fold Core_Data.set_elim global_thms #> ((case compilation options of Pred => add_equations | DSeq => add_dseq_equations @@ -1762,7 +1764,7 @@ (compilation, _) t_compr = let val compfuns = Comp_Mod.compfuns comp_modifiers - val all_modes_of = all_modes_of compilation + val all_modes_of = Core_Data.all_modes_of compilation val (((body, output), T_compr), output_names) = (case try dest_special_compr t_compr of SOME r => r @@ -1772,7 +1774,7 @@ (Const (name, T), all_args) => (Const (name, T), all_args) | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)) in - if defined_functions compilation ctxt name then + if Core_Data.defined_functions compilation ctxt name then let fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2) @@ -1878,7 +1880,6 @@ @{term natural_of_nat} $ (HOLogic.size_const T $ Bound 0)))) t else mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t - val thy = Proof_Context.theory_of ctxt val time_limit = seconds (Config.get ctxt values_timeout) val (ts, statistics) = (case compilation of diff -r 86049d52155c -r dcfc28144858 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 04 14:00:13 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 04 16:01:58 2015 +0200 @@ -12,14 +12,13 @@ -> (string * (term list * indprem list) list) list -> (string * typ) list -> string -> bool * mode -> (term list * (indprem * Mode_Inference.mode_derivation) list) list * term - -> Thm.thm + -> thm end; structure Predicate_Compile_Proof : PREDICATE_COMPILE_PROOF = struct open Predicate_Compile_Aux; -open Core_Data; open Mode_Inference; @@ -62,7 +61,7 @@ val f_tac = (case f of Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps - [@{thm eval_pred}, predfun_definition_of ctxt name mode, + [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode, @{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 | Free _ => @@ -88,7 +87,7 @@ (Const (name, _), args) => let val mode = head_mode_of deriv - val introrule = predfun_intro_of ctxt name mode + val introrule = Core_Data.predfun_intro_of ctxt name mode val param_derivations = param_derivations_of deriv val ho_args = ho_args_of mode args in @@ -170,12 +169,12 @@ fun preds_of t nameTs = (case strip_comb t of (Const (name, T), args) => - if is_registered ctxt name then (name, T) :: nameTs - else fold preds_of args nameTs + if Core_Data.is_registered ctxt name then (name, T) :: nameTs + else fold preds_of args nameTs | _ => nameTs) val preds = preds_of t [] val defs = map - (fn (pred, T) => predfun_definition_of ctxt pred + (fn (pred, T) => Core_Data.predfun_definition_of ctxt pred (all_input_of T)) preds in @@ -227,7 +226,7 @@ val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE) val neg_intro_rule = Option.map (fn name => - the (predfun_neg_intro_of ctxt name mode)) name + the (Core_Data.predfun_neg_intro_of ctxt name mode)) name val param_derivations = param_derivations_of deriv val params = ho_args_of mode args in @@ -278,11 +277,11 @@ let val T = the (AList.lookup (op =) preds pred) val nargs = length (binder_types T) - val pred_case_rule = the_elim_of ctxt pred + val pred_case_rule = Core_Data.the_elim_of ctxt pred in REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})) THEN trace_tac ctxt options "before applying elim rule" - THEN eresolve_tac ctxt [predfun_elim_of ctxt pred mode] 1 + THEN eresolve_tac ctxt [Core_Data.predfun_elim_of ctxt pred mode] 1 THEN eresolve_tac ctxt [pred_case_rule] 1 THEN trace_tac ctxt options "after applying elim rule" THEN (EVERY (map @@ -338,8 +337,8 @@ val f_tac = (case f of Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps - (@{thm eval_pred}::(predfun_definition_of ctxt name mode) - :: @{thm "Product_Type.split_conv"}::[])) 1 + [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode, + @{thm Product_Type.split_conv}]) 1 | Free _ => all_tac | _ => error "prove_param2: illegal parameter term") in @@ -360,7 +359,7 @@ eresolve_tac ctxt @{thms bindE} 1 THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))) THEN trace_tac ctxt options "prove_expr2-before" - THEN eresolve_tac ctxt [predfun_elim_of ctxt name mode] 1 + THEN eresolve_tac ctxt [Core_Data.predfun_elim_of ctxt name mode] 1 THEN trace_tac ctxt options "prove_expr2" THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)) THEN trace_tac ctxt options "finished prove_expr2" @@ -372,12 +371,12 @@ fun preds_of t nameTs = (case strip_comb t of (Const (name, T), args) => - if is_registered ctxt name then (name, T) :: nameTs - else fold preds_of args nameTs + if Core_Data.is_registered ctxt name then (name, T) :: nameTs + else fold preds_of args nameTs | _ => nameTs) val preds = preds_of t [] val defs = map - (fn (pred, T) => predfun_definition_of ctxt pred + (fn (pred, T) => Core_Data.predfun_definition_of ctxt pred (all_input_of T)) preds in @@ -389,7 +388,7 @@ fun prove_clause2 options ctxt pred mode (ts, ps) i = let - val pred_intro_rule = nth (intros_of ctxt pred) (i - 1) + val pred_intro_rule = nth (Core_Data.intros_of ctxt pred) (i - 1) val (in_ts, _) = split_mode mode ts; val split_simpset = put_simpset HOL_basic_ss' ctxt @@ -441,9 +440,9 @@ THEN eresolve_tac ctxt @{thms bindE} 1 THEN (if is_some name then full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps - [predfun_definition_of ctxt (the name) mode]) 1 + [Core_Data.predfun_definition_of ctxt (the name) mode]) 1 THEN eresolve_tac ctxt @{thms not_predE} 1 - THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1 + THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms not_False_eq_True}) 1 THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)) else eresolve_tac ctxt @{thms not_predE'} 1) @@ -478,7 +477,7 @@ in (DETERM (TRY (resolve_tac ctxt @{thms unit.induct} 1))) THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))) - THEN (resolve_tac ctxt [predfun_intro_of ctxt pred mode] 1) + THEN (resolve_tac ctxt [Core_Data.predfun_intro_of ctxt pred mode] 1) THEN (REPEAT_DETERM (resolve_tac ctxt @{thms refl} 2)) THEN ( if null moded_clauses then eresolve_tac ctxt @{thms botE} 1