276 val has_elim = is_some o #elim oo the_pred_data |
276 val has_elim = is_some o #elim oo the_pred_data |
277 |
277 |
278 fun function_names_of compilation ctxt name = |
278 fun function_names_of compilation ctxt name = |
279 case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of |
279 case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of |
280 NONE => error ("No " ^ string_of_compilation compilation |
280 NONE => error ("No " ^ string_of_compilation compilation |
281 ^ "functions defined for predicate " ^ quote name) |
281 ^ " functions defined for predicate " ^ quote name) |
282 | SOME fun_names => fun_names |
282 | SOME fun_names => fun_names |
283 |
283 |
284 fun function_name_of compilation ctxt name mode = |
284 fun function_name_of compilation ctxt name mode = |
285 case AList.lookup eq_mode |
285 case AList.lookup eq_mode |
286 (function_names_of compilation ctxt name) mode of |
286 (function_names_of compilation ctxt name) mode of |
846 additional_arguments = additional_arguments, wrap_compilation = wrap_compilation, |
846 additional_arguments = additional_arguments, wrap_compilation = wrap_compilation, |
847 transform_additional_arguments = transform_additional_arguments}) |
847 transform_additional_arguments = transform_additional_arguments}) |
848 |
848 |
849 end; |
849 end; |
850 |
850 |
851 fun unlimited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq = |
851 fun unlimited_compfuns_of true New_Pos_Random_DSeq = |
852 New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns |
852 New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns |
853 | unlimited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq = |
853 | unlimited_compfuns_of false New_Pos_Random_DSeq = |
854 New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns |
854 New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns |
855 |
855 | unlimited_compfuns_of true Pos_Generator_DSeq = |
|
856 New_Pos_DSequence_CompFuns.depth_unlimited_compfuns |
|
857 | unlimited_compfuns_of false Pos_Generator_DSeq = |
|
858 New_Neg_DSequence_CompFuns.depth_unlimited_compfuns |
|
859 | unlimited_compfuns_of _ c = |
|
860 raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c) |
|
861 |
856 fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq = |
862 fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq = |
857 New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns |
863 New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns |
858 | limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq = |
864 | limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq = |
859 New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns |
865 New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns |
860 |
866 | limited_compfuns_of true Pos_Generator_DSeq = |
|
867 New_Pos_DSequence_CompFuns.depth_limited_compfuns |
|
868 | limited_compfuns_of false Pos_Generator_DSeq = |
|
869 New_Neg_DSequence_CompFuns.depth_limited_compfuns |
|
870 | limited_compfuns_of _ c = |
|
871 raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c) |
861 |
872 |
862 val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers |
873 val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers |
863 { |
874 { |
864 compilation = Depth_Limited, |
875 compilation = Depth_Limited, |
865 function_name_prefix = "depth_limited_", |
876 function_name_prefix = "depth_limited_", |
995 val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers |
1006 val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers |
996 { |
1007 { |
997 compilation = DSeq, |
1008 compilation = DSeq, |
998 function_name_prefix = "dseq_", |
1009 function_name_prefix = "dseq_", |
999 compfuns = DSequence_CompFuns.compfuns, |
1010 compfuns = DSequence_CompFuns.compfuns, |
1000 mk_random = (fn _ => error "no random generation"), |
1011 mk_random = (fn _ => error "no random generation in dseq"), |
1001 modify_funT = I, |
1012 modify_funT = I, |
1002 additional_arguments = K [], |
1013 additional_arguments = K [], |
1003 wrap_compilation = K (K (K (K (K I)))) |
1014 wrap_compilation = K (K (K (K (K I)))) |
1004 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
1015 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
1005 transform_additional_arguments = K I : (indprem -> term list -> term list) |
1016 transform_additional_arguments = K I : (indprem -> term list -> term list) |
1075 wrap_compilation = K (K (K (K (K I)))) |
1086 wrap_compilation = K (K (K (K (K I)))) |
1076 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
1087 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
1077 transform_additional_arguments = K I : (indprem -> term list -> term list) |
1088 transform_additional_arguments = K I : (indprem -> term list -> term list) |
1078 } |
1089 } |
1079 |
1090 |
|
1091 val pos_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers |
|
1092 { |
|
1093 compilation = Pos_Generator_DSeq, |
|
1094 function_name_prefix = "generator_dseq_", |
|
1095 compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns, |
|
1096 mk_random = |
|
1097 (fn T => fn additional_arguments => |
|
1098 let |
|
1099 val small_lazy = |
|
1100 Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"}, |
|
1101 @{typ "Int.int"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T])) |
|
1102 in |
|
1103 absdummy (@{typ code_numeral}, small_lazy $ HOLogic.mk_number @{typ int} 3) |
|
1104 end |
|
1105 ), |
|
1106 modify_funT = I, |
|
1107 additional_arguments = K [], |
|
1108 wrap_compilation = K (K (K (K (K I)))) |
|
1109 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
|
1110 transform_additional_arguments = K I : (indprem -> term list -> term list) |
|
1111 } |
|
1112 |
|
1113 val neg_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers |
|
1114 { |
|
1115 compilation = Neg_Generator_DSeq, |
|
1116 function_name_prefix = "generator_dseq_neg_", |
|
1117 compfuns = New_Neg_DSequence_CompFuns.depth_limited_compfuns, |
|
1118 mk_random = (fn _ => error "no random generation"), |
|
1119 modify_funT = I, |
|
1120 additional_arguments = K [], |
|
1121 wrap_compilation = K (K (K (K (K I)))) |
|
1122 : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), |
|
1123 transform_additional_arguments = K I : (indprem -> term list -> term list) |
|
1124 } |
|
1125 |
1080 fun negative_comp_modifiers_of comp_modifiers = |
1126 fun negative_comp_modifiers_of comp_modifiers = |
1081 (case Comp_Mod.compilation comp_modifiers of |
1127 (case Comp_Mod.compilation comp_modifiers of |
1082 Pos_Random_DSeq => neg_random_dseq_comp_modifiers |
1128 Pos_Random_DSeq => neg_random_dseq_comp_modifiers |
1083 | Neg_Random_DSeq => pos_random_dseq_comp_modifiers |
1129 | Neg_Random_DSeq => pos_random_dseq_comp_modifiers |
1084 | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers |
1130 | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers |
1085 | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers |
1131 | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers |
|
1132 | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers |
|
1133 | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers |
1086 | c => comp_modifiers) |
1134 | c => comp_modifiers) |
1087 |
1135 |
1088 (** mode analysis **) |
1136 (** mode analysis **) |
1089 |
1137 |
1090 type mode_analysis_options = |
1138 type mode_analysis_options = |
3097 add_code_equations = K (K I), |
3145 add_code_equations = K (K I), |
3098 comp_modifiers = new_pos_random_dseq_comp_modifiers, |
3146 comp_modifiers = new_pos_random_dseq_comp_modifiers, |
3099 use_generators = true, |
3147 use_generators = true, |
3100 qname = "new_random_dseq_equation"}) |
3148 qname = "new_random_dseq_equation"}) |
3101 |
3149 |
|
3150 val add_generator_dseq_equations = gen_add_equations |
|
3151 (Steps { |
|
3152 define_functions = |
|
3153 fn options => fn preds => fn (s, modes) => |
|
3154 let |
|
3155 val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes |
|
3156 val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes |
|
3157 in |
|
3158 define_functions pos_generator_dseq_comp_modifiers New_Pos_DSequence_CompFuns.depth_limited_compfuns |
|
3159 options preds (s, pos_modes) |
|
3160 #> define_functions neg_generator_dseq_comp_modifiers New_Neg_DSequence_CompFuns.depth_limited_compfuns |
|
3161 options preds (s, neg_modes) |
|
3162 end, |
|
3163 prove = prove_by_skip, |
|
3164 add_code_equations = K (K I), |
|
3165 comp_modifiers = pos_generator_dseq_comp_modifiers, |
|
3166 use_generators = true, |
|
3167 qname = "generator_dseq_equation"}) |
|
3168 |
3102 (** user interface **) |
3169 (** user interface **) |
3103 |
3170 |
3104 (* code_pred_intro attribute *) |
3171 (* code_pred_intro attribute *) |
3105 |
3172 |
3106 fun attrib' f opt_case_name = |
3173 fun attrib' f opt_case_name = |
3158 | Pos_Random_DSeq => add_random_dseq_equations |
3225 | Pos_Random_DSeq => add_random_dseq_equations |
3159 | Depth_Limited => add_depth_limited_equations |
3226 | Depth_Limited => add_depth_limited_equations |
3160 | Random => add_random_equations |
3227 | Random => add_random_equations |
3161 | Depth_Limited_Random => add_depth_limited_random_equations |
3228 | Depth_Limited_Random => add_depth_limited_random_equations |
3162 | New_Pos_Random_DSeq => add_new_random_dseq_equations |
3229 | New_Pos_Random_DSeq => add_new_random_dseq_equations |
|
3230 | Pos_Generator_DSeq => add_generator_dseq_equations |
3163 | compilation => error ("Compilation not supported") |
3231 | compilation => error ("Compilation not supported") |
3164 ) options [const])) |
3232 ) options [const])) |
3165 end |
3233 end |
3166 in |
3234 in |
3167 Proof.theorem NONE after_qed (map (single o (rpair [])) cases_rules) lthy'' |
3235 Proof.theorem NONE after_qed (map (single o (rpair [])) cases_rules) lthy'' |