2336 |
2336 |
2337 (* TFF allows implicit declarations of types, function symbols, and predicate |
2337 (* TFF allows implicit declarations of types, function symbols, and predicate |
2338 symbols (with "$i" as the type of individuals), but some provers (e.g., |
2338 symbols (with "$i" as the type of individuals), but some provers (e.g., |
2339 SNARK) require explicit declarations. The situation is similar for THF. *) |
2339 SNARK) require explicit declarations. The situation is similar for THF. *) |
2340 |
2340 |
2341 fun default_type pred_sym s = |
2341 fun default_type type_enc pred_sym s = |
2342 let |
2342 let |
2343 val ind = |
2343 val ind = |
2344 if String.isPrefix type_const_prefix s then atype_of_types |
2344 case type_enc of |
2345 else individual_atype |
2345 Simple_Types _ => |
|
2346 if String.isPrefix type_const_prefix s then atype_of_types |
|
2347 else individual_atype |
|
2348 | _ => individual_atype |
2346 fun typ 0 = if pred_sym then bool_atype else ind |
2349 fun typ 0 = if pred_sym then bool_atype else ind |
2347 | typ ary = AFun (ind, typ (ary - 1)) |
2350 | typ ary = AFun (ind, typ (ary - 1)) |
2348 in typ end |
2351 in typ end |
2349 |
2352 |
2350 fun nary_type_constr_type n = |
2353 fun nary_type_constr_type n = |
2351 funpow n (curry AFun atype_of_types) atype_of_types |
2354 funpow n (curry AFun atype_of_types) atype_of_types |
2352 |
2355 |
2353 fun undeclared_syms_in_problem problem = |
2356 fun undeclared_syms_in_problem type_enc problem = |
2354 let |
2357 let |
2355 val declared = declared_syms_in_problem problem |
2358 val declared = declared_syms_in_problem problem |
2356 fun do_sym name ty = |
2359 fun do_sym name ty = |
2357 if member (op =) declared name then I else AList.default (op =) (name, ty) |
2360 if member (op =) declared name then I else AList.default (op =) (name, ty) |
2358 fun do_type (AType (name as (s, _), tys)) = |
2361 fun do_type (AType (name as (s, _), tys)) = |
2361 #> fold do_type tys |
2364 #> fold do_type tys |
2362 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 |
2365 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 |
2363 | do_type (ATyAbs (_, ty)) = do_type ty |
2366 | do_type (ATyAbs (_, ty)) = do_type ty |
2364 fun do_term pred_sym (ATerm (name as (s, _), tms)) = |
2367 fun do_term pred_sym (ATerm (name as (s, _), tms)) = |
2365 is_tptp_user_symbol s |
2368 is_tptp_user_symbol s |
2366 ? do_sym name (fn _ => default_type pred_sym s (length tms)) |
2369 ? do_sym name (fn _ => default_type type_enc pred_sym s (length tms)) |
2367 #> fold (do_term false) tms |
2370 #> fold (do_term false) tms |
2368 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm |
2371 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm |
2369 fun do_formula (AQuant (_, xs, phi)) = |
2372 fun do_formula (AQuant (_, xs, phi)) = |
2370 fold do_type (map_filter snd xs) #> do_formula phi |
2373 fold do_type (map_filter snd xs) #> do_formula phi |
2371 | do_formula (AConn (_, phis)) = fold do_formula phis |
2374 | do_formula (AConn (_, phis)) = fold do_formula phis |
2375 in |
2378 in |
2376 fold (fold do_problem_line o snd) problem [] |
2379 fold (fold do_problem_line o snd) problem [] |
2377 |> filter_out (is_built_in_tptp_symbol o fst o fst) |
2380 |> filter_out (is_built_in_tptp_symbol o fst o fst) |
2378 end |
2381 end |
2379 |
2382 |
2380 fun declare_undeclared_syms_in_atp_problem problem = |
2383 fun declare_undeclared_syms_in_atp_problem type_enc problem = |
2381 let |
2384 let |
2382 val decls = |
2385 val decls = |
2383 problem |
2386 problem |
2384 |> undeclared_syms_in_problem |
2387 |> undeclared_syms_in_problem type_enc |
2385 |> sort_wrt (fst o fst) |
2388 |> sort_wrt (fst o fst) |
2386 |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ())) |
2389 |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ())) |
2387 in (implicit_declsN, decls) :: problem end |
2390 in (implicit_declsN, decls) :: problem end |
2388 |
2391 |
2389 val explicit_apply_threshold = 50 |
2392 val explicit_apply_threshold = 50 |
2462 CNF => ensure_cnf_problem |
2465 CNF => ensure_cnf_problem |
2463 | CNF_UEQ => filter_cnf_ueq_problem |
2466 | CNF_UEQ => filter_cnf_ueq_problem |
2464 | FOF => I |
2467 | FOF => I |
2465 | TFF (_, TPTP_Implicit) => I |
2468 | TFF (_, TPTP_Implicit) => I |
2466 | THF (_, TPTP_Implicit, _) => I |
2469 | THF (_, TPTP_Implicit, _) => I |
2467 | _ => declare_undeclared_syms_in_atp_problem) |
2470 | _ => declare_undeclared_syms_in_atp_problem type_enc) |
2468 val (problem, pool) = problem |> nice_atp_problem readable_names |
2471 val (problem, pool) = problem |> nice_atp_problem readable_names |
2469 fun add_sym_ary (s, {min_ary, ...} : sym_info) = |
2472 fun add_sym_ary (s, {min_ary, ...} : sym_info) = |
2470 min_ary > 0 ? Symtab.insert (op =) (s, min_ary) |
2473 min_ary > 0 ? Symtab.insert (op =) (s, min_ary) |
2471 in |
2474 in |
2472 (problem, |
2475 (problem, |