added profiling code, improved handling of proof terms, generation of domain
introduction rules becomes optional (global reference FundefCommon.domintros)
--- a/src/HOL/Tools/function_package/fundef_common.ML Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML Wed Nov 08 22:24:54 2006 +0100
@@ -12,6 +12,11 @@
(* Theory Dependencies *)
val acc_const_name = "FunDef.accP"
+val domintros = ref true;
+val profile = ref false;
+
+fun PROFILE msg = if !profile then timeap_msg msg else I
+
fun mk_acc domT R =
Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R
@@ -175,14 +180,26 @@
domintros : thm list
}
+datatype fundef_context_data =
+ FundefCtxData of
+ {
+ fixes : ((string * typ) * mixfix) list,
+ spec : ((string * Attrib.src list) * term list) list list,
+ mutual: mutual_info,
-type fundef_spec = ((string * typ) * mixfix) list *((string * Attrib.src list) * term list) list list
-type result_with_names = fundef_mresult * mutual_info * fundef_spec
+ f : term,
+ R : term,
+
+ psimps: thm list,
+ pinducts: thm list,
+ termination: thm
+ }
+
structure FundefData = GenericDataFun
(struct
val name = "HOL/function_def/data";
- type T = string * result_with_names Symtab.table
+ type T = string * fundef_context_data Symtab.table
val empty = ("", Symtab.empty);
val copy = I;
@@ -206,10 +223,11 @@
fun add_fundef_data name fundef_data =
- FundefData.map (fn (_,tab) => (name, Symtab.update_new (name, fundef_data) tab))
+ FundefData.map (fn (last,tab) => (name, Symtab.update_new (name, fundef_data) tab))
fun get_fundef_data name thy = Symtab.lookup (snd (FundefData.get thy)) name
+fun set_last_fundef name = FundefData.map (apfst (K name))
fun get_last_fundef thy = fst (FundefData.get thy)
val map_fundef_congs = FundefCongs.map
--- a/src/HOL/Tools/function_package/fundef_package.ML Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Nov 08 22:24:54 2006 +0100
@@ -50,31 +50,43 @@
fun add_simps label moreatts mutual_info fixes psimps spec lthy =
let
val fnames = map (fst o fst) fixes
- val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames psimps
+
+ val (saved_spec_psimps, lthy) = fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) lthy
+ val saved_psimps = flat (map snd (flat saved_spec_psimps))
+
+ val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
fun add_for_f fname psimps =
LocalTheory.note ((NameSpace.append fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
in
- lthy
- |> fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) |> snd
- |> fold2 add_for_f fnames psimps_by_f
+ (saved_psimps,
+ fold2 add_for_f fnames psimps_by_f lthy)
end
fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy =
let
- val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
- val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
- val qualify = NameSpace.append defname;
+ val Prep {f, R, ...} = data
+ val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
+ val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
+ val qualify = NameSpace.append defname
+
+ val (((psimps', pinducts'), (_, [termination'])), lthy) =
+ lthy
+ |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
+ ||>> PROFILE "adding pinduct" (LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
+ ||>> PROFILE "adding termination" (LocalTheory.note ((qualify "termination", []), [termination]))
+ ||> (snd o PROFILE "adding cases" (LocalTheory.note ((qualify "cases", []), [cases])))
+ ||> (snd o PROFILE "adding domintros" (LocalTheory.note ((qualify "domintros", []), domintros)))
+
+ val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
+ pinducts=snd pinducts', termination=termination', f=f, R=R }
+
+
in
lthy
- |> add_simps "psimps" [] mutual_info fixes psimps spec
- |> LocalTheory.note ((qualify "domintros", []), domintros) |> snd
- |> LocalTheory.note ((qualify "termination", []), [termination]) |> snd
- |> LocalTheory.note ((qualify "cases", []), [cases]) |> snd
- |> LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) |> snd
- |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* save in target *)
- |> Context.proof_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* also save in local context *)
+ |> LocalTheory.declaration (add_fundef_data defname cdata) (* save in target *)
+ |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
end (* FIXME: Add cases for induct and cases thm *)
@@ -117,12 +129,14 @@
fun total_termination_afterqed defname data [[totality]] lthy =
let
- val (FundefMResult {psimps, simple_pinducts, ... }, mutual_info, (fixes, stmts)) = data
+ val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data
+
+ val totality = PROFILE "closing" Drule.close_derivation totality
- val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
+ val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
- val tsimps = map remove_domain_condition psimps
- val tinduct = map remove_domain_condition simple_pinducts
+ val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
+ val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
(* FIXME: How to generate code from (possibly) local contexts
val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
@@ -131,8 +145,8 @@
val qualify = NameSpace.append defname;
in
lthy
- |> add_simps "simps" [] mutual_info fixes tsimps stmts
- |> LocalTheory.note ((qualify "induct", []), tinduct) |> snd
+ |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd
+ |> PROFILE "adding tinduct" (LocalTheory.note ((qualify "induct", []), tinduct)) |> snd
end
@@ -142,8 +156,8 @@
val data = the (get_fundef_data name (Context.Proof lthy))
handle Option.Option => raise ERROR ("No such function definition: " ^ name)
- val (res as FundefMResult {termination, ...}, _, _) = data
- val goal = FundefTermination.mk_total_termination_goal data
+ val FundefCtxData {termination, f, R, ...} = data
+ val goal = FundefTermination.mk_total_termination_goal f R
in
lthy
|> ProofContext.note_thmss_i [(("termination",
--- a/src/HOL/Tools/function_package/fundef_prep.ML Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Wed Nov 08 22:24:54 2006 +0100
@@ -477,6 +477,8 @@
val fvar = Free (fname, fT)
val domT = domain_type fT
val ranT = range_type fT
+
+
val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
@@ -485,7 +487,7 @@
val Globals { x, h, ... } = globals
- val clauses = map (mk_clause_context x ctxt') abstract_qglrs
+ val clauses = PROFILE "mk_clause_context" (map (mk_clause_context x ctxt')) abstract_qglrs
val n = length abstract_qglrs
@@ -494,34 +496,34 @@
fun build_tree (ClauseContext { ctxt, rhs, ...}) =
FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
- val trees = map build_tree clauses
- val RCss = map find_calls trees
+ val trees = PROFILE "making trees" (map build_tree) clauses
+ val RCss = PROFILE "finding calls" (map find_calls) trees
- val ((G, GIntro_thms, G_elim), lthy) = define_graph (defname ^ "_graph") fvar domT ranT clauses RCss lthy
- val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default lthy
+ val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (defname ^ "_graph") fvar domT ranT clauses RCss) lthy
+ val ((f, f_defthm), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
- val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
- val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
+ val RCss = PROFILE "inst_RCs" (map (map (inst_RC (ProofContext.theory_of lthy) fvar f))) RCss
+ val trees = PROFILE "inst_trees" (map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f)) trees
val ((R, RIntro_thmss, R_elim), lthy) =
- define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss lthy
+ PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss) lthy
val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", domT --> boolT), mk_acc domT R)
- val lthy = Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)] lthy
+ val lthy = PROFILE "abbrev" (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) lthy
val newthy = ProofContext.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
val cert = cterm_of (ProofContext.theory_of lthy)
- val xclauses = map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms RIntro_thmss
+ val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
- val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
- val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
+ val complete = PROFILE "mk_compl" (mk_completeness globals clauses) abstract_qglrs |> cert |> assume
+ val compat = PROFILE "mk_compat" (mk_compat_proof_obligations domT ranT fvar f) abstract_qglrs |> map (cert #> assume)
val compat_store = store_compat_thms n compat
- val (goal, goalI, ex1_iff, values) = prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim f_defthm
+ val (goal, goalI, ex1_iff, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
in
(Prep {globals = globals, f = f, G = G, R = R, goal = goal, goalI = goalI, values = values, clauses = xclauses, ex1_iff = ex1_iff, R_cases = R_elim}, f,
lthy)
--- a/src/HOL/Tools/function_package/fundef_proof.ML Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_proof.ML Wed Nov 08 22:24:54 2006 +0100
@@ -43,11 +43,11 @@
fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
let
- val Globals {domT, z, ...} = globals
-
- val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
- val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
- val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+ val Globals {domT, z, ...} = globals
+
+ val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
+ val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+ val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
in
((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
|> (fn it => it COMP graph_is_function)
@@ -64,29 +64,29 @@
fun mk_partial_induct_rule thy globals R complete_thm clauses =
let
- val Globals {domT, x, z, a, P, D, ...} = globals
- val acc_R = mk_acc domT R
-
- val x_D = assume (cterm_of thy (Trueprop (D $ x)))
- val a_D = cterm_of thy (Trueprop (D $ a))
-
- val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
-
- val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
- mk_forall x
- (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
- Logic.mk_implies (Trueprop (R $ z $ x),
- Trueprop (D $ z)))))
- |> cterm_of thy
-
-
+ val Globals {domT, x, z, a, P, D, ...} = globals
+ val acc_R = mk_acc domT R
+
+ val x_D = assume (cterm_of thy (Trueprop (D $ x)))
+ val a_D = cterm_of thy (Trueprop (D $ a))
+
+ val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
+
+ val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
+ mk_forall x
+ (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
+ Logic.mk_implies (Trueprop (R $ z $ x),
+ Trueprop (D $ z)))))
+ |> cterm_of thy
+
+
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
- val ihyp = all domT $ Abs ("z", domT,
- implies $ Trueprop (R $ Bound 0 $ x)
+ val ihyp = all domT $ Abs ("z", domT,
+ implies $ Trueprop (R $ Bound 0 $ x)
$ Trueprop (P $ Bound 0))
|> cterm_of thy
- val aihyp = assume ihyp
+ val aihyp = assume ihyp
fun prove_case clause =
let
@@ -188,6 +188,9 @@
end
+fun maybe_mk_domain_intro thy =
+ if !FundefCommon.domintros then mk_domain_intro thy
+ else K (K (K (K refl)))
fun mk_nest_term_case thy globals R' ihyp clause =
@@ -296,34 +299,22 @@
let
val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
- val _ = Output.debug "Closing Derivation"
-
- val provedgoal = Drule.close_derivation provedgoal
+ val provedgoal = PROFILE "Closing Derivation" Drule.close_derivation provedgoal
- val _ = Output.debug "Getting function theorem"
-
- val graph_is_function = (provedgoal COMP conjunctionD1)
- |> forall_elim_vars 0
+ val graph_is_function = PROFILE "Getting function theorem" (fn x => (x COMP conjunctionD1) |> forall_elim_vars 0) provedgoal
- val _ = Output.debug "Getting cases"
-
- val complete_thm = provedgoal COMP conjunctionD2
-
- val _ = Output.debug "Making f_iff"
-
- val f_iff = (graph_is_function RS ex1_iff)
+ val complete_thm = PROFILE "Getting cases" (curry op COMP provedgoal) conjunctionD2
+
+ val f_iff = PROFILE "Making f_iff" (curry op RS graph_is_function) ex1_iff
- val _ = Output.debug "Proving simplification rules"
- val psimps = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
+ val psimps = PROFILE "Proving simplification rules" (map2 (mk_psimp thy globals R f_iff graph_is_function)) clauses values
- val _ = Output.debug "Proving partial induction rule"
- val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
+ val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule"
+ (mk_partial_induct_rule thy globals R complete_thm) clauses
- val _ = Output.debug "Proving nested termination rule"
- val total_intro = mk_nest_term_rule thy globals R R_cases clauses
+ val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule thy globals R R_cases) clauses
- val _ = Output.debug "Proving domain introduction rules"
- val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
+ val dom_intros = PROFILE "Proving domain introduction rules" (map (maybe_mk_domain_intro thy globals R R_cases)) clauses
in
FundefResult {f=f, G=G, R=R, completeness=complete_thm,
psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
--- a/src/HOL/Tools/function_package/mutual.ML Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML Wed Nov 08 22:24:54 2006 +0100
@@ -337,10 +337,9 @@
fun mk_mpsimp fqgar sum_psimp =
in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
- val mpsimps = map2 mk_mpsimp fqgars psimps
-
- val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
- val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
+ val mpsimps = PROFILE "making mpsimps" (map2 mk_mpsimp fqgars) psimps
+ val minducts = PROFILE "making mpinduct" (mutual_induct_rules thy simple_pinduct all_f_defs) m
+ val termination = PROFILE "making mtermination" (full_simplify (HOL_basic_ss addsimps all_f_defs)) total_intro
in
FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R,
psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
--- a/src/HOL/Tools/function_package/termination.ML Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/termination.ML Wed Nov 08 22:24:54 2006 +0100
@@ -9,8 +9,8 @@
signature FUNDEF_TERMINATION =
sig
- val mk_total_termination_goal : FundefCommon.result_with_names -> term
- val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
+ val mk_total_termination_goal : term -> term -> term
+(* val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*)
end
structure FundefTermination : FUNDEF_TERMINATION =
@@ -21,7 +21,7 @@
open FundefCommon
open FundefAbbrev
-fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
+fun mk_total_termination_goal f R =
let
val domT = domain_type (fastype_of f)
val x = Free ("x", domT)
@@ -29,6 +29,7 @@
mk_forall x (Trueprop (mk_acc domT R $ x))
end
+(*
fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
let
val domT = domain_type (fastype_of f)
@@ -55,7 +56,7 @@
in
(subs, dcl)
end
-
+*)
end