1006 find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns) |
1006 find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns) |
1007 |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x)) |
1007 |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x)) |
1008 ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE)) |
1008 ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE)) |
1009 |> the o merge_options; |
1009 |> the o merge_options; |
1010 |
1010 |
|
1011 val bound_Ts = List.rev (map fastype_of fun_args); |
|
1012 |
1011 val lhs = list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); |
1013 val lhs = list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); |
1012 val maybe_rhs' = if is_some maybe_rhs then maybe_rhs else |
1014 val maybe_rhs_info = |
|
1015 (case maybe_rhs of |
|
1016 SOME rhs => |
|
1017 let |
|
1018 val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs; |
|
1019 val cond_ctrs = |
|
1020 fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs []; |
|
1021 val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs; |
|
1022 in SOME (rhs, raw_rhs, ctr_thms) end |
|
1023 | NONE => |
|
1024 let |
|
1025 fun prove_code_ctr {ctr, sels, ...} = |
|
1026 if not (exists (equal ctr o fst) ctr_alist) then NONE else |
|
1027 let |
|
1028 val prems = find_first (equal ctr o #ctr) disc_eqns |
|
1029 |> Option.map #prems |> the_default []; |
|
1030 val t = |
|
1031 filter (equal ctr o #ctr) sel_eqns |
|
1032 |> fst o finds ((op =) o apsnd #sel) sels |
|
1033 |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) |
|
1034 #-> abstract) |
|
1035 |> curry list_comb ctr; |
|
1036 in |
|
1037 SOME (prems, t) |
|
1038 end; |
|
1039 val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs; |
|
1040 in |
|
1041 if exists is_none maybe_ctr_conds_argss then NONE else |
|
1042 let |
|
1043 val rhs = fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t) |
|
1044 maybe_ctr_conds_argss |
|
1045 (Const (@{const_name Code.abort}, @{typ String.literal} --> |
|
1046 (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ |
|
1047 @{term "STR []"} $ (* FIXME *) |
|
1048 absdummy @{typ unit} (incr_boundvars 1 lhs)); |
|
1049 in SOME (rhs, rhs, map snd ctr_alist) end |
|
1050 end); |
|
1051 in |
|
1052 (case maybe_rhs_info of |
|
1053 NONE => [] |
|
1054 | SOME (rhs, raw_rhs, ctr_thms) => |
1013 let |
1055 let |
1014 fun prove_code_ctr {ctr, sels, ...} = |
|
1015 if not (exists (equal ctr o fst) ctr_alist) then NONE else |
|
1016 let |
|
1017 val prems = find_first (equal ctr o #ctr) disc_eqns |
|
1018 |> Option.map #prems |> the_default []; |
|
1019 val t = |
|
1020 filter (equal ctr o #ctr) sel_eqns |
|
1021 |> fst o finds ((op =) o apsnd #sel) sels |
|
1022 |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract) |
|
1023 |> curry list_comb ctr; |
|
1024 in |
|
1025 SOME (prems, t) |
|
1026 end; |
|
1027 val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs; |
|
1028 in |
|
1029 if exists is_none maybe_ctr_conds_argss then NONE else |
|
1030 fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t) |
|
1031 maybe_ctr_conds_argss |
|
1032 (Const (@{const_name Code.abort}, @{typ String.literal} --> |
|
1033 (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ |
|
1034 @{term "STR []"} $ (* FIXME *) |
|
1035 absdummy @{typ unit} (incr_boundvars 1 lhs)) |
|
1036 |> SOME |
|
1037 end; |
|
1038 in |
|
1039 if is_none maybe_rhs' then [] else |
|
1040 let |
|
1041 val rhs = the maybe_rhs'; |
|
1042 val bound_Ts = List.rev (map fastype_of fun_args); |
|
1043 val (raw_rhs, ctr_thms) = |
|
1044 if is_some maybe_rhs then |
|
1045 let |
|
1046 val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs; |
|
1047 val cond_ctrs = |
|
1048 fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs []; |
|
1049 val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs; |
|
1050 in (raw_rhs, ctr_thms) end |
|
1051 else |
|
1052 (rhs, map snd ctr_alist); |
|
1053 |
|
1054 val ms = map (Logic.count_prems o prop_of) ctr_thms; |
1056 val ms = map (Logic.count_prems o prop_of) ctr_thms; |
1055 val (raw_t, t) = (raw_rhs, rhs) |
1057 val (raw_t, t) = (raw_rhs, rhs) |
1056 |> pairself |
1058 |> pairself |
1057 (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T), |
1059 (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T), |
1058 map Bound (length fun_args - 1 downto 0))) |
1060 map Bound (length fun_args - 1 downto 0))) |