# HG changeset patch # User bulwahn # Date 1257491518 -3600 # Node ID e96a0c52d74bfb9435de456c4164adde14abb585 # Parent a15a2f7f7560a0d12faf4e6549652e3cf6d0dfca renamed generator to random_function in the predicate compiler diff -r a15a2f7f7560 -r e96a0c52d74b 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 @@ -21,10 +21,10 @@ 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 random_modes_of: theory -> string -> Predicate_Compile_Aux.mode list + val random_function_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 all_random_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 @@ -207,20 +207,20 @@ elim : thm option, nparams : int, functions : bool * (mode * predfun_data) list, - generators : bool * (mode * function_data) list, (*TODO: maybe rename to random_functions *) + random_functions : bool * (mode * function_data) list, depth_limited_functions : bool * (mode * function_data) list, annotated_functions : bool * (mode * function_data) list }; fun rep_pred_data (PredData data) = data; fun mk_pred_data ((intros, elim, nparams), - (functions, generators, depth_limited_functions, annotated_functions)) = + (functions, random_functions, depth_limited_functions, annotated_functions)) = PredData {intros = intros, elim = elim, nparams = nparams, - functions = functions, generators = generators, + functions = functions, random_functions = random_functions, depth_limited_functions = depth_limited_functions, annotated_functions = annotated_functions} fun map_pred_data f (PredData {intros, elim, nparams, - functions, generators, depth_limited_functions, annotated_functions}) = - mk_pred_data (f ((intros, elim, nparams), (functions, generators, + functions, random_functions, depth_limited_functions, annotated_functions}) = + mk_pred_data (f ((intros, elim, nparams), (functions, random_functions, depth_limited_functions, annotated_functions))) fun eq_option eq (NONE, NONE) = true @@ -287,27 +287,23 @@ val predfun_elim_of = #elim ooo the_predfun_data -fun lookup_generator_data thy name mode = +fun lookup_random_function_data thy name mode = Option.map rep_function_data - (AList.lookup (op =) (snd (#generators (the_pred_data thy name))) mode) + (AList.lookup (op =) (snd (#random_functions (the_pred_data thy name))) mode) -fun the_generator_data thy name mode = case lookup_generator_data thy name mode - of NONE => error ("No generator defined for mode " ^ string_of_mode mode ^ - " of predicate " ^ name) +fun the_random_function_data thy name mode = case lookup_random_function_data thy name mode of + NONE => error ("No random function defined for mode " ^ string_of_mode mode ^ + " of predicate " ^ name) | SOME data => data -val generator_name_of = #name ooo the_generator_data +val random_function_name_of = #name ooo the_random_function_data -(* TODO: duplicated function *) -val generator_modes_of = (map fst) o snd o #generators oo the_pred_data +val random_modes_of = (map fst) o snd o #random_functions oo the_pred_data -(* TODO: duplicated function *) -val random_modes_of = (map fst) o snd o #generators oo the_pred_data +val defined_random_functions = fst o #random_functions oo the_pred_data -val defined_random_functions = fst o #generators oo the_pred_data - -fun all_generator_modes_of thy = - map (fn name => (name, generator_modes_of thy name)) (all_preds_of thy) +fun all_random_modes_of thy = + map (fn name => (name, random_modes_of thy name)) (all_preds_of thy) fun lookup_depth_limited_function_data thy name mode = Option.map rep_function_data @@ -724,7 +720,7 @@ (mk_casesrule (ProofContext.init thy) pred nparams pre_intros) in register_predicate (constname, pre_intros, pre_elim, nparams) thy end -fun set_generator_name pred mode name = +fun set_random_function_name pred mode name = let val set = (apsnd o apsnd4) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y)) in @@ -904,8 +900,8 @@ 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_generator_of compfuns thy (name, T) mode = - Const (generator_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) (* Mode analysis *) @@ -1135,7 +1131,7 @@ let val prednames = map fst clauses val extra_modes' = all_modes_of thy - val gen_modes = all_generator_modes_of thy + val gen_modes = all_random_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name) val starting_modes = remove_from extra_modes' all_modes fun eq_mode (m1, m2) = (m1 = m2) @@ -1653,11 +1649,11 @@ fold create_definition modes thy end; -fun generator_funT_of (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 SOME is => generator_funT_of ([], is) | NONE => I) iss paramTs + 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)) @@ -1669,10 +1665,10 @@ fun create_definition mode thy = let val mode_cname = create_constname_of_mode thy "gen_" name mode - val funT = generator_funT_of mode T + 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_generator_name name mode mode_cname + |> set_random_function_name name mode mode_cname end; in fold create_definition modes thy @@ -2411,8 +2407,8 @@ } val random_comp_modifiers = Comp_Mod.Comp_Modifiers - {const_name_of = generator_name_of, - funT_of = K generator_funT_of : (compilation_funs -> mode -> typ -> typ), + {const_name_of = random_function_name_of, + 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)))) : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), @@ -2553,7 +2549,7 @@ (fn (i, t) => case t of Bound j => if j < length Ts then NONE else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*) val user_mode' = map (rpair NONE) user_mode - val all_modes_of = if random then all_generator_modes_of else all_modes_of + val all_modes_of = if random then all_random_modes_of else all_modes_of fun fits_to is NONE = true | fits_to is (SOME pm) = (is = pm) fun valid ((SOME (Mode (_, is, ms))) :: ms') (pm :: pms) = @@ -2583,7 +2579,7 @@ if annotated then annotated_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers val mk_fun_of = - if random then mk_generator_of else + 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