1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jul 26 18:11:38 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jul 26 22:53:06 2011 +0200
1.3 @@ -28,7 +28,7 @@
1.4
1.5 datatype type_enc =
1.6 Simple_Types of order * type_level |
1.7 - Preds of polymorphism * type_level * type_heaviness |
1.8 + Guards of polymorphism * type_level * type_heaviness |
1.9 Tags of polymorphism * type_level * type_heaviness
1.10
1.11 val bound_var_prefix : string
1.12 @@ -45,7 +45,7 @@
1.13 val new_skolem_const_prefix : string
1.14 val type_decl_prefix : string
1.15 val sym_decl_prefix : string
1.16 - val preds_sym_formula_prefix : string
1.17 + val guards_sym_formula_prefix : string
1.18 val lightweight_tags_sym_formula_prefix : string
1.19 val fact_prefix : string
1.20 val conjecture_prefix : string
1.21 @@ -133,7 +133,7 @@
1.22
1.23 val type_decl_prefix = "ty_"
1.24 val sym_decl_prefix = "sy_"
1.25 -val preds_sym_formula_prefix = "psy_"
1.26 +val guards_sym_formula_prefix = "gsy_"
1.27 val lightweight_tags_sym_formula_prefix = "tsy_"
1.28 val fact_prefix = "fact_"
1.29 val conjecture_prefix = "conj_"
1.30 @@ -518,7 +518,7 @@
1.31
1.32 datatype type_enc =
1.33 Simple_Types of order * type_level |
1.34 - Preds of polymorphism * type_level * type_heaviness |
1.35 + Guards of polymorphism * type_level * type_heaviness |
1.36 Tags of polymorphism * type_level * type_heaviness
1.37
1.38 fun try_unsuffixes ss s =
1.39 @@ -554,14 +554,14 @@
1.40 | ("simple_higher", (NONE, _, Lightweight)) =>
1.41 if level = Noninf_Nonmono_Types then raise Same.SAME
1.42 else Simple_Types (Higher_Order, level)
1.43 - | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
1.44 + | ("guards", (SOME poly, _, _)) => Guards (poly, level, heaviness)
1.45 | ("tags", (SOME Polymorphic, _, _)) =>
1.46 Tags (Polymorphic, level, heaviness)
1.47 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
1.48 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
1.49 - Preds (poly, Const_Arg_Types, Lightweight)
1.50 + Guards (poly, Const_Arg_Types, Lightweight)
1.51 | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
1.52 - Preds (Polymorphic, No_Types, Lightweight)
1.53 + Guards (Polymorphic, No_Types, Lightweight)
1.54 | _ => raise Same.SAME)
1.55 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
1.56
1.57 @@ -569,15 +569,15 @@
1.58 | is_type_enc_higher_order _ = false
1.59
1.60 fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
1.61 - | polymorphism_of_type_enc (Preds (poly, _, _)) = poly
1.62 + | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
1.63 | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
1.64
1.65 fun level_of_type_enc (Simple_Types (_, level)) = level
1.66 - | level_of_type_enc (Preds (_, level, _)) = level
1.67 + | level_of_type_enc (Guards (_, level, _)) = level
1.68 | level_of_type_enc (Tags (_, level, _)) = level
1.69
1.70 fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
1.71 - | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
1.72 + | heaviness_of_type_enc (Guards (_, _, heaviness)) = heaviness
1.73 | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
1.74
1.75 fun is_type_level_virtually_sound level =
1.76 @@ -595,13 +595,13 @@
1.77 else if member (op =) formats TFF then
1.78 (TFF, Simple_Types (First_Order, level))
1.79 else
1.80 - choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
1.81 + choose_format formats (Guards (Mangled_Monomorphic, level, Heavyweight))
1.82 | choose_format formats type_enc =
1.83 (case hd formats of
1.84 CNF_UEQ =>
1.85 (CNF_UEQ, case type_enc of
1.86 - Preds stuff =>
1.87 - (if is_type_enc_fairly_sound type_enc then Tags else Preds)
1.88 + Guards stuff =>
1.89 + (if is_type_enc_fairly_sound type_enc then Tags else Guards)
1.90 stuff
1.91 | _ => type_enc)
1.92 | format => (format, type_enc))
1.93 @@ -1035,7 +1035,7 @@
1.94 is_type_surely_finite ctxt false T
1.95 | should_encode_type _ _ _ _ = false
1.96
1.97 -fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
1.98 +fun should_predicate_on_type ctxt nonmono_Ts (Guards (_, level, heaviness))
1.99 should_predicate_on_var T =
1.100 (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
1.101 should_encode_type ctxt nonmono_Ts level T
1.102 @@ -1756,7 +1756,7 @@
1.103 |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
1.104 end
1.105
1.106 -fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
1.107 +fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind nonmono_Ts
1.108 poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
1.109 let
1.110 val (kind, maybe_negate) =
1.111 @@ -1775,7 +1775,7 @@
1.112 val bound_Ts =
1.113 arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
1.114 in
1.115 - Formula (preds_sym_formula_prefix ^ s ^
1.116 + Formula (guards_sym_formula_prefix ^ s ^
1.117 (if n > 1 then "_" ^ string_of_int j else ""), kind,
1.118 IConst ((s, s'), T, T_args)
1.119 |> fold (curry (IApp o swap)) bounds
1.120 @@ -1851,7 +1851,7 @@
1.121 case type_enc of
1.122 Simple_Types _ =>
1.123 decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
1.124 - | Preds _ =>
1.125 + | Guards _ =>
1.126 let
1.127 val decls =
1.128 case decls of
1.129 @@ -1871,7 +1871,7 @@
1.130 o result_type_of_decl)
1.131 in
1.132 (0 upto length decls - 1, decls)
1.133 - |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
1.134 + |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind
1.135 nonmono_Ts poly_nonmono_Ts type_enc n s)
1.136 end
1.137 | Tags (_, _, heaviness) =>