# HG changeset patch
# User bulwahn
# Date 1270046681 -7200
# Node ID f8297ebb21a7c63535c49ad7640db9cfa24a265f
# Parent  c3946372f5563d0e4187ee2629ce062857e6d5da
adding signature to Predicate_Compile_Aux; tuning Predicate_Compile_Aux structure

diff -r c3946372f556 -r f8297ebb21a7 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 31 16:44:41 2010 +0200
@@ -4,9 +4,138 @@
 Auxilary functions for predicate compiler.
 *)
 
-(* FIXME proper signature! *)
+signature PREDICATE_COMPILE_AUX =
+sig
+  (* general functions *)
+  val apfst3 : ('a -> 'd) -> 'a * 'b * 'c -> 'd * 'b * 'c
+  val apsnd3 : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c
+  val aptrd3 : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd
+  val find_indices : ('a -> bool) -> 'a list -> int list
+  val assert : bool -> unit
+  (* mode *)
+  datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
+  val eq_mode : mode * mode -> bool
+  val list_fun_mode : mode list -> mode
+  val strip_fun_mode : mode -> mode list
+  val dest_fun_mode : mode -> mode list
+  val dest_tuple_mode : mode -> mode list
+  val all_modes_of_typ : typ -> mode list
+  val all_smodes_of_typ : typ -> mode list
+  val fold_map_aterms_prodT : ('a -> 'a -> 'a) -> (typ -> 'b -> 'a * 'b) -> typ -> 'b -> 'a * 'b
+  val map_filter_prod : (term -> term option) -> term -> term option
+  val replace_ho_args : mode -> term list -> term list -> term list
+  val ho_arg_modes_of : mode -> mode list
+  val ho_argsT_of : mode -> typ list -> typ list
+  val ho_args_of : mode -> term list -> term list
+  val split_map_mode : (mode -> term -> term option * term option)
+    -> mode -> term list -> term list * term list
+  val split_map_modeT : (mode -> typ -> typ option * typ option)
+    -> mode -> typ list -> typ list * typ list
+  val split_mode : mode -> term list -> term list * term list
+  val split_modeT' : mode -> typ list -> typ list * typ list
+  val string_of_mode : mode -> string
+  val ascii_string_of_mode : mode -> string
+  (* premises *)
+  datatype indprem = Prem of term | Negprem of term | Sidecond of term
+    | Generator of (string * typ)
+  (* general syntactic functions *)
+  val conjuncts : term -> term list
+  val is_equationlike : thm -> bool
+  val is_pred_equation : thm -> bool
+  val is_intro : string -> thm -> bool
+  val is_predT : typ -> bool
+  val is_constrt : theory -> term -> bool
+  val is_constr : Proof.context -> string -> bool
+  val focus_ex : term -> Name.context -> ((string * typ) list * term) * Name.context
+  val strip_all : term -> (string * typ) list * term
+  (* introduction rule combinators *)
+  val map_atoms : (term -> term) -> term -> term
+  val fold_atoms : (term -> 'a -> 'a) -> term -> 'a -> 'a
+  val fold_map_atoms : (term -> 'a -> term * 'a) -> term -> 'a -> term * 'a
+  val maps_premises : (term -> term list) -> term -> term
+  val map_concl : (term -> term) -> term -> term
+  val map_term : theory -> (term -> term) -> thm -> thm
+  (* split theorems of case expressions *)
+  val prepare_split_thm : Proof.context -> thm -> thm
+  val find_split_thm : theory -> term -> thm option
+  (* datastructures and setup for generic compilation *)
+  datatype compilation_funs = CompilationFuns of {
+    mk_predT : typ -> typ,
+    dest_predT : typ -> typ,
+    mk_bot : typ -> term,
+    mk_single : term -> term,
+    mk_bind : term * term -> term,
+    mk_sup : term * term -> term,
+    mk_if : term -> term,
+    mk_not : term -> term,
+    mk_map : typ -> typ -> term -> term -> term
+  };
+  val mk_predT : compilation_funs -> typ -> typ
+  val dest_predT : compilation_funs -> typ -> typ
+  val mk_bot : compilation_funs -> typ -> term
+  val mk_single : compilation_funs -> term -> term
+  val mk_bind : compilation_funs -> term * term -> term
+  val mk_sup : compilation_funs -> term * term -> term
+  val mk_if : compilation_funs -> term -> term
+  val mk_not : compilation_funs -> term -> term
+  val mk_map : compilation_funs -> typ -> typ -> term -> term -> term
+  val funT_of : compilation_funs -> mode -> typ -> typ
+  (* Different compilations *)
+  datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
+    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
+  val negative_compilation_of : compilation -> compilation
+  val compilation_for_polarity : bool -> compilation -> compilation
+  val string_of_compilation : compilation -> string
+  val compilation_names : (string * compilation) list
+  val non_random_compilations : compilation list
+  val random_compilations : compilation list
+  (* Different options for compiler *)
+  datatype options = Options of {  
+    expected_modes : (string * mode list) option,
+    proposed_modes : (string * mode list) option,
+    proposed_names : ((string * mode) * string) list,
+    show_steps : bool,
+    show_proof_trace : bool,
+    show_intermediate_results : bool,
+    show_mode_inference : bool,
+    show_modes : bool,
+    show_compilation : bool,
+    show_caught_failures : bool,
+    skip_proof : bool,
+    no_topmost_reordering : bool,
+    function_flattening : bool,
+    fail_safe_function_flattening : bool,
+    no_higher_order_predicate : string list,
+    inductify : bool,
+    compilation : compilation
+  };
+  val expected_modes : options -> (string * mode list) option
+  val proposed_modes : options -> (string * mode list) option
+  val proposed_names : options -> string -> mode -> string option
+  val show_steps : options -> bool
+  val show_proof_trace : options -> bool
+  val show_intermediate_results : options -> bool
+  val show_mode_inference : options -> bool
+  val show_modes : options -> bool
+  val show_compilation : options -> bool
+  val show_caught_failures : options -> bool
+  val skip_proof : options -> bool
+  val no_topmost_reordering : options -> bool
+  val function_flattening : options -> bool
+  val fail_safe_function_flattening : options -> bool
+  val no_higher_order_predicate : options -> string list
+  val is_inductify : options -> bool
+  val compilation : options -> compilation
+  val default_options : options
+  val bool_options : string list
+  val print_step : options -> string -> unit
+  (* simple transformations *)
+  val expand_tuples : theory -> thm -> thm
+  val eta_contract_ho_arguments : theory -> thm -> thm
+  val remove_equalities : theory -> thm -> thm
+end;
 
-structure Predicate_Compile_Aux =
+structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
 struct
 
 (* general functions *)
@@ -54,13 +183,13 @@
   | strip_fun_mode Bool = []
   | strip_fun_mode _ = raise Fail "Bad mode for strip_fun_mode"
 
+(* name: strip_fun_mode? *)
 fun dest_fun_mode (Fun (mode, mode')) = mode :: dest_fun_mode mode'
   | dest_fun_mode mode = [mode]
 
 fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode'
   | dest_tuple_mode _ = []
 
-
 fun all_modes_of_typ' (T as Type ("fun", _)) = 
   let
     val (S, U) = strip_type T
@@ -98,7 +227,7 @@
     if U = HOLogic.boolT then
       fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool]
     else
-      raise Fail "all_smodes_of_typ: invalid type for predicate"
+      raise Fail "invalid type for predicate"
   end
 
 fun ho_arg_modes_of mode =
@@ -113,7 +242,7 @@
 fun ho_args_of mode ts =
   let
     fun ho_arg (Fun _) (SOME t) = [t]
-      | ho_arg (Fun _) NONE = error "ho_arg_of"
+      | ho_arg (Fun _) NONE = raise Fail "mode and term do not match"
       | ho_arg (Pair (m1, m2)) (SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) =
           ho_arg m1 (SOME t1) @ ho_arg m2 (SOME t2)
       | ho_arg (Pair (m1, m2)) NONE = ho_arg m1 NONE @ ho_arg m2 NONE
@@ -331,6 +460,8 @@
 
 val is_constr = Code.is_constr o ProofContext.theory_of;
 
+fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
+
 fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
   let
     val (xTs, t') = strip_ex t
@@ -350,8 +481,6 @@
 
 (* introduction rule combinators *)
 
-(* combinators to apply a function to all literals of an introduction rules *)
-
 fun map_atoms f intro = 
   let
     val (literals, head) = Logic.strip_horn intro
@@ -412,9 +541,6 @@
 fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype_Data.info_of_case thy name)
   | find_split_thm thy _ = NONE
 
-fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
-
-
 (* lifting term operations to theorems *)
 
 fun map_term thy f th =
@@ -576,7 +702,9 @@
 fun print_step options s =
   if show_steps options then tracing s else ()
 
-(* tuple processing *)
+(* simple transformations *)
+
+(** tuple processing **)
 
 fun expand_tuples thy intro =
   let
@@ -631,7 +759,7 @@
     intro'''''
   end
 
-(* eta contract higher-order arguments *)
+(** eta contract higher-order arguments **)
 
 fun eta_contract_ho_arguments thy intro =
   let
@@ -640,7 +768,7 @@
     map_term thy (map_concl f o map_atoms f) intro
   end
 
-(* remove equalities *)
+(** remove equalities **)
 
 fun remove_equalities thy intro =
   let