added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -8,6 +8,7 @@
   val define_predicates : (string * thm list) list -> theory -> theory
   val rewrite_intro : theory -> thm -> thm list
   val setup_oracle : theory -> theory
+  val pred_of_function : theory -> string -> string option
 end;
 
 structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
@@ -63,6 +64,8 @@
   fun merge _ = Symtab.merge (op =);
 )
 
+fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
+
 fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) 
 
 
@@ -246,6 +249,8 @@
           let
             val _ = tracing ("Flattening term " ^ (Syntax.string_of_term_global thy t))
             val (f, args) = strip_comb t
+            (* TODO: special procedure for higher-order functions: split arguments in
+              simple types and function types *)
             val resname = Name.variant names "res"
             val resvar = Free (resname, body_type (fastype_of t))
             val names' = resname :: names
@@ -356,7 +361,7 @@
             Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
         end
     fun mk_rewr_thm (func, pred) = @{thm refl}
-  in    
+  in
     case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of
       NONE => thy 
     | SOME intr_ts => let

--- 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 full_constname
-      |> Predicate_Compile_Core.add_equations [full_constname]
-      |> Predicate_Compile_Core.add_sizelim_equations [full_constname]
-      |> Predicate_Compile_Core.add_quickcheck_equations [full_constname]
+      |> Predicate_Compile_Core.add_equations NONE [full_constname]
+      |> Predicate_Compile_Core.add_sizelim_equations NONE [full_constname]
+      |> Predicate_Compile_Core.add_quickcheck_equations NONE [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
@@ -135,28 +135,38 @@
     (Graph.strong_conn gr) thy
   end
 
-fun code_pred_cmd ((inductify_all, rpred), raw_const) lthy =
+fun code_pred_cmd (((modes, inductify_all), rpred), raw_const) lthy =
   if inductify_all then
     let
       val thy = ProofContext.theory_of lthy
       val const = Code.read_const thy raw_const
       val lthy' = LocalTheory.theory (preprocess 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 _ = tracing "Starting Predicate Compile Core..."
-    in Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy' end
+    in Predicate_Compile_Core.code_pred modes rpred const lthy' end
   else
-    Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy
+    Predicate_Compile_Core.code_pred_cmd modes rpred raw_const lthy
 
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
 
-val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred"]
+val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred", "mode"]
 
 local structure P = OuterParse
 in
 
+val opt_modes =
+  Scan.optional (P.$$$ "(" |-- P.$$$ "mode" |-- P.$$$ ":" |--
+   P.enum1 "," (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]")
+  --| P.$$$ ")" >> SOME) NONE
+
 val _ = OuterSyntax.local_theory_to_proof "code_pred"
   "prove equations for predicate specified by intro/elim rules"
-  OuterKeyword.thy_goal (P.opt_keyword "inductify_all" -- P.opt_keyword "rpred" -- P.term_group >> code_pred_cmd)
+  OuterKeyword.thy_goal (opt_modes --
+    P.opt_keyword "inductify_all" -- P.opt_keyword "rpred" -- P.term_group >> code_pred_cmd)
 
 end
 

--- 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: bool -> string -> Proof.context -> Proof.state
-  val code_pred_cmd: bool -> string -> Proof.context -> Proof.state
+  val code_pred: int list list option -> bool -> string -> Proof.context -> Proof.state
+  val code_pred_cmd: int list list option -> bool -> 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 : string list -> theory -> theory
+  val add_equations : int list list option -> 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 : string list -> theory -> theory
-  val add_sizelim_equations : string list -> theory -> theory
+  val add_quickcheck_equations : int list list option -> string list -> theory -> theory
+  val add_sizelim_equations : int list list option -> 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
@@ -197,6 +197,13 @@
 
 (** data structures **)
 
+(* new datatype for modes: *)
+(*
+datatype instantiation = Input | Output
+type arg_mode = Tuple of instantiation list | Atom of instantiation | HigherOrderMode of mode
+type mode = arg_mode list
+type tmode = Mode of mode * 
+*)
 type smode = (int * int list option) list
 type mode = smode option list * smode;
 datatype tmode = Mode of mode * smode * tmode option list;
@@ -2193,7 +2200,8 @@
     fun check_arg arg = case HOLogic.strip_tupleT (fastype_of arg) of
       (Ts as _ :: _ :: _) =>
         if (length (HOLogic.strip_tuple arg) = length Ts) then true
-        else error ("Format of introduction rule is invalid: tuples must be expanded:"
+        else
+        error ("Format of introduction rule is invalid: tuples must be expanded:"
         ^ (Syntax.string_of_term_global thy arg) ^ " in " ^
         (Display.string_of_thm_global thy intro)) 
       | _ => true
@@ -2210,16 +2218,21 @@
 
 (** main function of predicate compiler **)
 
-fun add_equations_of steps prednames thy =
+fun add_equations_of steps expected_modes prednames thy =
   let
     val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
     val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
-    val _ = map (check_format_of_intro_rule thy) (maps (intros_of 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 _ = Output.tracing "Infering modes..."
     val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses 
-    val modes = map (fn (p, mps) => (p, map fst mps)) moded_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 _ = print_modes modes
     val _ = print_moded_clauses thy moded_clauses
     val _ = Output.tracing "Defining executable functions..."
@@ -2258,7 +2271,7 @@
 
 fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) 
   
-fun gen_add_equations steps names thy =
+fun gen_add_equations steps expected_modes names thy =
   let
     val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy
       |> Theory.checkpoint;
@@ -2267,7 +2280,7 @@
     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 preds thy else thy)
+        if #are_not_defined steps thy preds then add_equations_of steps expected_modes preds thy else thy)
       scc thy' |> Theory.checkpoint
   in thy'' end
 
@@ -2323,7 +2336,7 @@
   (*FIXME why distinguished attribute for cases?*)
 
 (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
-fun generic_code_pred prep_const rpred raw_const lthy =
+fun generic_code_pred prep_const modes rpred raw_const lthy =
   let
     val thy = ProofContext.theory_of lthy
     val const = prep_const thy raw_const
@@ -2353,9 +2366,9 @@
       in
         goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
           (if rpred then
-            (add_equations [const] #>
-             add_sizelim_equations [const] #> add_quickcheck_equations [const])
-        else add_equations [const]))
+            (add_equations NONE [const] #>
+             add_sizelim_equations NONE [const] #> add_quickcheck_equations NONE [const])
+           else add_equations modes [const]))
       end  
   in
     Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
@@ -2442,7 +2455,6 @@
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   in Pretty.writeln p end;
 
-
 local structure P = OuterParse in
 
 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Sat Oct 24 16:55:42 2009 +0200
@@ -7,11 +7,28 @@
   | "even n \<Longrightarrow> odd (Suc n)"
   | "odd n \<Longrightarrow> even (Suc n)"
 
-code_pred even .
+code_pred (mode: [], [1]) even .
 
 thm odd.equation
 thm even.equation
+(*
+lemma unit: "unit_case f = (\<lambda>x. f)"
+apply (rule ext)
+apply (case_tac x)
+apply (simp only: unit.cases)
+done
 
+lemma "even_1 (Suc (Suc n)) = even_1 n"
+thm even.equation(2)
+unfolding even.equation(1)[of "Suc (Suc n)"]
+unfolding odd.equation
+unfolding single_bind
+apply simp
+apply (simp add: unit)
+unfolding bind_single
+apply (rule refl)
+done
+*)
 values "{x. even 2}"
 values "{x. odd 2}"
 values 10 "{n. even n}"
@@ -21,7 +38,9 @@
     "append [] xs xs"
   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
-code_pred append .
+code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
+thm append.equation
+
 code_pred (inductify_all) (rpred) append .
 
 thm append.equation
@@ -57,7 +76,7 @@
 
 code_pred (inductify_all) tupled_append' .
 thm tupled_append'.equation
-(* TODO: Missing a few modes! *)
+(* TODO: Modeanalysis returns mode [2] ?? *)
 
 inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
 where
@@ -68,7 +87,7 @@
 
 code_pred (inductify_all) tupled_append'' .
 thm tupled_append''.equation
-(* TODO: Missing a few modes *)
+(* TODO: Modeanalysis returns mode [2] ?? *)
 
 inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
 where
@@ -78,9 +97,7 @@
 code_pred (inductify_all) tupled_append''' .
 thm tupled_append'''.equation
 (* TODO: Missing a few modes *)
-thm fst_conv snd_conv
-thm map_of.simps
-term "map_of"
+
 inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
 where
   "map_ofP ((a, b)#xs) a b"
@@ -367,6 +384,33 @@
 code_pred (inductify_all) Domain .
 thm Domain.equation
 
+section {* List functions *}
+
+code_pred (inductify_all) length .
+thm size_listP.equation
+
+code_pred (inductify_all) concat .
+thm concatP.equation
+
+code_pred (inductify_all) hd .
+code_pred (inductify_all) tl .
+code_pred (inductify_all) last .
+code_pred (inductify_all) butlast .
+(*code_pred (inductify_all) listsum .*)
+code_pred (inductify_all) take .
+code_pred (inductify_all) drop .
+code_pred (inductify_all) zip .
+code_pred (inductify_all) upt .
+code_pred set sorry
+code_pred (inductify_all) remdups .
+code_pred (inductify_all) remove1 .
+code_pred (inductify_all) removeAll .
+code_pred (inductify_all) distinct .
+code_pred (inductify_all) replicate .
+code_pred (inductify_all) splice .
+code_pred (inductify_all) List.rev .
+thm revP.equation
+
 
 section {* Context Free Grammar *}