moved argument expected_modes into options; improved mode check to only check mode of the named predicate

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -133,18 +133,18 @@
 (* Different options for compiler *)
 
 datatype options = Options of {  
-  (*check_modes : (string * int list list) list,*)
+  expected_modes : (string * int list list) option,
   show_steps : bool,
   show_mode_inference : bool,
   show_proof_trace : bool,
   show_intermediate_results : bool,
-  (*
-  inductify_functions : bool,
-  *)
+
   inductify : bool,
-  rpred : bool
+  rpred : bool,
+  sizelim : bool
 };
 
+fun expected_modes (Options opt) = #expected_modes opt
 fun show_steps (Options opt) = #show_steps opt
 fun show_mode_inference (Options opt) = #show_mode_inference opt
 fun show_intermediate_results (Options opt) = #show_intermediate_results opt
@@ -152,15 +152,17 @@
 
 fun is_inductify (Options opt) = #inductify opt
 fun is_rpred (Options opt) = #rpred opt
-
+fun is_sizelim (Options opt) = #sizelim opt
 
 val default_options = Options {
+  expected_modes = NONE,
   show_steps = false,
   show_intermediate_results = false,
   show_proof_trace = false,
   show_mode_inference = false,
   inductify = false,
-  rpred = false
+  rpred = false,
+  sizelim = false
 }
 
 

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -64,9 +64,9 @@
     val thy'' = thy'
       |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
       |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
-      |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options NONE [full_constname]
-      |> Predicate_Compile_Core.add_sizelim_equations Predicate_Compile_Aux.default_options NONE [full_constname]
-      |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options NONE [full_constname]
+      |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]
+      |> Predicate_Compile_Core.add_sizelim_equations Predicate_Compile_Aux.default_options [full_constname]
+      |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname]
     val sizelim_modes = Predicate_Compile_Core.sizelim_modes_of thy'' full_constname
     val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname  
     val prog =

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -101,46 +101,47 @@
     (Graph.strong_conn gr) thy
   end
 
-fun extract_options ((modes, raw_options), raw_const) =
+fun extract_options ((modes, raw_options), const) =
   let
     fun chk s = member (op =) raw_options s
   in
     Options {
+      expected_modes = Option.map (pair const) modes,
       show_steps = chk "show_steps",
       show_intermediate_results = chk "show_intermediate_results",
       show_proof_trace = chk "show_proof_trace",
       show_mode_inference = chk "show_mode_inference",
       inductify = chk "inductify",
-      rpred = chk "rpred"
+      rpred = chk "rpred",
+      sizelim = chk "sizelim"
     }
   end
 
 fun code_pred_cmd ((modes, raw_options), raw_const) lthy =
   let
-    val options = extract_options ((modes, raw_options), raw_const)
-  in  
+     val thy = ProofContext.theory_of lthy
+     val const = Code.read_const thy raw_const
+     val options = extract_options ((modes, raw_options), const)
+  in
     if (is_inductify options) then
       let
-        val thy = ProofContext.theory_of lthy
-        val const = Code.read_const thy raw_const
         val lthy' = LocalTheory.theory (preprocess options const) lthy
           |> LocalTheory.checkpoint
-          
         val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
             SOME c => c
           | NONE => const
         val _ = print_step options "Starting Predicate Compile Core..."
       in
-        Predicate_Compile_Core.code_pred options modes const lthy'
+        Predicate_Compile_Core.code_pred options const lthy'
       end
     else
-      Predicate_Compile_Core.code_pred_cmd options modes raw_const lthy
+      Predicate_Compile_Core.code_pred_cmd options raw_const lthy
   end
 
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace",
-  "show_mode_inference", "inductify", "rpred"]
+  "show_mode_inference", "inductify", "rpred", "sizelim"]
 
 val _ = List.app OuterKeyword.keyword ("mode" :: bool_options)
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -7,8 +7,8 @@
 signature PREDICATE_COMPILE_CORE =
 sig
   val setup: theory -> theory
-  val code_pred: Predicate_Compile_Aux.options -> int list list option -> string -> Proof.context -> Proof.state
-  val code_pred_cmd: Predicate_Compile_Aux.options -> int list list option -> string -> Proof.context -> Proof.state
+  val code_pred: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+  val code_pred_cmd: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
   type smode = (int * int list option) list
   type mode = smode option list * smode
   datatype tmode = Mode of mode * smode * tmode option list;
@@ -39,7 +39,7 @@
   val mk_casesrule : Proof.context -> int -> thm list -> term
   val analyze_compr: theory -> term -> term
   val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref
-  val add_equations : Predicate_Compile_Aux.options -> int list list option -> string list -> theory -> theory
+  val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val code_pred_intros_attrib : attribute
   (* used by Quickcheck_Generator *) 
   (*val funT_of : mode -> typ -> typ
@@ -90,8 +90,8 @@
   val rpred_compfuns : compilation_funs
   val dest_funT : typ -> typ * typ
  (* val depending_preds_of : theory -> thm list -> string list *)
-  val add_quickcheck_equations : Predicate_Compile_Aux.options -> int list list option -> string list -> theory -> theory
-  val add_sizelim_equations : Predicate_Compile_Aux.options -> int list list option -> string list -> theory -> theory
+  val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+  val add_sizelim_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val is_inductive_predicate : theory -> string -> bool
   val terms_vs : term list -> string list
   val subsets : int -> int -> int list list
@@ -398,9 +398,10 @@
      
 (* diagnostic display functions *)
 
-fun print_modes modes = tracing ("Inferred modes:\n" ^
-  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
-    string_of_mode ms)) modes));
+fun print_modes modes =
+  tracing ("Inferred modes:\n" ^
+    cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
+      string_of_mode ms)) modes));
 
 fun print_pred_mode_table string_of_entry thy pred_mode_table =
   let
@@ -482,6 +483,19 @@
     fold print (all_modes_of thy) ()
   end
 
+(* validity checks *)
+
+fun check_expected_modes (options : Predicate_Compile_Aux.options) modes =
+  case expected_modes options of
+    SOME (s, ms) => (case AList.lookup (op =) modes s of
+      SOME modes =>
+        if not (eq_set (map (map (rpair NONE)) ms, map snd modes)) then
+          error ("expected modes were not inferred:"
+            ^ "infered modes for " ^ s ^ ": " ^ commas (map (string_of_smode o snd) modes))
+        else ()
+      | NONE => ())
+  | NONE => ()
+
 (* importing introduction rules *)   
 
 fun unify_consts thy cs intr_ts =
@@ -1470,7 +1484,7 @@
                      NONE => in_ts
                    | SOME size_t => in_ts @ [size_t]
                    val u = lift_pred compfuns
-                     (list_comb (compile_expr NONE size thy (mode, t), args))                     
+                     (list_comb (compile_expr NONE size thy (mode, t), args))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
@@ -2305,22 +2319,18 @@
 
 (** main function of predicate compiler **)
 
-fun add_equations_of steps options expected_modes prednames thy =
+fun add_equations_of steps options prednames thy =
   let
     val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
-    val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
+    val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
       (*val _ = check_intros_elim_match thy prednames*)
       (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
     val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
       prepare_intrs thy prednames (maps (intros_of thy) prednames)
     val _ = print_step options "Infering modes..."
     val moded_clauses = #infer_modes steps options thy extra_modes all_modes param_vs clauses 
-    val modes : (string * ((int * int list option) list option list * (int * int list option) list) list) list = map (fn (p, mps) => (p, map fst mps)) moded_clauses
-    val all_smodes : (((int * int list option) list) list) list = map (map snd) (map snd modes)
-    val _ = case expected_modes of
-      SOME ms => if not (forall (fn smodes => eq_set (map (map (rpair NONE)) ms, smodes)) all_smodes) then
-      error ("expected modes were not inferred - " ^ commas (map string_of_smode (flat all_smodes))) else ()
-      | NONE => ()
+    val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
+    val _ = check_expected_modes options modes
     val _ = print_modes modes
     val _ = print_moded_clauses thy moded_clauses
     val _ = print_step options "Defining executable functions..."
@@ -2359,7 +2369,7 @@
 
 fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) 
   
-fun gen_add_equations steps options expected_modes names thy =
+fun gen_add_equations steps options names thy =
   let
     val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy
       |> Theory.checkpoint;
@@ -2369,7 +2379,7 @@
     val thy'' = fold_rev
       (fn preds => fn thy =>
         if #are_not_defined steps thy preds then
-          add_equations_of steps options expected_modes preds thy else thy)
+          add_equations_of steps options preds thy else thy)
       scc thy' |> Theory.checkpoint
   in thy'' end
 
@@ -2417,15 +2427,11 @@
 val setup = PredData.put (Graph.empty) #>
   Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
     "adding alternative introduction rules for code generation of inductive predicates"
-(*  Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib)
-    "adding alternative elimination rules for code generation of inductive predicates";
-    *)
   (*FIXME name discrepancy in attribs and ML code*)
   (*FIXME intros should be better named intro*)
-  (*FIXME why distinguished attribute for cases?*)
 
 (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
-fun generic_code_pred prep_const options modes raw_const lthy =
+fun generic_code_pred prep_const options raw_const lthy =
   let
     val thy = ProofContext.theory_of lthy
     val const = prep_const thy raw_const
@@ -2455,9 +2461,12 @@
       in
         goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
           (if is_rpred options then
-            (add_equations options NONE [const] #>
-             add_sizelim_equations options NONE [const] #> add_quickcheck_equations options NONE [const])
-           else add_equations options modes [const]))
+            (add_equations options [const] #>
+             add_sizelim_equations options [const] #> add_quickcheck_equations options [const])
+           else if is_sizelim options then
+             add_sizelim_equations options [const]
+           else
+             add_equations options [const]))
       end  
   in
     Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''