1024 |> single |
1024 |> single |
1025 end; |
1025 end; |
1026 |
1026 |
1027 fun prove_code disc_eqns sel_eqns maybe_exh ctr_alist ctr_specs = |
1027 fun prove_code disc_eqns sel_eqns maybe_exh ctr_alist ctr_specs = |
1028 let |
1028 let |
1029 val fun_data = |
1029 val maybe_fun_data = |
1030 (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns, |
1030 (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns, |
1031 find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns) |
1031 find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns) |
1032 |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x)) |
1032 |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x)) |
1033 ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE)) |
1033 ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE)) |
1034 |> merge_options; |
1034 |> merge_options; |
1035 in |
1035 in |
1036 (case fun_data of |
1036 (case maybe_fun_data of |
1037 NONE => [] |
1037 NONE => [] |
1038 | SOME (fun_name, fun_T, fun_args, maybe_rhs) => |
1038 | SOME (fun_name, fun_T, fun_args, maybe_rhs) => |
1039 let |
1039 let |
1040 val bound_Ts = List.rev (map fastype_of fun_args); |
1040 val bound_Ts = List.rev (map fastype_of fun_args); |
1041 |
1041 |
1042 val lhs = list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); |
1042 val lhs = |
|
1043 list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); |
1043 val maybe_rhs_info = |
1044 val maybe_rhs_info = |
1044 (case maybe_rhs of |
1045 (case maybe_rhs of |
1045 SOME rhs => |
1046 SOME rhs => |
1046 let |
1047 let |
1047 val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs; |
1048 val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs; |
1065 in |
1066 in |
1066 SOME (prems, t) |
1067 SOME (prems, t) |
1067 end; |
1068 end; |
1068 val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs; |
1069 val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs; |
1069 in |
1070 in |
1070 if exists is_none maybe_ctr_conds_argss then NONE else |
1071 let |
1071 let |
1072 val rhs = (if exhaustive |
1072 val rhs = (if exhaustive then |
1073 orelse forall is_some maybe_ctr_conds_argss |
1073 split_last maybe_ctr_conds_argss ||> snd o the |
1074 andalso exists #auto_gen disc_eqns then |
1074 else |
1075 split_last (map_filter I maybe_ctr_conds_argss) ||> snd |
1075 Const (@{const_name Code.abort}, @{typ String.literal} --> |
1076 else |
1076 (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ |
1077 Const (@{const_name Code.abort}, @{typ String.literal} --> |
1077 HOLogic.mk_literal fun_name $ |
1078 (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ |
1078 absdummy @{typ unit} (incr_boundvars 1 lhs) |
1079 HOLogic.mk_literal fun_name $ |
1079 |> pair maybe_ctr_conds_argss) |
1080 absdummy @{typ unit} (incr_boundvars 1 lhs) |
1080 |-> fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t) |
1081 |> pair (map_filter I maybe_ctr_conds_argss)) |
1081 in SOME (rhs, rhs, map snd ctr_alist) end |
1082 |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u) |
|
1083 in SOME (rhs, rhs, map snd ctr_alist) end |
1082 end); |
1084 end); |
1083 in |
1085 in |
1084 (case maybe_rhs_info of |
1086 (case maybe_rhs_info of |
1085 NONE => [] |
1087 NONE => [] |
1086 | SOME (rhs, raw_rhs, ctr_thms) => |
1088 | SOME (rhs, raw_rhs, ctr_thms) => |