73 type_enc, slices, timeout, ...} : params) state goal i facts options = |
73 type_enc, slices, timeout, ...} : params) state goal i facts options = |
74 let |
74 let |
75 val run_timeout = slice_timeout slices timeout |
75 val run_timeout = slice_timeout slices timeout |
76 val (higher_order, nat_as_int) = |
76 val (higher_order, nat_as_int) = |
77 (case type_enc of |
77 (case type_enc of |
78 SOME s => (String.isSubstring "native_higher" s, String.isSubstring "arith" s) |
78 SOME s => (SOME (String.isSubstring "native_higher" s), SOME (String.isSubstring "arith" s)) |
79 | NONE => (false, false)) |
79 | NONE => (NONE, NONE)) |
80 fun repair_context ctxt = ctxt |
80 fun repair_context ctxt = ctxt |
81 |> Context.proof_map (SMT_Config.select_solver name) |
81 |> Context.proof_map (SMT_Config.select_solver name) |
82 |> Config.put SMT_Config.higher_order higher_order |
82 |> (case higher_order of |
83 |> Config.put SMT_Config.nat_as_int nat_as_int |
83 SOME higher_order => Config.put SMT_Config.higher_order higher_order |
|
84 | NONE => I) |
|
85 |> (case nat_as_int of |
|
86 SOME nat_as_int => Config.put SMT_Config.nat_as_int nat_as_int |
|
87 | NONE => I) |
84 |> (if overlord then |
88 |> (if overlord then |
85 Config.put SMT_Config.debug_files |
89 Config.put SMT_Config.debug_files |
86 (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name)) |
90 (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name)) |
87 else |
91 else |
88 I) |
92 I) |