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

equal deleted inserted replaced

-:e096b1effbbb
+:de026aecab9b
 datatype locality =
 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
 Chained
+datatype order = First_Order | Higher_Order
 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
 datatype type_level =
 All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
 No_Types
 datatype type_heaviness = Heavyweight | Lightweight
 datatype type_sys =
-Simple_Types of type_level |
+Simple_Types of order * type_level |
 Preds of polymorphism * type_level * type_heaviness |
 Tags of polymorphism * type_level * type_heaviness
 val bound_var_prefix : string
 val schematic_var_prefix : string
 fun is_locality_global Local = false
 | is_locality_global Assum = false
 | is_locality_global Chained = false
 | is_locality_global _ = true
+datatype order = First_Order | Higher_Order
 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
 datatype type_level =
 All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
 No_Types
 datatype type_heaviness = Heavyweight | Lightweight
 datatype type_sys =
-Simple_Types of type_level |
+Simple_Types of order * type_level |
 Preds 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
 | NONE =>
 case try (unprefix "mangled_") s of
 SOME s => (SOME Mangled_Monomorphic, s)
 | NONE => (NONE, s))
 ||> (fn s =>
-(* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
+(* "_query" and "_bang" are for the ASCII-challenged Metis and
+Mirabelle. *)
 case try_unsuffixes ["?", "_query"] s of
 SOME s => (Noninf_Nonmono_Types, s)
 | NONE =>
 case try_unsuffixes ["!", "_bang"] s of
 SOME s => (Fin_Nonmono_Types, s)
 case try (unsuffix "_heavy") s of
 SOME s => (Heavyweight, s)
 | NONE => (Lightweight, s))
 |> (fn (poly, (level, (heaviness, core))) =>
 case (core, (poly, level, heaviness)) of
-("simple", (NONE, _, Lightweight)) => Simple_Types level
+("simple", (NONE, _, Lightweight)) =>
+Simple_Types (First_Order, level)
+| ("simple_higher", (NONE, _, Lightweight)) =>
+Simple_Types (Higher_Order, level)
 | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
 | ("tags", (SOME Polymorphic, _, _)) =>
 Tags (Polymorphic, level, heaviness)
 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
 | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
 Preds (Polymorphic, No_Types, Lightweight)
 | _ => raise Same.SAME)
 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
+fun is_type_sys_higher_order (Simple_Types (Higher_Order, _)) = true
+| is_type_sys_higher_order _ = false
 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
 | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
 | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
-fun level_of_type_sys (Simple_Types level) = level
+fun level_of_type_sys (Simple_Types (_, level)) = level
 | level_of_type_sys (Preds (_, level, _)) = level
 | level_of_type_sys (Tags (_, level, _)) = level
 fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
 | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
 fun is_type_level_fairly_sound level =
 is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
-fun is_setting_higher_order THF (Simple_Types _) = true
+fun choose_format formats (Simple_Types (order, level)) =
-| is_setting_higher_order _ _ = false
+if member (op =) formats THF then
+(THF, Simple_Types (order, level))
-fun choose_format formats (Simple_Types level) =
+else if member (op =) formats TFF then
-if member (op =) formats THF then (THF, Simple_Types level)
+(TFF, Simple_Types (First_Order, level))
-else if member (op =) formats TFF then (TFF, Simple_Types level)
+else
-else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
+choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
 | choose_format formats type_sys =
 (case hd formats of
 CNF_UEQ =>
 (CNF_UEQ, case type_sys of
 Preds stuff =>
 val homo_infinite_type = Type (homo_infinite_type_name, [])
 fun fo_term_from_typ format type_sys =
 let
 fun term (Type (s, Ts)) =
-ATerm (case (is_setting_higher_order format type_sys, s) of
+ATerm (case (is_type_sys_higher_order type_sys, s) of
 (true, @{type_name bool}) => `I tptp_bool_type
 | (true, @{type_name fun}) => `I tptp_fun_type
 | _ => if s = homo_infinite_type_name andalso
 (format = TFF orelse format = THF) then
 `I tptp_individual_type
 s = tptp_individual_type then
 s
 else
 simple_type_prefix ^ ascii_of s
-fun ho_type_from_fo_term format type_sys pred_sym ary =
+fun ho_type_from_fo_term type_sys pred_sym ary =
 let
 fun to_atype ty =
 AType ((make_simple_type (generic_mangled_type_name fst ty),
 generic_mangled_type_name snd ty))
 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
 fun to_ho (ty as ATerm ((s, _), tys)) =
 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
-in if is_setting_higher_order format type_sys then to_ho else to_fo ary end
+in if is_type_sys_higher_order type_sys then to_ho else to_fo ary end
 fun mangled_type format type_sys pred_sym ary =
-ho_type_from_fo_term format type_sys pred_sym ary
+ho_type_from_fo_term type_sys pred_sym ary
 o fo_term_from_typ format type_sys
 fun mangled_const_name format type_sys T_args (s, s') =
 let
 val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys)
 fun unmangled_const s =
 let val ss = space_explode mangled_type_sep s in
 (hd ss, map unmangled_type (tl ss))
 end
-fun introduce_proxies format type_sys =
+fun introduce_proxies type_sys =
 let
 fun intro top_level (CombApp (tm1, tm2)) =
 CombApp (intro top_level tm1, intro false tm2)
 | intro top_level (CombConst (name as (s, _), T, T_args)) =
 (case proxify_const s of
 SOME proxy_base =>
-if top_level orelse is_setting_higher_order format type_sys then
+if top_level orelse is_type_sys_higher_order type_sys then
 case (top_level, s) of
 (_, "c_False") => (`I tptp_false, [])
 | (_, "c_True") => (`I tptp_true, [])
 | (false, "c_Not") => (`I tptp_not, [])
 | (false, "c_conj") => (`I tptp_and, [])
 | NONE => (name, T_args))
 |> (fn (name, T_args) => CombConst (name, T, T_args))
 | intro _ tm = tm
 in intro true end
-fun combformula_from_prop thy format type_sys eq_as_iff =
+fun combformula_from_prop thy type_sys eq_as_iff =
 let
 fun do_term bs t atomic_types =
 combterm_from_term thy bs (Envir.eta_contract t)
-|>> (introduce_proxies format type_sys #> AAtom)
+|>> (introduce_proxies type_sys #> AAtom)
 ||> union (op =) atomic_types
 fun do_quant bs q s T t' =
 let val s = singleton (Name.variant_list (map fst bs)) s in
 do_formula ((s, T) :: bs) t'
 #>> mk_aquant q [(`make_bound_var s, SOME T)]
 |> perhaps (try (HOLogic.dest_Trueprop))
 |> introduce_combinators_in_term ctxt kind
 end
 (* making fact and conjecture formulas *)
-fun make_formula thy format type_sys eq_as_iff name loc kind t =
+fun make_formula thy type_sys eq_as_iff name loc kind t =
 let
 val (combformula, atomic_types) =
-combformula_from_prop thy format type_sys eq_as_iff t []
+combformula_from_prop thy type_sys eq_as_iff t []
 in
 {name = name, locality = loc, kind = kind, combformula = combformula,
 atomic_types = atomic_types}
 end
 fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
 ((name, loc), t) =
 let val thy = Proof_Context.theory_of ctxt in
 case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
-|> make_formula thy format type_sys (eq_as_iff andalso format <> CNF)
+|> make_formula thy type_sys (eq_as_iff andalso format <> CNF) name
-name loc Axiom of
+loc Axiom of
 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
 if s = tptp_true then NONE else SOME formula
 | formula => SOME formula
 end
 if prem_kind = Conjecture then update_combformula mk_anot
 else I)
 in
 t |> preproc ?
 (preprocess_prop ctxt presimp_consts kind #> freeze_term)
-|> make_formula thy format type_sys (format <> CNF)
+|> make_formula thy type_sys (format <> CNF) (string_of_int j)
-(string_of_int j) Local kind
+Local kind
 |> maybe_negate
 end)
 (0 upto last) ts
 end
 |> (fn (name, T_args) => CombConst (name, T, T_args))
 | aux _ tm = tm
 in aux 0 end
 fun repair_combterm ctxt format type_sys sym_tab =
-not (is_setting_higher_order format type_sys)
+not (is_type_sys_higher_order type_sys)
 ? (introduce_explicit_apps_in_combterm sym_tab
 #> introduce_predicators_in_combterm sym_tab)
 #> enforce_type_arg_policy_in_combterm ctxt format type_sys
 fun repair_fact ctxt format type_sys sym_tab =
 update_combformula (formula_map
 let
 fun do_term pos =
 term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
 val do_bound_type =
 case type_sys of
-Simple_Types level =>
+Simple_Types (_, level) =>
 homogenized_type ctxt nonmono_Ts level 0
 #> mangled_type format type_sys false 0 #> SOME
 | _ => K NONE
 fun do_out_of_bound_type pos phi universal (name, T) =
 if should_predicate_on_type ctxt nonmono_Ts type_sys
 fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
 (s', T_args, T, pred_sym, ary, _) =
 let
 val (T_arg_Ts, level) =
 case type_sys of
-Simple_Types level => ([], level)
+Simple_Types (_, level) => ([], level)
 | _ => (replicate (length T_args) homo_infinite_type, No_Types)
 in
 Decl (sym_decl_prefix ^ s, (s, s'),
 (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
 |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))

changeset 44491	de026aecab9b
parent 44490	e096b1effbbb
child 44493	a867ebb12209