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

equal deleted inserted replaced

-:233f30abb040
+:a7bc1bdb8bb4
 Local | Assum | Chained
 datatype order = First_Order | Higher_Order
 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
 datatype soundness = Sound_Modulo_Infiniteness | Sound
+datatype uniformity = Uniform | Nonuniform
 datatype type_level =
 All_Types |
-Noninf_Nonmono_Types of soundness |
+Noninf_Nonmono_Types of soundness * uniformity |
-Fin_Nonmono_Types |
+Fin_Nonmono_Types of uniformity |
 Const_Arg_Types |
 No_Types
-datatype type_uniformity = Uniform | Nonuniform
 datatype type_enc =
 Simple_Types of order * polymorphism * type_level |
-Guards of polymorphism * type_level * type_uniformity |
+Guards of polymorphism * type_level |
-Tags of polymorphism * type_level * type_uniformity
+Tags of polymorphism * type_level
 val type_tag_idempotence : bool Config.T
 val type_tag_arguments : bool Config.T
 val no_lambdasN : string
 val concealedN : string
 val invert_const : string -> string
 val unproxify_const : string -> string
 val new_skolem_var_name_from_const : string -> string
 val atp_irrelevant_consts : string list
 val atp_schematic_consts_of : term -> typ list Symtab.table
-val type_enc_from_string : soundness -> string -> type_enc
 val is_type_enc_higher_order : type_enc -> bool
 val polymorphism_of_type_enc : type_enc -> polymorphism
 val level_of_type_enc : type_enc -> type_level
 val is_type_enc_quasi_sound : type_enc -> bool
 val is_type_enc_fairly_sound : type_enc -> bool
+val type_enc_from_string : soundness -> string -> type_enc
 val adjust_type_enc : tptp_format -> type_enc -> type_enc
 val mk_aconns :
 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
 val unmangled_const : string -> string * (string, 'b) ho_term list
 val unmangled_const_name : string -> string
 Local | Assum | Chained
 datatype order = First_Order | Higher_Order
 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
 datatype soundness = Sound_Modulo_Infiniteness | Sound
+datatype uniformity = Uniform | Nonuniform
 datatype type_level =
 All_Types |
-Noninf_Nonmono_Types of soundness |
+Noninf_Nonmono_Types of soundness * uniformity |
-Fin_Nonmono_Types |
+Fin_Nonmono_Types of uniformity |
 Const_Arg_Types |
 No_Types
-datatype type_uniformity = Uniform | Nonuniform
 datatype type_enc =
 Simple_Types of order * polymorphism * type_level |
-Guards of polymorphism * type_level * type_uniformity |
+Guards of polymorphism * type_level |
-Tags of polymorphism * type_level * type_uniformity
+Tags of polymorphism * type_level
+fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
+| is_type_enc_higher_order _ = false
+fun polymorphism_of_type_enc (Simple_Types (_, 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 (Guards (_, level)) = level
+| level_of_type_enc (Tags (_, level)) = level
+fun is_level_uniform (Noninf_Nonmono_Types (_, Nonuniform)) = false
+| is_level_uniform (Fin_Nonmono_Types Nonuniform) = false
+| is_level_uniform _ = true
+fun is_type_level_quasi_sound All_Types = true
+| is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
+| is_type_level_quasi_sound _ = false
+val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
+fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
+| is_type_level_fairly_sound level = is_type_level_quasi_sound level
+val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
+fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
+| is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
+| is_type_level_monotonicity_based _ = false
 fun try_unsuffixes ss s =
 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
+val queries = ["?", "_query"]
+val bangs = ["!", "_bang"]
 fun type_enc_from_string soundness s =
 (case try (unprefix "poly_") s of
 SOME s => (SOME Polymorphic, s)
 | NONE =>
 SOME s => (SOME Mangled_Monomorphic, s)
 | NONE => (NONE, s))
 ||> (fn s =>
 (* "_query" and "_bang" are for the ASCII-challenged Metis and
 Mirabelle. *)
-case try_unsuffixes ["?", "_query"] s of
+case try_unsuffixes queries s of
-SOME s => (Noninf_Nonmono_Types soundness, s)
+SOME s =>
+(case try_unsuffixes queries s of
+SOME s => (Noninf_Nonmono_Types (soundness, Nonuniform), s)
+| NONE => (Noninf_Nonmono_Types (soundness, Uniform), s))
 | NONE =>
-case try_unsuffixes ["!", "_bang"] s of
+case try_unsuffixes bangs s of
-SOME s => (Fin_Nonmono_Types, s)
+SOME s =>
+(case try_unsuffixes bangs s of
+SOME s => (Fin_Nonmono_Types Nonuniform, s)
+| NONE => (Fin_Nonmono_Types Uniform, s))
 | NONE => (All_Types, s))
-||> apsnd (fn s =>
+|> (fn (poly, (level, core)) =>
-case try (unsuffix "_uniform") s of
+case (core, (poly, level)) of
-SOME s => (Uniform, s)
+("simple", (SOME poly, _)) =>
-| NONE => (Nonuniform, s))
-|> (fn (poly, (level, (uniformity, core))) =>
-case (core, (poly, level, uniformity)) of
-("simple", (SOME poly, _, Nonuniform)) =>
 (case (poly, level) of
 (Polymorphic, All_Types) =>
 Simple_Types (First_Order, Polymorphic, All_Types)
 | (Mangled_Monomorphic, _) =>
-Simple_Types (First_Order, Mangled_Monomorphic, level)
+if is_level_uniform level then
+Simple_Types (First_Order, Mangled_Monomorphic, level)
+else
+raise Same.SAME
 | _ => raise Same.SAME)
-| ("simple_higher", (SOME poly, _, Nonuniform)) =>
+| ("simple_higher", (SOME poly, _)) =>
 (case (poly, level) of
 (Polymorphic, All_Types) =>
 Simple_Types (Higher_Order, Polymorphic, All_Types)
 | (_, Noninf_Nonmono_Types _) => raise Same.SAME
 | (Mangled_Monomorphic, _) =>
-Simple_Types (Higher_Order, Mangled_Monomorphic, level)
+if is_level_uniform level then
+Simple_Types (Higher_Order, Mangled_Monomorphic, level)
+else
+raise Same.SAME
 | _ => raise Same.SAME)
-| ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
+| ("guards", (SOME poly, _)) => Guards (poly, level)
-| ("tags", (SOME Polymorphic, _, _)) =>
+| ("tags", (SOME Polymorphic, _)) => Tags (Polymorphic, level)
-Tags (Polymorphic, level, uniformity)
+| ("tags", (SOME poly, _)) => Tags (poly, level)
-| ("tags", (SOME poly, _, _)) => Tags (poly, level, uniformity)
+| ("args", (SOME poly, All_Types (* naja *))) =>
-| ("args", (SOME poly, All_Types (* naja *), Nonuniform)) =>
+Guards (poly, Const_Arg_Types)
-Guards (poly, Const_Arg_Types, Nonuniform)
+| ("erased", (NONE, All_Types (* naja *))) =>
-| ("erased", (NONE, All_Types (* naja *), Nonuniform)) =>
+Guards (Polymorphic, No_Types)
-Guards (Polymorphic, No_Types, Nonuniform)
 | _ => 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 (_, 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 (Guards (_, level, _)) = level
-| level_of_type_enc (Tags (_, level, _)) = level
-fun uniformity_of_type_enc (Simple_Types _) = Uniform
-| uniformity_of_type_enc (Guards (_, _, uniformity)) = uniformity
-| uniformity_of_type_enc (Tags (_, _, uniformity)) = uniformity
-fun is_type_level_quasi_sound All_Types = true
-| is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
-| is_type_level_quasi_sound _ = false
-val is_type_enc_quasi_sound =
-is_type_level_quasi_sound o level_of_type_enc
-fun is_type_level_fairly_sound level =
-is_type_level_quasi_sound level orelse level = Fin_Nonmono_Types
-val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
-fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
-| is_type_level_monotonicity_based Fin_Nonmono_Types = true
-| is_type_level_monotonicity_based _ = false
 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
 (Simple_Types (order, _, level)) =
 Simple_Types (order, Mangled_Monomorphic, level)
 | adjust_type_enc (THF _) type_enc = type_enc
 | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
 Simple_Types (First_Order, Mangled_Monomorphic, level)
 | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
 Simple_Types (First_Order, poly, level)
 | adjust_type_enc format (Simple_Types (_, poly, level)) =
-adjust_type_enc format (Guards (poly, level, Uniform))
+adjust_type_enc format (Guards (poly, level))
 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
 (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
 | adjust_type_enc _ type_enc = type_enc
 fun lift_lambdas ctxt type_enc =
 Mangled_Type_Args of bool |
 No_Type_Args
 fun should_drop_arg_type_args (Simple_Types _) = false
 | should_drop_arg_type_args type_enc =
-level_of_type_enc type_enc = All_Types andalso
+level_of_type_enc type_enc = All_Types
-uniformity_of_type_enc type_enc = Uniform
 fun type_arg_policy type_enc s =
 if s = type_tag_name then
 (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
 Mangled_Type_Args
 else
 Explicit_Type_Args) false
 else case type_enc of
-Tags (_, All_Types, Uniform) => No_Type_Args
+Tags (_, All_Types) => No_Type_Args
 | _ =>
 let val level = level_of_type_enc type_enc in
 if level = No_Types orelse s = @{const_name HOL.eq} orelse
 (s = app_op_name andalso level = Const_Arg_Types) then
 No_Type_Args
 models in first-order logic (via Löwenheim-Skolem). *)
 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
 maybe_nonmono_Ts, ...}
-(Noninf_Nonmono_Types soundness) T =
+(Noninf_Nonmono_Types (soundness, _)) T =
 exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
 not (exists (type_instance ctxt T) surely_infinite_Ts orelse
 (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
 is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
 maybe_nonmono_Ts, ...}
-Fin_Nonmono_Types T =
+(Fin_Nonmono_Types _) T =
 exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
 (exists (type_generalization ctxt T) surely_finite_Ts orelse
 (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
 is_type_surely_finite ctxt T))
 | should_encode_type _ _ _ _ = false
-fun should_guard_type ctxt mono (Guards (_, level, uniformity)) should_guard_var
+fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
-T =
+(is_level_uniform level orelse should_guard_var ()) andalso
-(uniformity = Uniform orelse should_guard_var ()) andalso
 should_encode_type ctxt mono level T
 | should_guard_type _ _ _ _ _ = false
 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
 String.isPrefix bound_var_prefix s orelse
 Top_Level of bool option |
 Eq_Arg of bool option |
 Elsewhere
 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
-| should_tag_with_type ctxt mono (Tags (_, level, uniformity)) site u T =
+| should_tag_with_type ctxt mono (Tags (_, level)) site u T =
-(case uniformity of
+(if is_level_uniform level then
-Uniform => should_encode_type ctxt mono level T
+should_encode_type ctxt mono level T
-| Nonuniform =>
+else case (site, is_maybe_universal_var u) of
-case (site, is_maybe_universal_var u) of
+(Eq_Arg _, true) => should_encode_type ctxt mono level T
-(Eq_Arg _, true) => should_encode_type ctxt mono level T
+| _ => false)
-| _ => false)
 | should_tag_with_type _ _ _ _ _ _ = false
 fun fused_type ctxt mono level =
 let
 val should_encode = should_encode_type ctxt mono level
 fun should_guard_var_in_formula pos phi (SOME true) name =
 formula_fold pos (is_var_positively_naked_in_term name) phi false
 | should_guard_var_in_formula _ _ _ _ = true
 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
-| should_generate_tag_bound_decl ctxt mono (Tags (_, level, Nonuniform)) _ T =
+| should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
-should_encode_type ctxt mono level T
+not (is_level_uniform level) andalso should_encode_type ctxt mono level T
 | should_generate_tag_bound_decl _ _ _ _ _ = false
 fun mk_aterm format type_enc name T_args args =
 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
 {maybe_finite_Ts = [@{typ bool}],
 surely_finite_Ts = [@{typ bool}],
 maybe_infinite_Ts = known_infinite_types,
 surely_infinite_Ts =
 case level of
-Noninf_Nonmono_Types Sound => []
+Noninf_Nonmono_Types (Sound, _) => []
 | _ => known_infinite_types,
 maybe_nonmono_Ts = [@{typ bool}]}
 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
 out with monotonicity" paper presented at CADE 2011. *)
 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
 surely_infinite_Ts, maybe_nonmono_Ts}) =
 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
 case level of
-Noninf_Nonmono_Types soundness =>
+Noninf_Nonmono_Types (soundness, _) =>
 if exists (type_instance ctxt T) surely_infinite_Ts orelse
 member (type_aconv ctxt) maybe_finite_Ts T then
 mono
 else if is_type_kind_of_surely_infinite ctxt soundness
 surely_infinite_Ts T then
 {maybe_finite_Ts = maybe_finite_Ts |> insert (type_aconv ctxt) T,
 surely_finite_Ts = surely_finite_Ts,
 maybe_infinite_Ts = maybe_infinite_Ts,
 surely_infinite_Ts = surely_infinite_Ts,
 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
-| Fin_Nonmono_Types =>
+| Fin_Nonmono_Types _ =>
 if exists (type_instance ctxt T) surely_finite_Ts orelse
 member (type_aconv ctxt) maybe_infinite_Ts T then
 mono
 else if is_type_surely_finite ctxt T then
 {maybe_finite_Ts = maybe_finite_Ts,
 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
 (s, decls) =
 case type_enc of
 Simple_Types _ =>
 decls |> map (decl_line_for_sym ctxt format mono type_enc s)
-| Guards (_, level, _) =>
+| Guards (_, level) =>
 let
 val decls =
 case decls of
 decl :: (decls' as _ :: _) =>
 let val T = result_type_of_decl decl in
 in
 (0 upto length decls - 1, decls)
 |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
 type_enc n s)
 end
-| Tags (_, _, uniformity) =>
+| Tags (_, level) =>
-(case uniformity of
+if is_level_uniform level then
-Uniform => []
+[]
-| Nonuniform =>
+else
 let val n = length decls in
 (0 upto n - 1 ~~ decls)
 |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
 conj_sym_kind mono type_enc n s)
-end)
+end
 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
 mono_Ts sym_decl_tab =
 let
 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
 fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
 mono type_enc)
 syms []
 in mono_lines @ decl_lines end
-fun needs_type_tag_idempotence ctxt (Tags (poly, level, uniformity)) =
+fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
 Config.get ctxt type_tag_idempotence andalso
-poly <> Mangled_Monomorphic andalso
+is_type_level_monotonicity_based level andalso
-((level = All_Types andalso uniformity = Nonuniform) orelse
+poly <> Mangled_Monomorphic
-is_type_level_monotonicity_based level)
 | needs_type_tag_idempotence _ _ = false
 fun offset_of_heading_in_problem _ [] j = j
 | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
 if heading = needle then j

changeset 45639	a7bc1bdb8bb4
parent 45618	265174356212
child 45641	3b1b4d805441