# HG changeset patch # User bulwahn # Date 1257491518 -3600 # Node ID 0df4f6e46e5e789264eb3d9397e006e388cd0674 # Parent e96a0c52d74bfb9435de456c4164adde14abb585 made definition of functions generically for the different instances diff -r e96a0c52d74b -r 0df4f6e46e5e src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 06 08:11:58 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 06 08:11:58 2009 +0100 @@ -871,6 +871,15 @@ (* function types and names of different compilations *) +fun funT_of compfuns (iss, is) T = + let + val Ts = binder_types T + val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts + val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs + in + (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs)) + end; + fun depth_limited_funT_of compfuns (iss, is) T = let val Ts = binder_types T @@ -882,26 +891,15 @@ ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs)) end; -fun funT_of compfuns (iss, is) T = +fun random_function_funT_of (iss, is) T = let val Ts = binder_types T val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs + val paramTs' = map2 (fn SOME is => random_function_funT_of ([], is) | NONE => I) iss paramTs in - (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs)) - end; - -fun mk_fun_of compfuns thy (name, T) mode = - Const (predfun_name_of thy name mode, funT_of compfuns mode T) - -fun mk_annotated_fun_of compfuns thy (name, T) mode = - Const (annotated_function_name_of thy name mode, funT_of compfuns mode T) - -fun mk_depth_limited_fun_of compfuns thy (name, T) mode = - Const (depth_limited_function_name_of thy name mode, depth_limited_funT_of compfuns mode T) - -fun mk_random_fun_of compfuns thy (name, T) mode = - Const (random_function_name_of thy name mode, depth_limited_funT_of compfuns mode T) + (paramTs' @ inargTs @ [@{typ code_numeral}]) ---> + (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs)) + end (* Mode analysis *) @@ -1227,7 +1225,9 @@ datatype comp_modifiers = Comp_Modifiers of { - const_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string, + function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string, + set_function_name : string -> Predicate_Compile_Aux.mode -> string -> theory -> theory, + function_name_prefix : string, funT_of : compilation_funs -> mode -> typ -> typ, additional_arguments : string list -> term list, wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term, @@ -1236,7 +1236,9 @@ fun dest_comp_modifiers (Comp_Modifiers c) = c -val const_name_of = #const_name_of o dest_comp_modifiers +val function_name_of = #function_name_of o dest_comp_modifiers +val set_function_name = #set_function_name o dest_comp_modifiers +val function_name_prefix = #function_name_prefix o dest_comp_modifiers val funT_of = #funT_of o dest_comp_modifiers val additional_arguments = #additional_arguments o dest_comp_modifiers val wrap_compilation = #wrap_compilation o dest_comp_modifiers @@ -1302,7 +1304,7 @@ val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params) val f' = case f of - Const (name, T) => Const (Comp_Mod.const_name_of compilation_modifiers thy name mode, + Const (name, T) => Const (Comp_Mod.function_name_of compilation_modifiers thy name mode, Comp_Mod.funT_of compilation_modifiers compfuns mode T) | Free (name, T) => Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T) | _ => error ("PredicateCompiler: illegal parameter term") @@ -1316,8 +1318,7 @@ (Const (name, T), params) => let val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params) - (*val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of*) - val name' = Comp_Mod.const_name_of compilation_modifiers thy name mode + val name' = Comp_Mod.function_name_of compilation_modifiers thy name mode val T' = Comp_Mod.funT_of compilation_modifiers compfuns mode T in (list_comb (Const (name', T'), params' @ inargs @ additional_arguments)) @@ -1443,7 +1444,7 @@ mk_bot compfuns (HOLogic.mk_tupleT Us2) else foldr1 (mk_sup compfuns) cl_ts) val fun_const = - Const (Comp_Mod.const_name_of compilation_modifiers thy s mode, + Const (Comp_Mod.function_name_of compilation_modifiers thy s mode, Comp_Mod.funT_of compilation_modifiers compfuns mode T) in HOLogic.mk_Trueprop @@ -1634,62 +1635,22 @@ fold create_definition modes thy end; -fun create_definitions_of_depth_limited_functions preds (name, modes) thy = +fun define_functions comp_modifiers compfuns preds (name, modes) thy = let val T = AList.lookup (op =) preds name |> the fun create_definition mode thy = let - val mode_cname = create_constname_of_mode thy "depth_limited_" name mode - val funT = depth_limited_funT_of PredicateCompFuns.compfuns mode T + val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers + val mode_cname = create_constname_of_mode thy function_name_prefix name mode + val funT = Comp_Mod.funT_of comp_modifiers compfuns mode T in thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] - |> set_depth_limited_function_name name mode mode_cname + |> Comp_Mod.set_function_name comp_modifiers name mode mode_cname end; in fold create_definition modes thy end; -fun random_function_funT_of (iss, is) T = - let - val Ts = binder_types T - val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn SOME is => random_function_funT_of ([], is) | NONE => I) iss paramTs - in - (paramTs' @ inargTs @ [@{typ code_numeral}]) ---> - (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs)) - end - -fun random_create_definitions preds (name, modes) thy = - let - val T = AList.lookup (op =) preds name |> the - fun create_definition mode thy = - let - val mode_cname = create_constname_of_mode thy "gen_" name mode - val funT = random_function_funT_of mode T - in - thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] - |> set_random_function_name name mode mode_cname - end; - in - fold create_definition modes thy - end; - -fun create_definitions_of_annotated_functions preds (name, modes) thy = - let - val T = AList.lookup (op =) preds name |> the - fun create_definition mode thy = - let - val mode_cname = create_constname_of_mode thy "annotated_" name mode - val funT = funT_of PredicateCompFuns.compfuns mode T - in - thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] - |> set_annotated_function_name name mode mode_cname - end; - in - fold create_definition modes thy - end; - - (* Proving equivalence of term *) fun is_Type (Type _) = true @@ -2277,7 +2238,7 @@ { compile_preds : theory -> string list -> string list -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table, - create_definitions: (string * typ) list -> string * mode list -> theory -> theory, + define_functions : (string * typ) list -> string * mode list -> theory -> theory, infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list -> string list -> (string * (term list * indprem list) list) list -> moded_clause list pred_mode_table, @@ -2308,7 +2269,7 @@ val _ = print_modes options modes (*val _ = print_moded_clauses thy moded_clauses*) val _ = print_step options "Defining executable functions..." - val thy' = fold (#create_definitions (dest_steps steps) preds) modes thy + val thy' = fold (#define_functions (dest_steps steps) preds) modes thy |> Theory.checkpoint val _ = print_step options "Compiling equations..." val compiled_terms = @@ -2364,7 +2325,9 @@ (* different instantiantions of the predicate compiler *) val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers - {const_name_of = predfun_name_of : (theory -> string -> mode -> string), + {function_name_of = predfun_name_of : (theory -> string -> mode -> string), + set_function_name = (fn _ => fn _ => fn _ => I), + function_name_prefix = "", funT_of = funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = K [], wrap_compilation = K (K (K (K (K I)))) @@ -2373,8 +2336,10 @@ } val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers - {const_name_of = depth_limited_function_name_of, + {function_name_of = depth_limited_function_name_of, + set_function_name = set_depth_limited_function_name, funT_of = depth_limited_funT_of : (compilation_funs -> mode -> typ -> typ), + function_name_prefix = "depth_limited_", additional_arguments = fn names => let val [depth_name, polarity_name] = Name.variant_list names ["depth", "polarity"] @@ -2407,7 +2372,9 @@ } val random_comp_modifiers = Comp_Mod.Comp_Modifiers - {const_name_of = random_function_name_of, + {function_name_of = random_function_name_of, + set_function_name = set_random_function_name, + function_name_prefix = "random", funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})], wrap_compilation = K (K (K (K (K I)))) @@ -2416,7 +2383,9 @@ } val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers - {const_name_of = annotated_function_name_of, + {function_name_of = annotated_function_name_of, + set_function_name = set_annotated_function_name, + function_name_prefix = "annotated", funT_of = funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = K [], wrap_compilation = @@ -2427,7 +2396,7 @@ val add_equations = gen_add_equations (Steps {infer_modes = infer_modes, - create_definitions = create_definitions, + define_functions = create_definitions, compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns, prove = prove, add_code_equations = add_code_equations, @@ -2436,7 +2405,7 @@ val add_depth_limited_equations = gen_add_equations (Steps {infer_modes = infer_modes, - create_definitions = create_definitions_of_depth_limited_functions, + define_functions = define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns, compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns, prove = prove_by_skip, add_code_equations = K (K (K I)), @@ -2445,7 +2414,7 @@ val add_annotated_equations = gen_add_equations (Steps {infer_modes = infer_modes, - create_definitions = create_definitions_of_annotated_functions, + define_functions = define_functions annotated_comp_modifiers PredicateCompFuns.compfuns, compile_preds = compile_preds annotated_comp_modifiers PredicateCompFuns.compfuns, prove = prove_by_skip, add_code_equations = K (K (K I)), @@ -2454,7 +2423,7 @@ val add_quickcheck_equations = gen_add_equations (Steps {infer_modes = infer_modes_with_generator, - create_definitions = random_create_definitions, + define_functions = define_functions random_comp_modifiers RandomPredCompFuns.compfuns, compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns, prove = prove_by_skip, add_code_equations = K (K (K I)), @@ -2537,7 +2506,7 @@ Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option); (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*) -(* TODO: *) +(* TODO: make analyze_compr generic with respect to the compilation modifiers*) fun analyze_compr thy compfuns param_user_modes (depth_limit, (random, annotated)) t_compr = let val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t @@ -2578,10 +2547,6 @@ (if random then random_comp_modifiers else if annotated then annotated_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers - val mk_fun_of = - if random then mk_random_fun_of else - if annotated then mk_annotated_fun_of else - if (is_some depth_limit) then mk_depth_limited_fun_of else mk_fun_of val t_pred = compile_expr comp_modifiers compfuns thy (m, list_comb (pred, params)) inargs additional_arguments; val t_eval = if null outargs then t_pred else