src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

 *)
 
 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;
   (*val add_equations_of: bool -> string list -> theory -> theory *)
   val register_predicate : (thm list * thm * int) -> theory -> theory

   val print_all_modes: theory -> unit
   val do_proofs: bool Unsynchronized.ref
   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
   val mk_if_pred : term -> term
   val mk_Eval : term * term -> term*)

   (*val rpred_prove_preds : theory -> term pred_mode_table -> thm pred_mode_table*)
   val pred_compfuns : compilation_funs
   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
   val check_mode_clause : bool -> theory -> string list ->
     (string * mode list) list -> (string * mode list) list -> mode -> (term list * indprem list)

 
 (*val generator_modes_of = (map fst) o #generators oo the_pred_data*)
      
 (* 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
     fun print_mode pred (mode, entry) =  "mode : " ^ (string_of_mode mode)
       ^ (string_of_entry pred mode entry)  

         val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
       in u end  
   in
     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 =
   (let

                    val in_ts = map (compile_arg size thy param_vs iss) in_ts
                    val args = case size of
                      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)
                  end
              | Negprem (us, t) =>

 *)
 
 
 (** 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..."
     val thy' = fold (#create_definitions steps preds) modes thy
       |> Theory.checkpoint

     (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
   end;
 
 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;
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
     val scc = strong_conn_of (PredData.get thy') names
     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
 
 (* different instantiantions of the predicate compiler *)
 

 *)
 
 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
     val lthy' = LocalTheory.theory (PredData.map
         (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy

         val global_thms = ProofContext.export goal_ctxt
           (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
       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''
   end;