(* Title: HOL/Tools/Predicate_Compile/predicate_compile_data.ML
Author: Lukas Bulwahn, TU Muenchen
Book-keeping datastructure for the predicate compiler.
*)
signature PREDICATE_COMPILE_DATA =
sig
type specification_table;
(*val make_const_spec_table : Predicate_Compile_Aux.options -> theory -> specification_table*)
val get_specification : theory -> term -> thm list
val obtain_specification_graph :
Predicate_Compile_Aux.options -> theory -> term -> thm list TermGraph.T
val normalize_equation : theory -> thm -> thm
end;
structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA =
struct
open Predicate_Compile_Aux;
structure Data = Theory_Data
(
type T =
{const_spec_table : thm list Symtab.table};
val empty =
{const_spec_table = Symtab.empty};
val extend = I;
fun merge
({const_spec_table = const_spec_table1},
{const_spec_table = const_spec_table2}) =
{const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
);
fun mk_data c = {const_spec_table = c}
fun map_data f {const_spec_table = c} = mk_data (f c)
type specification_table = thm list Symtab.table
fun defining_term_of_introrule_term t =
let
val _ $ u = Logic.strip_imp_concl t
in fst (strip_comb u) end
(*
in case pred of
Const (c, T) => c
| _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
end
*)
val defining_term_of_introrule = defining_term_of_introrule_term o prop_of
(*TODO*)
fun is_introlike_term t = true
val is_introlike = is_introlike_term o prop_of
fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
(case strip_comb u of
(Const (c, T), args) =>
if (length (binder_types T) = length args) then
true
else
raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
| _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
| check_equation_format_term t =
raise TERM ("check_equation_format_term failed: Not an equation", [t])
val check_equation_format = check_equation_format_term o prop_of
fun defining_term_of_equation_term (t as (Const ("==", _) $ u $ v)) = fst (strip_comb u)
| defining_term_of_equation_term t =
raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
val defining_term_of_equation = defining_term_of_equation_term o prop_of
fun defining_const_of_equation th =
case defining_term_of_equation th
of Const (c, _) => c
| _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th])
(* Normalizing equations *)
fun mk_meta_equation th =
case prop_of th of
Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
| _ => th
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
fun full_fun_cong_expand th =
let
val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
val i = length (binder_types (fastype_of f)) - length args
in funpow i (fn th => th RS meta_fun_cong) th end;
fun declare_names s xs ctxt =
let
val res = Name.names ctxt s xs
in (res, fold Name.declare (map fst res) ctxt) end
fun split_all_pairs thy th =
let
val ctxt = ProofContext.init thy
val ((_, [th']), ctxt') = Variable.import true [th] ctxt
val t = prop_of th'
val frees = Term.add_frees t []
val freenames = Term.add_free_names t []
val nctxt = Name.make_context freenames
fun mk_tuple_rewrites (x, T) nctxt =
let
val Ts = HOLogic.flatten_tupleT T
val (xTs, nctxt') = declare_names x Ts nctxt
val paths = HOLogic.flat_tupleT_paths T
in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
val t' = Pattern.rewrite_term thy rewr [] t
val tac = Skip_Proof.cheat_tac thy
val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
in
th'''
end;
fun normalize_equation thy th =
mk_meta_equation th
|> Predicate_Compile_Set.unfold_set_notation
|> full_fun_cong_expand
|> split_all_pairs thy
|> tap check_equation_format
fun inline_equations thy th =
let
val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init thy)
val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th
(*val _ = print_step options
("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*)
in
th'
end
(*
fun store_thm_in_table options ignore thy th=
let
val th = th
|> inline_equations options thy
|> Predicate_Compile_Set.unfold_set_notation
|> AxClass.unoverload thy
val (const, th) =
if is_equationlike th then
let
val eq = normalize_equation thy th
in
(defining_const_of_equation eq, eq)
end
else if is_introlike th then (defining_const_of_introrule th, th)
else error "store_thm: unexpected definition format"
in
if ignore const then I else Symtab.cons_list (const, th)
end
fun make_const_spec_table options thy =
let
fun store ignore f =
fold (store_thm_in_table options ignore thy)
(map (Thm.transfer thy) (f ))
val table = Symtab.empty
|> store (K false) Predicate_Compile_Alternative_Defs.get
val ignore = Symtab.defined table
in
table
|> store ignore (fn ctxt => maps
else [])
|> store ignore Nitpick_Simps.get
|> store ignore Nitpick_Intros.get
end
fun get_specification table constname =
case Symtab.lookup table constname of
SOME thms => thms
| NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
*)
fun get_specification thy t =
Output.cond_timeit true "get_specification" (fn () =>
let
val ctxt = ProofContext.init thy
fun filtering th =
if is_equationlike th andalso
defining_const_of_equation (normalize_equation thy th) = (fst (dest_Const t)) then
SOME (normalize_equation thy th)
else
if is_introlike th andalso defining_term_of_introrule th = t then
SOME th
else
NONE
in
case map_filter filtering (map (Thm.transfer thy) (Predicate_Compile_Alternative_Defs.get ctxt))
of [] => (case Spec_Rules.retrieve ctxt t
of [] => rev (map_filter filtering (map (Thm.transfer thy) (Nitpick_Intros.get ctxt)))
| ((_, (_, ths)) :: _) => map (normalize_equation thy o Thm.transfer thy) ths)
| ths => rev ths
end)
val logic_operator_names =
[@{const_name "=="},
@{const_name "==>"},
@{const_name "Trueprop"},
@{const_name "Not"},
@{const_name "op ="},
@{const_name "op -->"},
@{const_name "All"},
@{const_name "Ex"},
@{const_name "op &"}]
fun special_cases (c, T) = member (op =) [
@{const_name Product_Type.Unity},
@{const_name False},
@{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
@{const_name Nat.one_nat_inst.one_nat},
@{const_name Orderings.less}, @{const_name Orderings.less_eq},
@{const_name Groups.zero},
@{const_name Groups.one}, @{const_name Groups.plus},
@{const_name Nat.ord_nat_inst.less_eq_nat},
@{const_name Nat.ord_nat_inst.less_nat},
@{const_name number_nat_inst.number_of_nat},
@{const_name Int.Bit0},
@{const_name Int.Bit1},
@{const_name Int.Pls},
@{const_name Int.zero_int_inst.zero_int},
@{const_name List.filter}] c
fun print_specification options thy constname specs =
if show_intermediate_results options then
tracing ("Specification of " ^ constname ^ ":\n" ^
cat_lines (map (Display.string_of_thm_global thy) specs))
else ()
fun obtain_specification_graph options thy t =
let
fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
fun has_code_pred_intros (c, T) = is_some (try (Predicate_Compile_Core.intros_of thy) 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 =
fold (Term.add_consts o prop_of) specs []
|> filter_out is_datatype_constructor
|> filter_out is_nondefining_const
|> filter_out has_code_pred_intros
|> filter_out case_consts
|> filter_out special_cases
|> map Const
(*
|> filter is_defining_constname*)
fun extend t =
let
val specs = get_specification thy t
|> map (inline_equations thy)
(*|> Predicate_Compile_Set.unfold_set_notation*)
(*val _ = print_specification options thy constname specs*)
in (specs, defiants_of specs) end;
in
TermGraph.extend extend t TermGraph.empty
end;
end;