2431 |> List.partition is_poly_constr |
2431 |> List.partition is_poly_constr |
2432 |> pairself (map fst) |
2432 |> pairself (map fst) |
2433 |
2433 |
2434 (* Forcing explicit applications is expensive for polymorphic encodings, because |
2434 (* Forcing explicit applications is expensive for polymorphic encodings, because |
2435 it takes only one existential variable ranging over "'a => 'b" to ruin |
2435 it takes only one existential variable ranging over "'a => 'b" to ruin |
2436 everything. Hence we do it only if there are few facts (is normally the case |
2436 everything. Hence we do it only if there are few facts (which is normally the |
2437 for "metis" and the minimizer. *) |
2437 case for "metis" and the minimizer). *) |
2438 val explicit_apply_threshold = 50 |
2438 val explicit_apply_threshold = 50 |
2439 |
2439 |
2440 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter |
2440 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter |
2441 lam_trans readable_names preproc hyp_ts concl_t facts = |
2441 lam_trans readable_names preproc hyp_ts concl_t facts = |
2442 let |
2442 let |
2443 val thy = Proof_Context.theory_of ctxt |
2443 val thy = Proof_Context.theory_of ctxt |
2444 val type_enc = type_enc |> adjust_type_enc format |
2444 val type_enc = type_enc |> adjust_type_enc format |
2445 val explicit_apply = |
2445 val explicit_apply = |
2446 if polymorphism_of_type_enc type_enc <> Polymorphic orelse |
2446 if polymorphism_of_type_enc type_enc = Polymorphic andalso |
2447 length facts <= explicit_apply_threshold then |
2447 length facts >= explicit_apply_threshold then |
|
2448 SOME false |
|
2449 else |
2448 NONE |
2450 NONE |
2449 else |
|
2450 SOME false |
|
2451 val lam_trans = |
2451 val lam_trans = |
2452 if lam_trans = keep_lamsN andalso |
2452 if lam_trans = keep_lamsN andalso |
2453 not (is_type_enc_higher_order type_enc) then |
2453 not (is_type_enc_higher_order type_enc) then |
2454 error ("Lambda translation scheme incompatible with first-order \ |
2454 error ("Lambda translation scheme incompatible with first-order \ |
2455 \encoding.") |
2455 \encoding.") |