166 |
166 |
167 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) |
167 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) |
168 | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) |
168 | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) |
169 | formula_map f (AAtom tm) = AAtom (f tm) |
169 | formula_map f (AAtom tm) = AAtom (f tm) |
170 |
170 |
|
171 fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi |
|
172 | aconn_fold pos f (AImplies, [phi1, phi2]) = |
|
173 f (Option.map not pos) phi1 #> f pos phi2 |
|
174 | aconn_fold pos f (AAnd, phis) = fold (f pos) phis |
|
175 | aconn_fold pos f (AOr, phis) = fold (f pos) phis |
|
176 | aconn_fold _ f (_, phis) = fold (f NONE) phis |
|
177 |
|
178 fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi]) |
|
179 | aconn_map pos f (AImplies, [phi1, phi2]) = |
|
180 AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2]) |
|
181 | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis) |
|
182 | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis) |
|
183 | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis) |
|
184 |
171 fun formula_fold pos f = |
185 fun formula_fold pos f = |
172 let |
186 let |
173 fun aux pos (AQuant (_, _, phi)) = aux pos phi |
187 fun aux pos (AQuant (_, _, phi)) = aux pos phi |
174 | aux pos (AConn (ANot, [phi])) = aux (Option.map not pos) phi |
188 | aux pos (AConn conn) = aconn_fold pos aux conn |
175 | aux pos (AConn (AImplies, [phi1, phi2])) = |
|
176 aux (Option.map not pos) phi1 #> aux pos phi2 |
|
177 | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis |
|
178 | aux pos (AConn (AOr, phis)) = fold (aux pos) phis |
|
179 | aux _ (AConn (_, phis)) = fold (aux NONE) phis |
|
180 | aux pos (AAtom tm) = f pos tm |
189 | aux pos (AAtom tm) = f pos tm |
181 in aux pos end |
190 in aux pos end |
182 |
191 |
183 type translated_formula = |
192 type translated_formula = |
184 {name: string, |
193 {name: string, |
487 | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T |
496 | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T |
488 | should_encode_type _ _ _ _ = false |
497 | should_encode_type _ _ _ _ = false |
489 |
498 |
490 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness)) |
499 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness)) |
491 should_predicate_on_var T = |
500 should_predicate_on_var T = |
492 (heaviness = Heavy orelse should_predicate_on_var ()) andalso |
501 (heaviness = Heavy orelse should_predicate_on_var ()) andalso |
493 should_encode_type ctxt nonmono_Ts level T |
502 should_encode_type ctxt nonmono_Ts level T |
494 | should_predicate_on_type _ _ _ _ _ = false |
503 | should_predicate_on_type _ _ _ _ _ = false |
495 |
504 |
496 fun is_var_or_bound_var (CombConst ((s, _), _, _)) = |
505 fun is_var_or_bound_var (CombConst ((s, _), _, _)) = |
497 String.isPrefix bound_var_prefix s |
506 String.isPrefix bound_var_prefix s |
498 | is_var_or_bound_var (CombVar _) = true |
507 | is_var_or_bound_var (CombVar _) = true |
778 | fo_literal_from_type_literal (TyLitFree (class, name)) = |
787 | fo_literal_from_type_literal (TyLitFree (class, name)) = |
779 (true, ATerm (class, [ATerm (name, [])])) |
788 (true, ATerm (class, [ATerm (name, [])])) |
780 |
789 |
781 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot |
790 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot |
782 |
791 |
783 fun type_pred_combatom ctxt nonmono_Ts type_sys T tm = |
792 fun type_pred_combterm ctxt nonmono_Ts type_sys T tm = |
784 CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]) |
793 CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]) |
785 |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys, |
794 |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys, |
786 tm) |
795 tm) |
787 |> AAtom |
796 |
788 |
797 fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum |
789 fun var_occurs_naked_in_term name (ATerm ((s, _), tms)) accum = |
798 | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = |
790 accum orelse |
799 accum orelse (s = "equal" andalso member (op =) tms (ATerm (name, []))) |
791 (s = "equal" andalso member (op =) tms (ATerm (name, []))) |
800 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false |
792 fun var_occurs_naked_in_formula phi name = |
801 | is_var_nonmonotonic_in_formula pos phi _ name = |
793 formula_fold NONE (K (var_occurs_naked_in_term name)) phi false |
802 formula_fold pos (var_occurs_positively_naked_in_term name) phi false |
794 |
803 |
795 fun tag_with_type ctxt nonmono_Ts type_sys T tm = |
804 fun tag_with_type ctxt nonmono_Ts type_sys T tm = |
796 CombConst (`make_fixed_const type_tag_name, T --> T, [T]) |
805 CombConst (`make_fixed_const type_tag_name, T --> T, [T]) |
797 |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys |
806 |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys |
798 |> term_from_combterm ctxt nonmono_Ts type_sys Top_Level |
807 |> term_from_combterm ctxt nonmono_Ts type_sys Top_Level |
817 else |
826 else |
818 I) |
827 I) |
819 end |
828 end |
820 and formula_from_combformula ctxt nonmono_Ts type_sys should_predicate_on_var = |
829 and formula_from_combformula ctxt nonmono_Ts type_sys should_predicate_on_var = |
821 let |
830 let |
|
831 val do_term = term_from_combterm ctxt nonmono_Ts type_sys Top_Level |
822 val do_bound_type = |
832 val do_bound_type = |
823 case type_sys of |
833 case type_sys of |
824 Simple_Types level => |
834 Simple_Types level => |
825 SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level |
835 SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level |
826 | _ => K NONE |
836 | _ => K NONE |
827 fun do_out_of_bound_type phi (name, T) = |
837 fun do_out_of_bound_type pos phi universal (name, T) = |
828 if should_predicate_on_type ctxt nonmono_Ts type_sys |
838 if should_predicate_on_type ctxt nonmono_Ts type_sys |
829 (fn () => should_predicate_on_var phi name) T then |
839 (fn () => should_predicate_on_var pos phi universal name) T then |
830 CombVar (name, T) |
840 CombVar (name, T) |
831 |> type_pred_combatom ctxt nonmono_Ts type_sys T |
841 |> type_pred_combterm ctxt nonmono_Ts type_sys T |
832 |> do_formula |> SOME |
842 |> do_term |> AAtom |> SOME |
833 else |
843 else |
834 NONE |
844 NONE |
835 and do_formula (AQuant (q, xs, phi)) = |
845 fun do_formula pos (AQuant (q, xs, phi)) = |
836 let val phi = phi |> do_formula in |
846 let |
|
847 val phi = phi |> do_formula pos |
|
848 val universal = Option.map (q = AExists ? not) pos |
|
849 in |
837 AQuant (q, xs |> map (apsnd (fn NONE => NONE |
850 AQuant (q, xs |> map (apsnd (fn NONE => NONE |
838 | SOME T => do_bound_type T)), |
851 | SOME T => do_bound_type T)), |
839 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) |
852 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) |
840 (map_filter |
853 (map_filter |
841 (fn (_, NONE) => NONE |
854 (fn (_, NONE) => NONE |
842 | (s, SOME T) => |
855 | (s, SOME T) => |
843 do_out_of_bound_type phi (s, T)) xs) |
856 do_out_of_bound_type pos phi universal (s, T)) |
|
857 xs) |
844 phi) |
858 phi) |
845 end |
859 end |
846 | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) |
860 | do_formula pos (AConn conn) = aconn_map pos do_formula conn |
847 | do_formula (AAtom tm) = |
861 | do_formula _ (AAtom tm) = AAtom (do_term tm) |
848 AAtom (term_from_combterm ctxt nonmono_Ts type_sys Top_Level tm) |
862 in do_formula o SOME end |
849 in do_formula end |
|
850 |
863 |
851 fun bound_atomic_types type_sys Ts = |
864 fun bound_atomic_types type_sys Ts = |
852 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) |
865 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) |
853 (atp_type_literals_for_types type_sys Axiom Ts)) |
866 (atp_type_literals_for_types type_sys Axiom Ts)) |
854 |
867 |
855 fun formula_for_fact ctxt nonmono_Ts type_sys |
868 fun formula_for_fact ctxt nonmono_Ts type_sys |
856 ({combformula, atomic_types, ...} : translated_formula) = |
869 ({combformula, atomic_types, ...} : translated_formula) = |
857 combformula |
870 combformula |
858 |> close_combformula_universally |
871 |> close_combformula_universally |
859 |> formula_from_combformula ctxt nonmono_Ts type_sys |
872 |> formula_from_combformula ctxt nonmono_Ts type_sys |
860 var_occurs_naked_in_formula |
873 is_var_nonmonotonic_in_formula true |
861 |> bound_atomic_types type_sys atomic_types |
874 |> bound_atomic_types type_sys atomic_types |
862 |> close_formula_universally |
875 |> close_formula_universally |
863 |
876 |
864 fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])])) |
877 fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])])) |
865 |
878 |
906 |
919 |
907 fun formula_line_for_conjecture ctxt nonmono_Ts type_sys |
920 fun formula_line_for_conjecture ctxt nonmono_Ts type_sys |
908 ({name, kind, combformula, ...} : translated_formula) = |
921 ({name, kind, combformula, ...} : translated_formula) = |
909 Formula (conjecture_prefix ^ name, kind, |
922 Formula (conjecture_prefix ^ name, kind, |
910 formula_from_combformula ctxt nonmono_Ts type_sys |
923 formula_from_combformula ctxt nonmono_Ts type_sys |
911 var_occurs_naked_in_formula |
924 is_var_nonmonotonic_in_formula false |
912 (close_combformula_universally combformula) |
925 (close_combformula_universally combformula) |
913 |> close_formula_universally, NONE, NONE) |
926 |> close_formula_universally, NONE, NONE) |
914 |
927 |
915 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = |
928 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = |
916 atomic_types |> atp_type_literals_for_types type_sys Conjecture |
929 atomic_types |> atp_type_literals_for_types type_sys Conjecture |
1027 in |
1040 in |
1028 Formula (sym_decl_prefix ^ s ^ |
1041 Formula (sym_decl_prefix ^ s ^ |
1029 (if n > 1 then "_" ^ string_of_int j else ""), kind, |
1042 (if n > 1 then "_" ^ string_of_int j else ""), kind, |
1030 CombConst ((s, s'), T, T_args) |
1043 CombConst ((s, s'), T, T_args) |
1031 |> fold (curry (CombApp o swap)) bounds |
1044 |> fold (curry (CombApp o swap)) bounds |
1032 |> type_pred_combatom ctxt nonmono_Ts type_sys res_T |
1045 |> type_pred_combterm ctxt nonmono_Ts type_sys res_T |
|
1046 |> AAtom |
1033 |> mk_aquant AForall (bound_names ~~ bound_Ts) |
1047 |> mk_aquant AForall (bound_names ~~ bound_Ts) |
1034 |> formula_from_combformula ctxt nonmono_Ts type_sys (K (K true)) |
1048 |> formula_from_combformula ctxt nonmono_Ts type_sys |
|
1049 (K (K (K (K true)))) true |
1035 |> n > 1 ? bound_atomic_types type_sys (atyps_of T) |
1050 |> n > 1 ? bound_atomic_types type_sys (atyps_of T) |
1036 |> close_formula_universally |
1051 |> close_formula_universally |
1037 |> maybe_negate, |
1052 |> maybe_negate, |
1038 NONE, NONE) |
1053 NONE, NONE) |
1039 end |
1054 end |