--- a/src/HOL/ex/predicate_compile.ML Tue Jun 30 14:54:32 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Tue Jun 30 14:55:06 2009 +0200
@@ -9,6 +9,8 @@
type mode = int list option list * int list
val add_equations_of: string list -> theory -> theory
val register_predicate : (thm list * thm * int) -> theory -> theory
+ val is_registered : theory -> string -> bool
+ val fetch_pred_data : theory -> string -> (thm list * thm * int)
val predfun_intro_of: theory -> string -> mode -> thm
val predfun_elim_of: theory -> string -> mode -> thm
val strip_intro_concl: int -> term -> term * (term list * term list)
@@ -17,14 +19,18 @@
val modes_of: theory -> string -> mode list
val intros_of: theory -> string -> thm list
val nparams_of: theory -> string -> int
+ val add_intro: thm -> theory -> theory
+ val set_elim: thm -> theory -> theory
val setup: theory -> theory
val code_pred: string -> Proof.context -> Proof.state
val code_pred_cmd: string -> Proof.context -> Proof.state
-(* val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) *)
+ val print_stored_rules: theory -> unit
val do_proofs: bool ref
+ val mk_casesrule : Proof.context -> int -> thm list -> term
val analyze_compr: theory -> term -> term
val eval_ref: (unit -> term Predicate.pred) option ref
val add_equations : string -> theory -> theory
+ val code_pred_intros_attrib : attribute
end;
structure Predicate_Compile : PREDICATE_COMPILE =
@@ -187,7 +193,7 @@
of NONE => error ("No such predicate " ^ quote name)
| SOME data => data;
-val is_pred = is_some oo lookup_pred_data
+val is_registered = is_some oo lookup_pred_data
val all_preds_of = Graph.keys o PredData.get
@@ -223,25 +229,26 @@
val predfun_elim_of = #elim ooo the_predfun_data
+fun print_stored_rules thy =
+ let
+ val preds = (Graph.keys o PredData.get) thy
+ fun print pred () = let
+ val _ = writeln ("predicate: " ^ pred)
+ val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
+ val _ = writeln ("introrules: ")
+ val _ = fold (fn thm => fn u => writeln (Display.string_of_thm thm))
+ (rev (intros_of thy pred)) ()
+ in
+ if (has_elim thy pred) then
+ writeln ("elimrule: " ^ Display.string_of_thm (the_elim_of thy pred))
+ else
+ writeln ("no elimrule defined")
+ end
+ in
+ fold print preds ()
+ end;
-(* replaces print_alternative_rules *)
-(* TODO:
-fun print_alternative_rules thy = let
- val d = IndCodegenData.get thy
- val preds = (Symtab.keys (#intro_rules d)) union (Symtab.keys (#elim_rules d))
- val _ = tracing ("preds: " ^ (makestring preds))
- fun print pred = let
- val _ = tracing ("predicate: " ^ pred)
- val _ = tracing ("introrules: ")
- val _ = fold (fn thm => fn u => tracing (makestring thm))
- (rev (Symtab.lookup_list (#intro_rules d) pred)) ()
- val _ = tracing ("casesrule: ")
- val _ = tracing (makestring (Symtab.lookup (#elim_rules d) pred))
- in () end
- val _ = map print preds
- in thy end;
-*)
-
+(** preprocessing rules **)
fun imp_prems_conv cv ct =
case Thm.term_of ct of
@@ -298,6 +305,23 @@
val add = apsnd (cons (mode, mk_predfun_data data))
in PredData.map (Graph.map_node name (map_pred_data add)) end
+fun is_inductive_predicate thy name =
+ is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
+
+fun depending_preds_of thy intros = fold Term.add_consts (map Thm.prop_of intros) [] |> map fst
+ |> filter (fn c => is_inductive_predicate thy c orelse is_registered thy c)
+
+(* code dependency graph *)
+fun dependencies_of thy name =
+ let
+ val (intros, elim, nparams) = fetch_pred_data thy name
+ val data = mk_pred_data ((intros, SOME elim, nparams), [])
+ val keys = depending_preds_of thy intros
+ in
+ (data, keys)
+ end;
+
+(* TODO: add_edges - by analysing dependencies *)
fun add_intro thm thy = let
val (name, _) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
fun cons_intro gr =
@@ -320,10 +344,13 @@
fun set (intros, elim, _ ) = (intros, elim, nparams)
in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
-fun register_predicate (intros, elim, nparams) = let
+fun register_predicate (intros, elim, nparams) thy = let
val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd intros))))
fun set _ = (intros, SOME elim, nparams)
- in PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))) end
+ in
+ PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))
+ #> fold Graph.add_edge (map (pair name) (depending_preds_of thy intros))) thy
+ end
(* Mode analysis *)
@@ -625,10 +652,11 @@
and compile_param thy modes (NONE, t) = t
| compile_param thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
- (case t of
- Abs _ => compile_param_ext thy modes (m, t)
- | _ => let
- val (f, args) = strip_comb t
+ (* (case t of
+ Abs _ => error "compile_param: Invalid term" *) (* compile_param_ext thy modes (m, t) *)
+ (* | _ => let *)
+ let
+ val (f, args) = strip_comb (Envir.eta_contract t)
val (params, args') = chop (length ms) args
val params' = map (compile_param thy modes) (ms ~~ params)
val f' = case f of
@@ -637,7 +665,7 @@
Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T)
else error "compile param: Not an inductive predicate with correct mode"
| Free (name, T) => Free (name, funT_of T (SOME is'))
- in list_comb (f', params' @ args') end)
+ in list_comb (f', params' @ args') end
| compile_param _ _ _ = error "compile params"
@@ -1116,7 +1144,7 @@
(* VERY LARGE SIMILIRATIY to function prove_param
-- join both functions
*)
-(*
+
fun prove_param2 thy modes (NONE, t) = all_tac
| prove_param2 thy modes (m as SOME (Mode (mode, is, ms)), t) = let
val (f, args) = strip_comb t
@@ -1132,7 +1160,7 @@
THEN print_tac "after simplification in prove_args"
THEN (EVERY (map (prove_param2 thy modes) (ms ~~ params)))
end
-*)
+
fun prove_expr2 thy modes (SOME (Mode (mode, is, ms)), t) =
(case strip_comb t of
@@ -1140,14 +1168,16 @@
if AList.defined op = modes name then
etac @{thm bindE} 1
THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
+ THEN new_print_tac "prove_expr2-before"
THEN (debug_tac (Syntax.string_of_term_global thy
(prop_of (predfun_elim_of thy name mode))))
THEN (etac (predfun_elim_of thy name mode) 1)
THEN new_print_tac "prove_expr2"
(* TODO -- FIXME: replace remove_last_goal*)
- THEN (EVERY (replicate (length args) (remove_last_goal thy)))
+ (* THEN (EVERY (replicate (length args) (remove_last_goal thy))) *)
+ THEN (EVERY (map (prove_param thy modes) (ms ~~ args)))
THEN new_print_tac "finished prove_expr2"
- (* THEN (EVERY (map (prove_param thy modes) (ms ~~ args))) *)
+
else error "Prove expr2 if case not implemented"
| _ => etac @{thm bindE} 1)
| prove_expr2 _ _ _ = error "Prove expr2 not implemented"
@@ -1243,7 +1273,7 @@
end;
val prems_tac = prove_prems2 in_ts' param_vs ps
in
- print_tac "starting prove_clause2"
+ new_print_tac "starting prove_clause2"
THEN etac @{thm bindE} 1
THEN (etac @{thm singleE'} 1)
THEN (TRY (etac @{thm Pair_inject} 1))
@@ -1259,6 +1289,7 @@
(DETERM (TRY (rtac @{thm unit.induct} 1)))
THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
THEN (rtac (predfun_intro_of thy pred mode) 1)
+ THEN (REPEAT_DETERM (rtac @{thm refl} 2))
THEN (EVERY (map prove_clause (clauses ~~ (1 upto (length clauses)))))
end;
@@ -1321,7 +1352,7 @@
| Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t)))
| Sidecond t => Sidecond (c $ t))
| (c as Const (s, _), ts) =>
- if is_pred thy s then
+ if is_registered thy s then
let val (ts1, ts2) = chop (nparams_of thy s) ts
in Prem (ts2, list_comb (c, ts1)) end
else Sidecond t
@@ -1409,21 +1440,6 @@
val cases = map mk_case intros
in Logic.list_implies (assm :: cases, prop) end;
-(* code dependency graph *)
-
-fun dependencies_of thy name =
- let
- fun is_inductive_predicate thy name =
- is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
- val (intro, elim, nparams) = fetch_pred_data thy name
- val data = mk_pred_data ((intro, SOME elim, nparams), [])
- val intros = map Thm.prop_of (#intros (rep_pred_data data))
- val keys = fold Term.add_consts intros [] |> map fst
- |> filter (is_inductive_predicate thy)
- in
- (data, keys)
- end;
-
fun add_equations name thy =
let
val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy |> Theory.checkpoint;
@@ -1437,17 +1453,15 @@
scc thy' |> Theory.checkpoint
in thy'' end
+
+fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
+
+val code_pred_intros_attrib = attrib add_intro;
+
(** user interface **)
local
-fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-
-(*
-val add_elim_attrib = attrib set_elim;
-*)
-
-
(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
(* TODO: must create state to prove multiple cases *)
fun generic_code_pred prep_const raw_const lthy =