22 val fact_prefix : string |
22 val fact_prefix : string |
23 val conjecture_prefix : string |
23 val conjecture_prefix : string |
24 val boolify_base : string |
24 val boolify_base : string |
25 val explicit_app_base : string |
25 val explicit_app_base : string |
26 val type_pred_base : string |
26 val type_pred_base : string |
27 val type_prefix : string |
27 val tff_type_prefix : string |
28 val is_type_system_sound : type_system -> bool |
28 val is_type_system_sound : type_system -> bool |
29 val type_system_types_dangerous_types : type_system -> bool |
29 val type_system_types_dangerous_types : type_system -> bool |
30 val num_atp_type_args : theory -> type_system -> string -> int |
30 val num_atp_type_args : theory -> type_system -> string -> int |
31 val unmangled_const : string -> string * string fo_term list |
31 val unmangled_const : string -> string * string fo_term list |
32 val translate_atp_fact : |
32 val translate_atp_fact : |
71 val sledgehammer_weak_prefix = "Sledgehammer:" |
71 val sledgehammer_weak_prefix = "Sledgehammer:" |
72 |
72 |
73 type translated_formula = |
73 type translated_formula = |
74 {name: string, |
74 {name: string, |
75 kind: formula_kind, |
75 kind: formula_kind, |
76 combformula: (name, combtyp, combterm) formula, |
76 combformula: (name, typ, combterm) formula, |
77 ctypes_sorts: typ list} |
77 atomic_types: typ list} |
78 |
78 |
79 fun update_combformula f |
79 fun update_combformula f |
80 ({name, kind, combformula, ctypes_sorts} : translated_formula) = |
80 ({name, kind, combformula, atomic_types} : translated_formula) = |
81 {name = name, kind = kind, combformula = f combformula, |
81 {name = name, kind = kind, combformula = f combformula, |
82 ctypes_sorts = ctypes_sorts} : translated_formula |
82 atomic_types = atomic_types} : translated_formula |
83 |
83 |
84 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula |
84 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula |
85 |
85 |
86 datatype type_system = |
86 datatype type_system = |
87 Many_Typed | |
87 Many_Typed | |
163 fun term_vars (ATerm (name as (s, _), tms)) = |
163 fun term_vars (ATerm (name as (s, _), tms)) = |
164 is_atp_variable s ? insert (op =) (name, NONE) |
164 is_atp_variable s ? insert (op =) (name, NONE) |
165 #> fold term_vars tms |
165 #> fold term_vars tms |
166 val close_formula_universally = close_universally term_vars |
166 val close_formula_universally = close_universally term_vars |
167 |
167 |
168 (* We are crossing our fingers that it doesn't clash with anything else. *) |
168 fun fo_term_from_typ (Type (s, Ts)) = |
|
169 ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts) |
|
170 | fo_term_from_typ (TFree (s, _)) = |
|
171 ATerm (`make_fixed_type_var s, []) |
|
172 | fo_term_from_typ (TVar ((x as (s, _)), _)) = |
|
173 ATerm ((make_schematic_type_var x, s), []) |
|
174 |
|
175 (* This shouldn't clash with anything else. *) |
169 val mangled_type_sep = "\000" |
176 val mangled_type_sep = "\000" |
170 |
177 |
171 fun mangled_combtyp_component f (CombTFree name) = f name |
178 fun generic_mangled_type_name f (ATerm (name, [])) = f name |
172 | mangled_combtyp_component f (CombTVar name) = |
179 | generic_mangled_type_name f (ATerm (name, tys)) = |
173 f name (* FIXME: shouldn't happen *) |
180 f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")" |
174 (* raise Fail "impossible schematic type variable" *) |
181 val mangled_type_name = |
175 | mangled_combtyp_component f (CombType (name, tys)) = |
182 fo_term_from_typ |
176 f name ^ "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")" |
183 #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty), |
177 |
184 generic_mangled_type_name snd ty)) |
178 fun mangled_combtyp ty = |
185 |
179 (make_type (mangled_combtyp_component fst ty), |
186 fun generic_mangled_type_suffix f g tys = |
180 mangled_combtyp_component snd ty) |
|
181 |
|
182 fun mangled_type_suffix f g tys = |
|
183 fold_rev (curry (op ^) o g o prefix mangled_type_sep |
187 fold_rev (curry (op ^) o g o prefix mangled_type_sep |
184 o mangled_combtyp_component f) tys "" |
188 o generic_mangled_type_name f) tys "" |
185 |
189 fun mangled_const_name T_args (s, s') = |
186 fun mangled_const_name_fst ty_args s = |
190 let val ty_args = map fo_term_from_typ T_args in |
187 s ^ mangled_type_suffix fst ascii_of ty_args |
191 (s ^ generic_mangled_type_suffix fst ascii_of ty_args, |
188 fun mangled_const_name_snd ty_args s' = s' ^ mangled_type_suffix snd I ty_args |
192 s' ^ generic_mangled_type_suffix snd I ty_args) |
189 fun mangled_const_name ty_args (s, s') = |
193 end |
190 (mangled_const_name_fst ty_args s, mangled_const_name_snd ty_args s') |
|
191 |
194 |
192 val parse_mangled_ident = |
195 val parse_mangled_ident = |
193 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode |
196 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode |
194 |
197 |
195 fun parse_mangled_type x = |
198 fun parse_mangled_type x = |
210 fun unmangled_const s = |
213 fun unmangled_const s = |
211 let val ss = space_explode mangled_type_sep s in |
214 let val ss = space_explode mangled_type_sep s in |
212 (hd ss, map unmangled_type (tl ss)) |
215 (hd ss, map unmangled_type (tl ss)) |
213 end |
216 end |
214 |
217 |
215 fun combformula_for_prop thy eq_as_iff = |
218 fun combformula_from_prop thy eq_as_iff = |
216 let |
219 let |
217 fun do_term bs t ts = |
220 fun do_term bs t ts = |
218 combterm_from_term thy bs (Envir.eta_contract t) |
221 combterm_from_term thy bs (Envir.eta_contract t) |
219 |>> AAtom ||> union (op =) ts |
222 |>> AAtom ||> union (op =) ts |
220 fun do_quant bs q s T t' = |
223 fun do_quant bs q s T t' = |
221 let val s = Name.variant (map fst bs) s in |
224 let val s = Name.variant (map fst bs) s in |
222 do_formula ((s, T) :: bs) t' |
225 do_formula ((s, T) :: bs) t' |
223 #>> mk_aquant q [(`make_bound_var s, SOME (combtyp_from_typ T))] |
226 #>> mk_aquant q [(`make_bound_var s, SOME T)] |
224 end |
227 end |
225 and do_conn bs c t1 t2 = |
228 and do_conn bs c t1 t2 = |
226 do_formula bs t1 ##>> do_formula bs t2 |
229 do_formula bs t1 ##>> do_formula bs t2 |
227 #>> uncurry (mk_aconn c) |
230 #>> uncurry (mk_aconn c) |
228 and do_formula bs t = |
231 and do_formula bs t = |
332 |> extensionalize_term |
335 |> extensionalize_term |
333 |> presimp ? presimplify_term thy |
336 |> presimp ? presimplify_term thy |
334 |> perhaps (try (HOLogic.dest_Trueprop)) |
337 |> perhaps (try (HOLogic.dest_Trueprop)) |
335 |> introduce_combinators_in_term ctxt kind |
338 |> introduce_combinators_in_term ctxt kind |
336 |> kind <> Axiom ? freeze_term |
339 |> kind <> Axiom ? freeze_term |
337 val (combformula, ctypes_sorts) = |
340 val (combformula, atomic_types) = |
338 combformula_for_prop thy eq_as_iff t [] |
341 combformula_from_prop thy eq_as_iff t [] |
339 in |
342 in |
340 {name = name, combformula = combformula, kind = kind, |
343 {name = name, combformula = combformula, kind = kind, |
341 ctypes_sorts = ctypes_sorts} |
344 atomic_types = atomic_types} |
342 end |
345 end |
343 |
346 |
344 fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), t) = |
347 fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), t) = |
345 case (keep_trivial, make_formula ctxt eq_as_iff presimp name Axiom t) of |
348 case (keep_trivial, make_formula ctxt eq_as_iff presimp name Axiom t) of |
346 (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) => |
349 (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) => |
372 Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom, |
375 Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom, |
373 AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) |
376 AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) |
374 |> close_formula_universally, NONE, NONE) |
377 |> close_formula_universally, NONE, NONE) |
375 end |
378 end |
376 |
379 |
377 (* FIXME #### : abolish combtyp altogether *) |
380 fun helper_facts_for_typed_const ctxt type_sys s (_, _, T) = |
378 fun typ_from_combtyp (CombType ((s, _), tys)) = |
|
379 Type (s |> strip_prefix_and_unascii type_const_prefix |> the |
|
380 |> invert_const, |
|
381 map typ_from_combtyp tys) |
|
382 | typ_from_combtyp (CombTFree (s, _)) = |
|
383 TFree (s |> strip_prefix_and_unascii tfree_prefix |> the, HOLogic.typeS) |
|
384 | typ_from_combtyp (CombTVar (s, _)) = |
|
385 TVar ((s |> strip_prefix_and_unascii tvar_prefix |> the, 0), HOLogic.typeS) |
|
386 |
|
387 fun helper_facts_for_typed_const ctxt type_sys s (_, _, ty) = |
|
388 case strip_prefix_and_unascii const_prefix s of |
381 case strip_prefix_and_unascii const_prefix s of |
389 SOME s'' => |
382 SOME s'' => |
390 let |
383 let |
391 val thy = Proof_Context.theory_of ctxt |
384 val thy = Proof_Context.theory_of ctxt |
392 val unmangled_s = s'' |> unmangled_const_name |
385 val unmangled_s = s'' |> unmangled_const_name |
393 (* ### FIXME avoid duplicate names *) |
386 (* ### FIXME avoid duplicate names *) |
394 fun dub_and_inst c needs_full_types (th, j) = |
387 fun dub_and_inst c needs_full_types (th, j) = |
395 ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""), |
388 ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""), |
396 false), |
389 false), |
397 th |> prop_of |
390 th |> prop_of |
398 |> specialize_type thy (invert_const unmangled_s, |
391 |> specialize_type thy (invert_const unmangled_s, T)) |
399 typ_from_combtyp ty)) |
|
400 fun make_facts eq_as_iff = |
392 fun make_facts eq_as_iff = |
401 map_filter (make_fact ctxt false eq_as_iff false) |
393 map_filter (make_fact ctxt false eq_as_iff false) |
402 in |
394 in |
403 metis_helpers |
395 metis_helpers |
404 |> maps (fn (metis_s, (needs_full_types, ths)) => |
396 |> maps (fn (metis_s, (needs_full_types, ths)) => |
486 | aux _ tm = tm |
478 | aux _ tm = tm |
487 in aux true end |
479 in aux true end |
488 |
480 |
489 fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t]) |
481 fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t]) |
490 |
482 |
491 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) |
483 fun fo_literal_from_type_literal (TyLitVar (class, name)) = |
492 | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) |
|
493 | fo_term_for_combtyp (CombType (name, tys)) = |
|
494 ATerm (name, map fo_term_for_combtyp tys) |
|
495 |
|
496 fun fo_literal_for_type_literal (TyLitVar (class, name)) = |
|
497 (true, ATerm (class, [ATerm (name, [])])) |
484 (true, ATerm (class, [ATerm (name, [])])) |
498 | fo_literal_for_type_literal (TyLitFree (class, name)) = |
485 | fo_literal_from_type_literal (TyLitFree (class, name)) = |
499 (true, ATerm (class, [ATerm (name, [])])) |
486 (true, ATerm (class, [ATerm (name, [])])) |
500 |
487 |
501 fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot |
488 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot |
502 |
489 |
503 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are |
490 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are |
504 considered dangerous because their "exhaust" properties can easily lead to |
491 considered dangerous because their "exhaust" properties can easily lead to |
505 unsound ATP proofs. The checks below are an (unsound) approximation of |
492 unsound ATP proofs. The checks below are an (unsound) approximation of |
506 finiteness. *) |
493 finiteness. *) |
522 case Typedef.get_info ctxt s of |
509 case Typedef.get_info ctxt s of |
523 ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type |
510 ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type |
524 | [] => true |
511 | [] => true |
525 end |
512 end |
526 |
513 |
527 fun is_combtyp_dangerous ctxt (CombType ((s, _), tys)) = |
514 fun should_tag_with_type ctxt (Tags full_types) T = |
528 (case strip_prefix_and_unascii type_const_prefix s of |
515 full_types orelse is_type_dangerous ctxt T |
529 SOME s' => forall (is_combtyp_dangerous ctxt) tys andalso |
|
530 is_type_constr_dangerous ctxt (invert_const s') |
|
531 | NONE => false) |
|
532 | is_combtyp_dangerous _ _ = false |
|
533 |
|
534 fun should_tag_with_type ctxt (Tags full_types) ty = |
|
535 full_types orelse is_combtyp_dangerous ctxt ty |
|
536 | should_tag_with_type _ _ _ = false |
516 | should_tag_with_type _ _ _ = false |
537 |
517 |
538 fun pred_combtyp ty = |
518 fun type_pred_combatom type_sys T tm = |
539 case combtyp_from_typ @{typ "unit => bool"} of |
519 CombApp (CombConst (`make_fixed_const type_pred_base, |
540 CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty]) |
520 T --> HOLogic.boolT, [T]), tm) |
541 | _ => raise Fail "expected two-argument type constructor" |
|
542 |
|
543 fun type_pred_combatom type_sys ty tm = |
|
544 CombApp (CombConst (`make_fixed_const type_pred_base, pred_combtyp ty, [ty]), |
|
545 tm) |
|
546 |> repair_combterm_consts type_sys |
521 |> repair_combterm_consts type_sys |
547 |> AAtom |
522 |> AAtom |
548 |
523 |
549 fun formula_for_combformula ctxt type_sys = |
524 fun formula_from_combformula ctxt type_sys = |
550 let |
525 let |
551 fun do_term top_level u = |
526 fun do_term top_level u = |
552 let |
527 let |
553 val (head, args) = strip_combterm_comb u |
528 val (head, args) = strip_combterm_comb u |
554 val (x, ty_args) = |
529 val (x, ty_args) = |
555 case head of |
530 case head of |
556 CombConst (name, _, ty_args) => (name, ty_args) |
531 CombConst (name, _, ty_args) => (name, ty_args) |
557 | CombVar (name, _) => (name, []) |
532 | CombVar (name, _) => (name, []) |
558 | CombApp _ => raise Fail "impossible \"CombApp\"" |
533 | CombApp _ => raise Fail "impossible \"CombApp\"" |
559 val t = ATerm (x, map fo_term_for_combtyp ty_args @ |
534 val t = ATerm (x, map fo_term_from_typ ty_args @ |
560 map (do_term false) args) |
535 map (do_term false) args) |
561 val ty = combtyp_of u |
536 val ty = combtyp_of u |
562 in |
537 in |
563 t |> (if not top_level andalso |
538 t |> (if not top_level andalso |
564 should_tag_with_type ctxt type_sys ty then |
539 should_tag_with_type ctxt type_sys ty then |
565 tag_with_type (fo_term_for_combtyp ty) |
540 tag_with_type (fo_term_from_typ ty) |
566 else |
541 else |
567 I) |
542 I) |
568 end |
543 end |
569 val do_bound_type = |
544 val do_bound_type = |
570 if type_sys = Many_Typed then SOME o mangled_combtyp else K NONE |
545 if type_sys = Many_Typed then SOME o mangled_type_name else K NONE |
571 val do_out_of_bound_type = |
546 val do_out_of_bound_type = |
572 if member (op =) [Mangled true, Args true] type_sys then |
547 if member (op =) [Mangled true, Args true] type_sys then |
573 (fn (s, ty) => |
548 (fn (s, ty) => |
574 type_pred_combatom type_sys ty (CombVar (s, ty)) |
549 type_pred_combatom type_sys ty (CombVar (s, ty)) |
575 |> formula_for_combformula ctxt type_sys |> SOME) |
550 |> formula_from_combformula ctxt type_sys |> SOME) |
576 else |
551 else |
577 K NONE |
552 K NONE |
578 fun do_formula (AQuant (q, xs, phi)) = |
553 fun do_formula (AQuant (q, xs, phi)) = |
579 AQuant (q, xs |> map (apsnd (fn NONE => NONE |
554 AQuant (q, xs |> map (apsnd (fn NONE => NONE |
580 | SOME ty => do_bound_type ty)), |
555 | SOME ty => do_bound_type ty)), |
586 | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) |
561 | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) |
587 | do_formula (AAtom tm) = AAtom (do_term true tm) |
562 | do_formula (AAtom tm) = AAtom (do_term true tm) |
588 in do_formula end |
563 in do_formula end |
589 |
564 |
590 fun formula_for_fact ctxt type_sys |
565 fun formula_for_fact ctxt type_sys |
591 ({combformula, ctypes_sorts, ...} : translated_formula) = |
566 ({combformula, atomic_types, ...} : translated_formula) = |
592 mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) |
567 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) |
593 (atp_type_literals_for_types type_sys Axiom ctypes_sorts)) |
568 (atp_type_literals_for_types type_sys Axiom atomic_types)) |
594 (formula_for_combformula ctxt type_sys |
569 (formula_from_combformula ctxt type_sys |
595 (close_combformula_universally combformula)) |
570 (close_combformula_universally combformula)) |
596 |> close_formula_universally |
571 |> close_formula_universally |
597 |
572 |
598 fun logic_for_type_sys Many_Typed = Tff |
573 fun logic_for_type_sys Many_Typed = Tff |
599 | logic_for_type_sys _ = Fof |
574 | logic_for_type_sys _ = Fof |
600 |
575 |
614 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), |
589 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), |
615 AAtom (ATerm (superclass, [ty_arg]))]) |
590 AAtom (ATerm (superclass, [ty_arg]))]) |
616 |> close_formula_universally, NONE, NONE) |
591 |> close_formula_universally, NONE, NONE) |
617 end |
592 end |
618 |
593 |
619 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = |
594 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = |
620 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) |
595 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) |
621 | fo_literal_for_arity_literal (TVarLit (c, sort)) = |
596 | fo_literal_from_arity_literal (TVarLit (c, sort)) = |
622 (false, ATerm (c, [ATerm (sort, [])])) |
597 (false, ATerm (c, [ATerm (sort, [])])) |
623 |
598 |
624 fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits, |
599 fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits, |
625 ...}) = |
600 ...}) = |
626 Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom, |
601 Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom, |
627 mk_ahorn (map (formula_for_fo_literal o apfst not |
602 mk_ahorn (map (formula_from_fo_literal o apfst not |
628 o fo_literal_for_arity_literal) premLits) |
603 o fo_literal_from_arity_literal) premLits) |
629 (formula_for_fo_literal |
604 (formula_from_fo_literal |
630 (fo_literal_for_arity_literal conclLit)) |
605 (fo_literal_from_arity_literal conclLit)) |
631 |> close_formula_universally, NONE, NONE) |
606 |> close_formula_universally, NONE, NONE) |
632 |
607 |
633 fun formula_line_for_conjecture ctxt type_sys |
608 fun formula_line_for_conjecture ctxt type_sys |
634 ({name, kind, combformula, ...} : translated_formula) = |
609 ({name, kind, combformula, ...} : translated_formula) = |
635 Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind, |
610 Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind, |
636 formula_for_combformula ctxt type_sys |
611 formula_from_combformula ctxt type_sys |
637 (close_combformula_universally combformula) |
612 (close_combformula_universally combformula) |
638 |> close_formula_universally, NONE, NONE) |
613 |> close_formula_universally, NONE, NONE) |
639 |
614 |
640 fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) = |
615 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = |
641 ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture |
616 atomic_types |> atp_type_literals_for_types type_sys Conjecture |
642 |> map fo_literal_for_type_literal |
617 |> map fo_literal_from_type_literal |
643 |
618 |
644 fun formula_line_for_free_type j lit = |
619 fun formula_line_for_free_type j lit = |
645 Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis, |
620 Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis, |
646 formula_for_fo_literal lit, NONE, NONE) |
621 formula_from_fo_literal lit, NONE, NONE) |
647 fun formula_lines_for_free_types type_sys facts = |
622 fun formula_lines_for_free_types type_sys facts = |
648 let |
623 let |
649 val litss = map (free_type_literals type_sys) facts |
624 val litss = map (free_type_literals type_sys) facts |
650 val lits = fold (union (op =)) litss [] |
625 val lits = fold (union (op =)) litss [] |
651 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end |
626 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end |
718 SOME {pred_sym, min_arity, max_arity} => |
693 SOME {pred_sym, min_arity, max_arity} => |
719 pred_sym andalso min_arity = max_arity |
694 pred_sym andalso min_arity = max_arity |
720 | NONE => false |
695 | NONE => false |
721 |
696 |
722 val boolify_combconst = |
697 val boolify_combconst = |
723 CombConst (`make_fixed_const boolify_base, |
698 CombConst (`make_fixed_const boolify_base, @{typ "bool => bool"}, []) |
724 combtyp_from_typ @{typ "bool => bool"}, []) |
|
725 fun boolify tm = CombApp (boolify_combconst, tm) |
699 fun boolify tm = CombApp (boolify_combconst, tm) |
726 |
700 |
727 fun repair_pred_syms_in_combterm sym_tab tm = |
701 fun repair_pred_syms_in_combterm sym_tab tm = |
728 case strip_combterm_comb tm of |
702 case strip_combterm_comb tm of |
729 (CombConst ((s, _), _, _), _) => |
703 (CombConst ((s, _), _, _), _) => |
730 if is_pred_sym sym_tab s then tm else boolify tm |
704 if is_pred_sym sym_tab s then tm else boolify tm |
731 | _ => boolify tm |
705 | _ => boolify tm |
732 |
706 |
733 fun list_app head args = fold (curry (CombApp o swap)) args head |
707 fun list_app head args = fold (curry (CombApp o swap)) args head |
734 |
708 |
735 val fun_name = `make_fixed_type_const @{type_name fun} |
|
736 |
|
737 fun explicit_app arg head = |
709 fun explicit_app arg head = |
738 let |
710 let |
739 val head_ty = combtyp_of head |
711 val head_T = combtyp_of head |
740 val (arg_ty, res_ty) = dest_combfun head_ty |
712 val (arg_T, res_T) = dest_funT head_T |
741 val explicit_app = |
713 val explicit_app = |
742 CombConst (`make_fixed_const explicit_app_base, |
714 CombConst (`make_fixed_const explicit_app_base, head_T --> head_T, |
743 CombType (fun_name, [head_ty, head_ty]), [arg_ty, res_ty]) |
715 [arg_T, res_T]) |
744 in list_app explicit_app [head, arg] end |
716 in list_app explicit_app [head, arg] end |
745 fun list_explicit_app head args = fold explicit_app args head |
717 fun list_explicit_app head args = fold explicit_app args head |
746 |
718 |
747 fun repair_apps_in_combterm sym_tab = |
719 fun repair_apps_in_combterm sym_tab = |
748 let |
720 let |
784 (* FIXME: needed? *) |
756 (* FIXME: needed? *) |
785 fun typed_const_table_for_facts type_sys sym_tab facts = |
757 fun typed_const_table_for_facts type_sys sym_tab facts = |
786 Symtab.empty |> member (op =) [Many_Typed, Mangled true, Args true] type_sys |
758 Symtab.empty |> member (op =) [Many_Typed, Mangled true, Args true] type_sys |
787 ? fold (consider_fact_consts type_sys sym_tab) facts |
759 ? fold (consider_fact_consts type_sys sym_tab) facts |
788 |
760 |
789 fun strip_and_map_combtyp 0 f ty = ([], f ty) |
761 fun strip_and_map_type 0 f T = ([], f T) |
790 | strip_and_map_combtyp n f (ty as CombType ((s, _), tys)) = |
762 | strip_and_map_type n f (Type (@{type_name fun}, [dom_T, ran_T])) = |
791 (case (strip_prefix_and_unascii type_const_prefix s, tys) of |
763 strip_and_map_type (n - 1) f ran_T |>> cons (f dom_T) |
792 (SOME @{type_name fun}, [dom_ty, ran_ty]) => |
764 | strip_and_map_type _ _ _ = raise Fail "unexpected non-function" |
793 strip_and_map_combtyp (n - 1) f ran_ty |>> cons (f dom_ty) |
765 |
794 | _ => ([], f ty)) |
766 fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, T) = |
795 | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function" |
|
796 |
|
797 fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, ty) = |
|
798 let val arity = min_arity_of sym_tab s in |
767 let val arity = min_arity_of sym_tab s in |
799 if type_sys = Many_Typed then |
768 if type_sys = Many_Typed then |
800 let |
769 let |
801 val (arg_tys, res_ty) = strip_and_map_combtyp arity mangled_combtyp ty |
770 val (arg_Ts, res_T) = strip_and_map_type arity mangled_type_name T |
802 val (s, s') = (s, s') |> mangled_const_name ty_args |
771 val (s, s') = (s, s') |> mangled_const_name ty_args |
803 in |
772 in |
804 Decl (sym_decl_prefix ^ ascii_of s, (s, s'), |
773 Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_Ts, |
805 arg_tys, |
|
806 (* ### FIXME: put that in typed_const_tab *) |
774 (* ### FIXME: put that in typed_const_tab *) |
807 if is_pred_sym sym_tab s then `I tff_bool_type else res_ty) |
775 if is_pred_sym sym_tab s then `I tff_bool_type else res_T) |
808 end |
776 end |
809 else |
777 else |
810 let |
778 let |
811 val (arg_tys, res_ty) = strip_and_map_combtyp arity I ty |
779 val (arg_Ts, res_T) = strip_and_map_type arity I T |
812 val bounds = |
780 val bounds = |
813 map (`I o make_bound_var o string_of_int) (1 upto length arg_tys) |
781 map (`I o make_bound_var o string_of_int) (1 upto length arg_Ts) |
814 ~~ map SOME arg_tys |
782 ~~ map SOME arg_Ts |
815 val bound_tms = |
783 val bound_tms = |
816 map (fn (name, ty) => CombConst (name, the ty, [])) bounds |
784 map (fn (name, T) => CombConst (name, the T, [])) bounds |
817 val freshener = |
785 val freshener = |
818 case type_sys of Args _ => string_of_int j ^ "_" | _ => "" |
786 case type_sys of Args _ => string_of_int j ^ "_" | _ => "" |
819 in |
787 in |
820 Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, |
788 Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, |
821 CombConst ((s, s'), ty, ty_args) |
789 CombConst ((s, s'), T, ty_args) |
822 |> fold (curry (CombApp o swap)) bound_tms |
790 |> fold (curry (CombApp o swap)) bound_tms |
823 |> type_pred_combatom type_sys res_ty |
791 |> type_pred_combatom type_sys res_T |
824 |> mk_aquant AForall bounds |
792 |> mk_aquant AForall bounds |
825 |> formula_for_combformula ctxt type_sys, |
793 |> formula_from_combformula ctxt type_sys, |
826 NONE, NONE) |
794 NONE, NONE) |
827 end |
795 end |
828 end |
796 end |
829 fun problem_lines_for_sym_decl ctxt type_sys sym_tab (s, xs) = |
797 fun problem_lines_for_sym_decl ctxt type_sys sym_tab (s, xs) = |
830 map2 (problem_line_for_typed_const ctxt type_sys sym_tab s) |
798 map2 (problem_line_for_typed_const ctxt type_sys sym_tab s) |
838 union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi |
806 union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi |
839 | add_tff_types_in_formula (AConn (_, phis)) = |
807 | add_tff_types_in_formula (AConn (_, phis)) = |
840 fold add_tff_types_in_formula phis |
808 fold add_tff_types_in_formula phis |
841 | add_tff_types_in_formula (AAtom _) = I |
809 | add_tff_types_in_formula (AAtom _) = I |
842 |
810 |
843 fun add_tff_types_in_problem_line (Decl (_, _, arg_tys, res_ty)) = |
811 fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) = |
844 union (op =) (res_ty :: arg_tys) |
812 union (op =) (res_T :: arg_Ts) |
845 | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) = |
813 | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) = |
846 add_tff_types_in_formula phi |
814 add_tff_types_in_formula phi |
847 |
815 |
848 fun tff_types_in_problem problem = |
816 fun tff_types_in_problem problem = |
849 fold (fold add_tff_types_in_problem_line o snd) problem [] |
817 fold (fold add_tff_types_in_problem_line o snd) problem [] |