wneuper/isa: comparison src/HOL/Tools/ATP/atp

equal deleted inserted replaced

-:def89b8c6948
+:eb763b3ff9ed
 No_Types
 datatype type_heaviness = Heavyweight | Lightweight
 datatype type_enc =
 Simple_Types of order * type_level |
-Preds of polymorphism * type_level * type_heaviness |
+Guards of polymorphism * type_level * type_heaviness |
 Tags of polymorphism * type_level * type_heaviness
 val bound_var_prefix : string
 val schematic_var_prefix : string
 val fixed_var_prefix : string
 val skolem_const_prefix : string
 val old_skolem_const_prefix : string
 val new_skolem_const_prefix : string
 val type_decl_prefix : string
 val sym_decl_prefix : string
-val preds_sym_formula_prefix : string
+val guards_sym_formula_prefix : string
 val lightweight_tags_sym_formula_prefix : string
 val fact_prefix : string
 val conjecture_prefix : string
 val helper_prefix : string
 val class_rel_clause_prefix : string
 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
 val type_decl_prefix = "ty_"
 val sym_decl_prefix = "sy_"
-val preds_sym_formula_prefix = "psy_"
+val guards_sym_formula_prefix = "gsy_"
 val lightweight_tags_sym_formula_prefix = "tsy_"
 val fact_prefix = "fact_"
 val conjecture_prefix = "conj_"
 val helper_prefix = "help_"
 val class_rel_clause_prefix = "clar_"
 No_Types
 datatype type_heaviness = Heavyweight | Lightweight
 datatype type_enc =
 Simple_Types of order * type_level |
-Preds of polymorphism * type_level * type_heaviness |
+Guards of polymorphism * type_level * type_heaviness |
 Tags of polymorphism * type_level * type_heaviness
 fun try_unsuffixes ss s =
 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
 ("simple", (NONE, _, Lightweight)) =>
 Simple_Types (First_Order, level)
 | ("simple_higher", (NONE, _, Lightweight)) =>
 if level = Noninf_Nonmono_Types then raise Same.SAME
 else Simple_Types (Higher_Order, level)
-| ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
+| ("guards", (SOME poly, _, _)) => Guards (poly, level, heaviness)
 | ("tags", (SOME Polymorphic, _, _)) =>
 Tags (Polymorphic, level, heaviness)
 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
-Preds (poly, Const_Arg_Types, Lightweight)
+Guards (poly, Const_Arg_Types, Lightweight)
 | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
-Preds (Polymorphic, No_Types, Lightweight)
+Guards (Polymorphic, No_Types, Lightweight)
 | _ => raise Same.SAME)
 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
 fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
 | is_type_enc_higher_order _ = false
 fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
-| polymorphism_of_type_enc (Preds (poly, _, _)) = poly
+| polymorphism_of_type_enc (Guards (poly, _, _)) = poly
 | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
 fun level_of_type_enc (Simple_Types (_, level)) = level
-| level_of_type_enc (Preds (_, level, _)) = level
+| level_of_type_enc (Guards (_, level, _)) = level
 | level_of_type_enc (Tags (_, level, _)) = level
 fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
-| heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
+| heaviness_of_type_enc (Guards (_, _, heaviness)) = heaviness
 | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
 fun is_type_level_virtually_sound level =
 level = All_Types orelse level = Noninf_Nonmono_Types
 val is_type_enc_virtually_sound =
 if member (op =) formats THF then
 (THF, Simple_Types (order, level))
 else if member (op =) formats TFF then
 (TFF, Simple_Types (First_Order, level))
 else
-choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
+choose_format formats (Guards (Mangled_Monomorphic, level, Heavyweight))
 | choose_format formats type_enc =
 (case hd formats of
 CNF_UEQ =>
 (CNF_UEQ, case type_enc of
-Preds stuff =>
+Guards stuff =>
-(if is_type_enc_fairly_sound type_enc then Tags else Preds)
+(if is_type_enc_fairly_sound type_enc then Tags else Guards)
 stuff
 | _ => type_enc)
 | format => (format, type_enc))
 type translated_formula =
 | should_encode_type _ _ All_Types _ = true
 | should_encode_type ctxt _ Fin_Nonmono_Types T =
 is_type_surely_finite ctxt false T
 | should_encode_type _ _ _ _ = false
-fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
+fun should_predicate_on_type ctxt nonmono_Ts (Guards (_, level, heaviness))
 should_predicate_on_var T =
 (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
 should_encode_type ctxt nonmono_Ts level T
 | should_predicate_on_type _ _ _ _ _ = false
 Decl (sym_decl_prefix ^ s, (s, s'),
 (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
 |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
 end
-fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
+fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind nonmono_Ts
 poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
 let
 val (kind, maybe_negate) =
 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
 else (Axiom, I)
 sym_needs_arg_types orelse
 not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)
 val bound_Ts =
 arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
 in
-Formula (preds_sym_formula_prefix ^ s ^
+Formula (guards_sym_formula_prefix ^ s ^
 (if n > 1 then "_" ^ string_of_int j else ""), kind,
 IConst ((s, s'), T, T_args)
 |> fold (curry (IApp o swap)) bounds
 |> type_pred_iterm ctxt format type_enc res_T
 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
 poly_nonmono_Ts type_enc (s, decls) =
 case type_enc of
 Simple_Types _ =>
 decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
-| Preds _ =>
+| Guards _ =>
 let
 val decls =
 case decls of
 decl :: (decls' as _ :: _) =>
 let val T = result_type_of_decl decl in
 decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc
 (K true)
 o result_type_of_decl)
 in
 (0 upto length decls - 1, decls)
-|-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
+|-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind
 nonmono_Ts poly_nonmono_Ts type_enc n s)
 end
 | Tags (_, _, heaviness) =>
 (case heaviness of
 Heavyweight => []

changeset 44860	eb763b3ff9ed
parent 44858	2850b7dc27a4
child 44868	578460971517