1.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy Sun Jun 28 22:51:29 2009 +0200
1.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Mon Jun 29 12:33:58 2009 +0200
1.3 @@ -58,11 +58,11 @@
1.4
1.5 lemma [code_pred_intros]:
1.6 "r a b ==> tranclp r a b"
1.7 -"r a b ==> tranclp r b c ==> tranclp r a c"
1.8 +"r a b ==> tranclp r b c ==> tranclp r a c"
1.9 by auto
1.10
1.11 (* Setup requires quick and dirty proof *)
1.12 -(*
1.13 +
1.14 code_pred tranclp
1.15 proof -
1.16 case tranclp
1.17 @@ -70,7 +70,6 @@
1.18 qed
1.19
1.20 thm tranclp.equation
1.21 -*)
1.22
1.23 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
1.24 "succ 0 1"
2.1 --- a/src/HOL/ex/predicate_compile.ML Sun Jun 28 22:51:29 2009 +0200
2.2 +++ b/src/HOL/ex/predicate_compile.ML Mon Jun 29 12:33:58 2009 +0200
2.3 @@ -9,6 +9,7 @@
2.4 type mode = int list option list * int list
2.5 val add_equations_of: string list -> theory -> theory
2.6 val register_predicate : (thm list * thm * int) -> theory -> theory
2.7 + val fetch_pred_data : theory -> string -> (thm list * thm * int)
2.8 val predfun_intro_of: theory -> string -> mode -> thm
2.9 val predfun_elim_of: theory -> string -> mode -> thm
2.10 val strip_intro_concl: int -> term -> term * (term list * term list)
2.11 @@ -17,14 +18,18 @@
2.12 val modes_of: theory -> string -> mode list
2.13 val intros_of: theory -> string -> thm list
2.14 val nparams_of: theory -> string -> int
2.15 + val add_intro: thm -> theory -> theory
2.16 + val set_elim: thm -> theory -> theory
2.17 val setup: theory -> theory
2.18 val code_pred: string -> Proof.context -> Proof.state
2.19 val code_pred_cmd: string -> Proof.context -> Proof.state
2.20 -(* val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) *)
2.21 + val print_stored_rules: theory -> unit
2.22 val do_proofs: bool ref
2.23 + val mk_casesrule : Proof.context -> int -> thm list -> term
2.24 val analyze_compr: theory -> term -> term
2.25 val eval_ref: (unit -> term Predicate.pred) option ref
2.26 val add_equations : string -> theory -> theory
2.27 + val code_pred_intros_attrib : attribute
2.28 end;
2.29
2.30 structure Predicate_Compile : PREDICATE_COMPILE =
2.31 @@ -223,25 +228,26 @@
2.32
2.33 val predfun_elim_of = #elim ooo the_predfun_data
2.34
2.35 +fun print_stored_rules thy =
2.36 + let
2.37 + val preds = (Graph.keys o PredData.get) thy
2.38 + fun print pred () = let
2.39 + val _ = writeln ("predicate: " ^ pred)
2.40 + val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
2.41 + val _ = writeln ("introrules: ")
2.42 + val _ = fold (fn thm => fn u => writeln (Display.string_of_thm thm))
2.43 + (rev (intros_of thy pred)) ()
2.44 + in
2.45 + if (has_elim thy pred) then
2.46 + writeln ("elimrule: " ^ Display.string_of_thm (the_elim_of thy pred))
2.47 + else
2.48 + writeln ("no elimrule defined")
2.49 + end
2.50 + in
2.51 + fold print preds ()
2.52 + end;
2.53
2.54 -(* replaces print_alternative_rules *)
2.55 -(* TODO:
2.56 -fun print_alternative_rules thy = let
2.57 - val d = IndCodegenData.get thy
2.58 - val preds = (Symtab.keys (#intro_rules d)) union (Symtab.keys (#elim_rules d))
2.59 - val _ = tracing ("preds: " ^ (makestring preds))
2.60 - fun print pred = let
2.61 - val _ = tracing ("predicate: " ^ pred)
2.62 - val _ = tracing ("introrules: ")
2.63 - val _ = fold (fn thm => fn u => tracing (makestring thm))
2.64 - (rev (Symtab.lookup_list (#intro_rules d) pred)) ()
2.65 - val _ = tracing ("casesrule: ")
2.66 - val _ = tracing (makestring (Symtab.lookup (#elim_rules d) pred))
2.67 - in () end
2.68 - val _ = map print preds
2.69 - in thy end;
2.70 -*)
2.71 -
2.72 +(** preprocessing rules **)
2.73
2.74 fun imp_prems_conv cv ct =
2.75 case Thm.term_of ct of
2.76 @@ -298,6 +304,23 @@
2.77 val add = apsnd (cons (mode, mk_predfun_data data))
2.78 in PredData.map (Graph.map_node name (map_pred_data add)) end
2.79
2.80 +fun is_inductive_predicate thy name =
2.81 + is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
2.82 +
2.83 +fun depending_preds_of thy intros = fold Term.add_consts (map Thm.prop_of intros) [] |> map fst
2.84 + |> filter (fn c => is_inductive_predicate thy c orelse is_pred thy c)
2.85 +
2.86 +(* code dependency graph *)
2.87 +fun dependencies_of thy name =
2.88 + let
2.89 + val (intros, elim, nparams) = fetch_pred_data thy name
2.90 + val data = mk_pred_data ((intros, SOME elim, nparams), [])
2.91 + val keys = depending_preds_of thy intros
2.92 + in
2.93 + (data, keys)
2.94 + end;
2.95 +
2.96 +(* TODO: add_edges - by analysing dependencies *)
2.97 fun add_intro thm thy = let
2.98 val (name, _) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
2.99 fun cons_intro gr =
2.100 @@ -320,10 +343,13 @@
2.101 fun set (intros, elim, _ ) = (intros, elim, nparams)
2.102 in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
2.103
2.104 -fun register_predicate (intros, elim, nparams) = let
2.105 +fun register_predicate (intros, elim, nparams) thy = let
2.106 val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd intros))))
2.107 fun set _ = (intros, SOME elim, nparams)
2.108 - in PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))) end
2.109 + in
2.110 + PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))
2.111 + #> fold Graph.add_edge (map (pair name) (depending_preds_of thy intros))) thy
2.112 + end
2.113
2.114
2.115 (* Mode analysis *)
2.116 @@ -1243,7 +1269,7 @@
2.117 end;
2.118 val prems_tac = prove_prems2 in_ts' param_vs ps
2.119 in
2.120 - print_tac "starting prove_clause2"
2.121 + new_print_tac "starting prove_clause2"
2.122 THEN etac @{thm bindE} 1
2.123 THEN (etac @{thm singleE'} 1)
2.124 THEN (TRY (etac @{thm Pair_inject} 1))
2.125 @@ -1259,6 +1285,7 @@
2.126 (DETERM (TRY (rtac @{thm unit.induct} 1)))
2.127 THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
2.128 THEN (rtac (predfun_intro_of thy pred mode) 1)
2.129 + THEN (REPEAT_DETERM (rtac @{thm refl} 2))
2.130 THEN (EVERY (map prove_clause (clauses ~~ (1 upto (length clauses)))))
2.131 end;
2.132
2.133 @@ -1409,21 +1436,6 @@
2.134 val cases = map mk_case intros
2.135 in Logic.list_implies (assm :: cases, prop) end;
2.136
2.137 -(* code dependency graph *)
2.138 -
2.139 -fun dependencies_of thy name =
2.140 - let
2.141 - fun is_inductive_predicate thy name =
2.142 - is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
2.143 - val (intro, elim, nparams) = fetch_pred_data thy name
2.144 - val data = mk_pred_data ((intro, SOME elim, nparams), [])
2.145 - val intros = map Thm.prop_of (#intros (rep_pred_data data))
2.146 - val keys = fold Term.add_consts intros [] |> map fst
2.147 - |> filter (is_inductive_predicate thy)
2.148 - in
2.149 - (data, keys)
2.150 - end;
2.151 -
2.152 fun add_equations name thy =
2.153 let
2.154 val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy |> Theory.checkpoint;
2.155 @@ -1437,17 +1449,15 @@
2.156 scc thy' |> Theory.checkpoint
2.157 in thy'' end
2.158
2.159 +
2.160 +fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
2.161 +
2.162 +val code_pred_intros_attrib = attrib add_intro;
2.163 +
2.164 (** user interface **)
2.165
2.166 local
2.167
2.168 -fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
2.169 -
2.170 -(*
2.171 -val add_elim_attrib = attrib set_elim;
2.172 -*)
2.173 -
2.174 -
2.175 (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
2.176 (* TODO: must create state to prove multiple cases *)
2.177 fun generic_code_pred prep_const raw_const lthy =