# HG changeset patch # User bulwahn # Date 1256729342 -3600 # Node ID 1d93dd8a02c9a8a6e5837333ac24ea569a686b49 # Parent 9d03957622a2d3f421d644098052a20ec1dc9751 moved datatype mode and string functions to the auxillary structure diff -r 9d03957622a2 -r 1d93dd8a02c9 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Oct 28 12:29:01 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Oct 28 12:29:02 2009 +0100 @@ -9,8 +9,28 @@ structure Predicate_Compile_Aux = struct + +(* mode *) + type smode = (int * int list option) list type mode = smode option list * smode +datatype tmode = Mode of mode * smode * tmode option list; + +fun string_of_smode js = + commas (map + (fn (i, is) => + string_of_int i ^ (case is of NONE => "" + | SOME is => "p" ^ enclose "[" "]" (commas (map string_of_int is)))) js) + +fun string_of_mode (iss, is) = space_implode " -> " (map + (fn NONE => "X" + | SOME js => enclose "[" "]" (string_of_smode js)) + (iss @ [SOME is])); + +fun string_of_tmode (Mode (predmode, termmode, param_modes)) = + "predmode: " ^ (string_of_mode predmode) ^ + (if null param_modes then "" else + "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes)) (* general syntactic functions *) diff -r 9d03957622a2 -r 1d93dd8a02c9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 28 12:29:01 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 28 12:29:02 2009 +0100 @@ -9,24 +9,20 @@ val setup: theory -> theory 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 register_predicate : (string * thm list * thm * int) -> theory -> theory val register_intros : string * thm list -> theory -> theory val is_registered : theory -> string -> bool - val predfun_intro_of: theory -> string -> mode -> thm - val predfun_elim_of: theory -> string -> mode -> thm - val predfun_name_of: theory -> string -> mode -> string + val predfun_intro_of: theory -> string -> Predicate_Compile_Aux.mode -> thm + val predfun_elim_of: theory -> string -> Predicate_Compile_Aux.mode -> thm + val predfun_name_of: theory -> string -> Predicate_Compile_Aux.mode -> string val all_preds_of : theory -> string list - val modes_of: theory -> string -> mode list - val depth_limited_modes_of: theory -> string -> mode list - val depth_limited_function_name_of : theory -> string -> mode -> string - val generator_modes_of: theory -> string -> mode list - val generator_name_of : theory -> string -> mode -> string - val all_modes_of : theory -> (string * mode list) list - val all_generator_modes_of : theory -> (string * mode list) list - val string_of_mode : mode -> string + val modes_of: theory -> string -> Predicate_Compile_Aux.mode list + val depth_limited_modes_of: theory -> string -> Predicate_Compile_Aux.mode list + val depth_limited_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string + val generator_modes_of: theory -> string -> Predicate_Compile_Aux.mode list + val generator_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string + val all_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list + val all_generator_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list val intros_of: theory -> string -> thm list val nparams_of: theory -> string -> int val add_intro: thm -> theory -> theory @@ -138,9 +134,6 @@ 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; fun gen_split_smode (mk_tuple, strip_tuple) smode ts = let @@ -174,22 +167,6 @@ val split_mode = gen_split_mode split_smode val split_modeT = gen_split_mode split_smodeT -fun string_of_smode js = - commas (map - (fn (i, is) => - string_of_int i ^ (case is of NONE => "" - | SOME is => "p" ^ enclose "[" "]" (commas (map string_of_int is)))) js) - -fun string_of_mode (iss, is) = space_implode " -> " (map - (fn NONE => "X" - | SOME js => enclose "[" "]" (string_of_smode js)) - (iss @ [SOME is])); - -fun string_of_tmode (Mode (predmode, termmode, param_modes)) = - "predmode: " ^ (string_of_mode predmode) ^ - (if null param_modes then "" else - "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes)) - datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term | Generator of (string * typ);