2822 else () |
2822 else () |
2823 val (preds, all_vs, param_vs, all_modes, clauses) = |
2823 val (preds, all_vs, param_vs, all_modes, clauses) = |
2824 prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames) |
2824 prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames) |
2825 val _ = print_step options "Infering modes..." |
2825 val _ = print_step options "Infering modes..." |
2826 val ((moded_clauses, errors), thy') = |
2826 val ((moded_clauses, errors), thy') = |
2827 Output.cond_timeit true "Infering modes" |
2827 Output.cond_timeit (!Quickcheck.timing) "Infering modes" |
2828 (fn _ => infer_modes mode_analysis_options |
2828 (fn _ => infer_modes mode_analysis_options |
2829 options compilation preds all_modes param_vs clauses thy) |
2829 options compilation preds all_modes param_vs clauses thy) |
2830 val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses |
2830 val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses |
2831 val _ = check_expected_modes preds options modes |
2831 val _ = check_expected_modes preds options modes |
2832 (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*) |
2832 (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*) |