288 prem_role = Conjecture, |
288 prem_role = Conjecture, |
289 best_slices = fn ctxt => |
289 best_slices = fn ctxt => |
290 let |
290 let |
291 val heuristic = Config.get ctxt e_selection_heuristic |
291 val heuristic = Config.get ctxt e_selection_heuristic |
292 val (format, enc) = |
292 val (format, enc) = |
293 if string_ord (getenv "E_VERSION", "2.6") <> LESS then |
293 if string_ord (getenv "E_VERSION", "2.7") <> LESS then |
294 (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher_fool") |
294 (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher_fool") |
|
295 else if string_ord (getenv "E_VERSION", "2.6") <> LESS then |
|
296 (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher") |
295 else |
297 else |
296 (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher") |
298 (THF (Without_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher") |
297 in |
299 in |
298 (* FUDGE *) |
300 (* FUDGE *) |
299 if heuristic = e_smartN then |
301 if heuristic = e_smartN then |
300 [(0.15, (((128, meshN), format, enc, combsN, false), e_fun_weightN)), |
302 [(0.15, (((128, meshN), format, enc, combsN, false), e_fun_weightN)), |
301 (0.15, (((128, mashN), format, enc, combsN, false), e_sym_offset_weightN)), |
303 (0.15, (((128, mashN), format, enc, combsN, false), e_sym_offset_weightN)), |