1491 | _ => false |
1491 | _ => false |
1492 end |
1492 end |
1493 |
1493 |
1494 fun unfold_mutually_inductive_preds thy table = |
1494 fun unfold_mutually_inductive_preds thy table = |
1495 map_aterms (fn t as Const x => |
1495 map_aterms (fn t as Const x => |
1496 (case def_of_const thy table x of |
1496 (case def_of_const thy table x of |
1497 SOME t' => |
1497 SOME t' => |
1498 let val t' = Envir.eta_contract t' in |
1498 let val t' = Envir.eta_contract t' in |
1499 if is_mutually_inductive_pred_def thy table t' then t' |
1499 if is_mutually_inductive_pred_def thy table t' then t' else t |
1500 else t |
1500 end |
1501 end |
1501 | NONE => t) |
1502 | NONE => t) |
1502 | t => t) |
1503 | t => t) |
|
1504 |
1503 |
1505 fun case_const_names ctxt = |
1504 fun case_const_names ctxt = |
1506 map_filter (fn {casex = Const (s, T), ...} => |
1505 map_filter (fn {casex = Const (s, T), ...} => |
1507 let val Ts = binder_types T in |
1506 (case rev (binder_types T) of |
1508 if is_data_type ctxt (List.last Ts) then SOME (s, length Ts - 1) |
1507 [] => NONE |
1509 else NONE |
1508 | T :: Ts => if is_data_type ctxt T then SOME (s, length Ts) else NONE)) |
1510 end) |
|
1511 (Ctr_Sugar.ctr_sugars_of ctxt) @ |
1509 (Ctr_Sugar.ctr_sugars_of ctxt) @ |
1512 map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) |
1510 map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) |
1513 |
1511 |
1514 fun fixpoint_kind_of_const thy table x = |
1512 fun fixpoint_kind_of_const thy table x = |
1515 if is_built_in_const x then NoFp |
1513 if is_built_in_const x then NoFp |
1516 else fixpoint_kind_of_rhs (the (def_of_const thy table x)) |
1514 else fixpoint_kind_of_rhs (the (def_of_const thy table x)) |
1517 handle Option.Option => NoFp |
1515 handle Option.Option => NoFp |
1518 |
1516 |
1519 fun is_raw_inductive_pred ({thy, def_tables, intro_table, ...} : hol_context) |
1517 fun is_raw_inductive_pred ({thy, def_tables, intro_table, ...} : hol_context) x = |
1520 x = |
|
1521 fixpoint_kind_of_const thy def_tables x <> NoFp andalso |
1518 fixpoint_kind_of_const thy def_tables x <> NoFp andalso |
1522 not (null (def_props_for_const thy intro_table x)) |
1519 not (null (def_props_for_const thy intro_table x)) |
1523 |
1520 |
1524 fun is_inductive_pred hol_ctxt (x as (s, _)) = |
1521 fun is_inductive_pred hol_ctxt (x as (s, _)) = |
1525 String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s orelse |
1522 String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s orelse |
1671 val j = num_record_fields thy rec_T - 1 |
1668 val j = num_record_fields thy rec_T - 1 |
1672 in |
1669 in |
1673 select_nth_constr_arg ctxt constr_x t j res_T |
1670 select_nth_constr_arg ctxt constr_x t j res_T |
1674 |> optimized_record_get hol_ctxt s rec_T' res_T |
1671 |> optimized_record_get hol_ctxt s rec_T' res_T |
1675 end |
1672 end |
1676 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T], |
1673 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T], [])) |
1677 [])) |
|
1678 | j => select_nth_constr_arg ctxt constr_x t j res_T |
1674 | j => select_nth_constr_arg ctxt constr_x t j res_T |
1679 end |
1675 end |
1680 |
1676 |
1681 fun optimized_record_update (hol_ctxt as {thy, ctxt, ...}) s rec_T fun_t |
1677 fun optimized_record_update (hol_ctxt as {thy, ctxt, ...}) s rec_T fun_t |
1682 rec_t = |
1678 rec_t = |