# HG changeset patch
# User bulwahn
# Date 1246366470 -7200
# Node ID e3de75d3b8987f38d40a01ae2cdf10daad9a8aec
# Parent  9ab571673059e3976d531c3984c9a8905d09be56
exported is_registered; added debug messages; removed extended parameter compilation in predicate compiler

diff -r 9ab571673059 -r e3de75d3b898 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Mon Jun 29 12:33:58 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Tue Jun 30 14:54:30 2009 +0200
@@ -9,6 +9,7 @@
   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
@@ -192,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
 
@@ -308,7 +309,7 @@
   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_pred thy c)
+    |> filter (fn c => is_inductive_predicate thy c orelse is_registered thy c)
 
 (* code dependency graph *)    
 fun dependencies_of thy name =
@@ -651,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
@@ -663,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"
   
   
@@ -1142,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
@@ -1158,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
@@ -1166,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"
@@ -1348,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