extended simple types with polymorphism -- the implementation still needs some work though
authorblanchet
Tue Aug 30 16:07:45 2011 +0200 (2011-08-30)
changeset 445910b107d11f634
parent 44590 3a8a31be92d2
child 44592 54906b0337ab
extended simple types with polymorphism -- the implementation still needs some work though
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 30 16:07:45 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 30 16:07:45 2011 +0200
     1.3 @@ -576,7 +576,7 @@
     1.4              relevance_override
     1.5        in
     1.6          if !reconstructor = "sledgehammer_tac" then
     1.7 -          sledge_tac 0.25 ATP_Systems.z3_tptpN "simple"
     1.8 +          sledge_tac 0.25 ATP_Systems.z3_tptpN "mono_simple"
     1.9            ORELSE' sledge_tac 0.25 ATP_Systems.eN "mono_guards?"
    1.10            ORELSE' sledge_tac 0.25 ATP_Systems.spassN "poly_tags_uniform"
    1.11            ORELSE' Metis_Tactics.metis_tac [] ctxt thms
     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:45 2011 +0200
     2.3 @@ -243,8 +243,10 @@
     2.4     prem_kind = Hypothesis,
     2.5     best_slices = fn ctxt =>
     2.6       (* FUDGE *)
     2.7 -     [(0.667, (false, (150, THF0 THF_Without_Choice, "simple_higher", sosN))),
     2.8 -      (0.333, (true, (50, THF0 THF_Without_Choice, "simple_higher", no_sosN)))]
     2.9 +     [(0.667, (false, (150, THF0 THF_Without_Choice,
    2.10 +                       "mono_simple_higher", sosN))),
    2.11 +      (0.333, (true, (50, THF0 THF_Without_Choice,
    2.12 +                      "mono_simple_higher", no_sosN)))]
    2.13       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    2.14           else I)}
    2.15  
    2.16 @@ -264,7 +266,7 @@
    2.17     conj_sym_kind = Axiom,
    2.18     prem_kind = Hypothesis,
    2.19     best_slices =
    2.20 -     K [(1.0, (true, (100, THF0 THF_With_Choice, "simple_higher", "")))]
    2.21 +     K [(1.0, (true, (100, THF0 THF_With_Choice, "mono_simple_higher", "")))]
    2.22       (* FUDGE *)}
    2.23  
    2.24  val satallax = (satallaxN, satallax_config)
    2.25 @@ -346,8 +348,8 @@
    2.26           (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
    2.27        else
    2.28          [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
    2.29 -         (0.333, (false, (500, vampire_tff, "simple", sosN))),
    2.30 -         (0.334, (true, (50, vampire_tff, "simple", no_sosN)))])
    2.31 +         (0.333, (false, (500, vampire_tff, "mono_simple", sosN))),
    2.32 +         (0.334, (true, (50, vampire_tff, "mono_simple", no_sosN)))])
    2.33       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    2.34           else I)}
    2.35  
    2.36 @@ -375,10 +377,10 @@
    2.37     prem_kind = Hypothesis,
    2.38     best_slices =
    2.39       (* FUDGE *)
    2.40 -     K [(0.5, (false, (250, z3_tff, "simple", ""))),
    2.41 -        (0.25, (false, (125, z3_tff, "simple", ""))),
    2.42 -        (0.125, (false, (62, z3_tff, "simple", ""))),
    2.43 -        (0.125, (false, (31, z3_tff, "simple", "")))]}
    2.44 +     K [(0.5, (false, (250, z3_tff, "mono_simple", ""))),
    2.45 +        (0.25, (false, (125, z3_tff, "mono_simple", ""))),
    2.46 +        (0.125, (false, (62, z3_tff, "mono_simple", ""))),
    2.47 +        (0.125, (false, (31, z3_tff, "mono_simple", "")))]}
    2.48  
    2.49  val z3_tptp = (z3_tptpN, z3_tptp_config)
    2.50  
    2.51 @@ -480,25 +482,27 @@
    2.52                 (K (750, FOF, "mono_tags?") (* FUDGE *))
    2.53  val remote_leo2 =
    2.54    remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
    2.55 -               (K (100, THF0 THF_Without_Choice, "simple_higher") (* FUDGE *))
    2.56 +               (K (100, THF0 THF_Without_Choice,
    2.57 +                   "mono_simple_higher") (* FUDGE *))
    2.58  val remote_satallax =
    2.59    remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
    2.60 -               (K (100, THF0 THF_With_Choice, "simple_higher") (* FUDGE *))
    2.61 +               (K (100, THF0 THF_With_Choice,
    2.62 +                   "mono_simple_higher") (* FUDGE *))
    2.63  val remote_vampire =
    2.64    remotify_atp vampire "Vampire" ["1.8"]
    2.65                 (K (250, FOF, "mono_guards?") (* FUDGE *))
    2.66  val remote_z3_tptp =
    2.67 -  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "simple") (* FUDGE *))
    2.68 +  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "mono_simple") (* FUDGE *))
    2.69  val remote_e_sine =
    2.70    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
    2.71               Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
    2.72  val remote_snark =
    2.73    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
    2.74               [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
    2.75 -             (K (100, dumb_tff, "simple") (* FUDGE *))
    2.76 +             (K (100, dumb_tff, "mono_simple") (* FUDGE *))
    2.77  val remote_e_tofof =
    2.78    remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
    2.79 -             Hypothesis (K (150, dumb_tff, "simple") (* FUDGE *))
    2.80 +             Hypothesis (K (150, dumb_tff, "mono_simple") (* FUDGE *))
    2.81  val remote_waldmeister =
    2.82    remote_atp waldmeisterN "Waldmeister" ["710"]
    2.83               [("#START OF PROOF", "Proved Goals:")]
     3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:45 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:45 2011 +0200
     3.3 @@ -31,7 +31,7 @@
     3.4    datatype type_uniformity = Uniform | Nonuniform
     3.5  
     3.6    datatype type_enc =
     3.7 -    Simple_Types of order * type_level |
     3.8 +    Simple_Types of order * polymorphism * type_level |
     3.9      Guards of polymorphism * type_level * type_uniformity |
    3.10      Tags of polymorphism * type_level * type_uniformity
    3.11  
    3.12 @@ -547,7 +547,7 @@
    3.13  datatype type_uniformity = Uniform | Nonuniform
    3.14  
    3.15  datatype type_enc =
    3.16 -  Simple_Types of order * type_level |
    3.17 +  Simple_Types of order * polymorphism * type_level |
    3.18    Guards of polymorphism * type_level * type_uniformity |
    3.19    Tags of polymorphism * type_level * type_uniformity
    3.20  
    3.21 @@ -579,12 +579,15 @@
    3.22                  | NONE => (Nonuniform, s))
    3.23    |> (fn (poly, (level, (uniformity, core))) =>
    3.24           case (core, (poly, level, uniformity)) of
    3.25 -           ("simple", (NONE, _, Nonuniform)) =>
    3.26 -           Simple_Types (First_Order, level)
    3.27 -         | ("simple_higher", (NONE, _, Nonuniform)) =>
    3.28 -           (case level of
    3.29 -              Noninf_Nonmono_Types _ => raise Same.SAME
    3.30 -            | _ => Simple_Types (Higher_Order, level))
    3.31 +           ("simple", (SOME poly, _, Nonuniform)) =>
    3.32 +           (case poly of
    3.33 +              Raw_Monomorphic => raise Same.SAME
    3.34 +            | _ => Simple_Types (First_Order, poly, level))
    3.35 +         | ("simple_higher", (SOME poly, _, Nonuniform)) =>
    3.36 +           (case (poly, level) of
    3.37 +              (Raw_Monomorphic, _) => raise Same.SAME
    3.38 +            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
    3.39 +            | _ => Simple_Types (Higher_Order, poly, level))
    3.40           | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
    3.41           | ("tags", (SOME Polymorphic, _, _)) =>
    3.42             Tags (Polymorphic, level, uniformity)
    3.43 @@ -596,14 +599,14 @@
    3.44           | _ => raise Same.SAME)
    3.45    handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
    3.46  
    3.47 -fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
    3.48 +fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
    3.49    | is_type_enc_higher_order _ = false
    3.50  
    3.51 -fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
    3.52 +fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
    3.53    | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
    3.54    | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
    3.55  
    3.56 -fun level_of_type_enc (Simple_Types (_, level)) = level
    3.57 +fun level_of_type_enc (Simple_Types (_, _, level)) = level
    3.58    | level_of_type_enc (Guards (_, level, _)) = level
    3.59    | level_of_type_enc (Tags (_, level, _)) = level
    3.60  
    3.61 @@ -625,11 +628,15 @@
    3.62    | is_type_level_monotonicity_based Fin_Nonmono_Types = true
    3.63    | is_type_level_monotonicity_based _ = false
    3.64  
    3.65 -fun adjust_type_enc (THF0 _) type_enc = type_enc
    3.66 -  | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
    3.67 -    Simple_Types (First_Order, level)
    3.68 -  | adjust_type_enc format (Simple_Types (_, level)) =
    3.69 -    adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
    3.70 +fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) =
    3.71 +    Simple_Types (order, Mangled_Monomorphic, level)
    3.72 +  | adjust_type_enc (THF0 _) type_enc = type_enc
    3.73 +  | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) =
    3.74 +    Simple_Types (First_Order, Mangled_Monomorphic, level)
    3.75 +  | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) =
    3.76 +    Simple_Types (First_Order, poly, level)
    3.77 +  | adjust_type_enc format (Simple_Types (_, poly, level)) =
    3.78 +    adjust_type_enc format (Guards (poly, level, Uniform))
    3.79    | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
    3.80      (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
    3.81    | adjust_type_enc _ type_enc = type_enc
    3.82 @@ -1662,7 +1669,7 @@
    3.83      val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
    3.84      val do_bound_type =
    3.85        case type_enc of
    3.86 -        Simple_Types (_, level) =>
    3.87 +        Simple_Types (_, _, level) =>
    3.88          homogenized_type ctxt mono level 0
    3.89          #> ho_type_from_typ format type_enc false 0 #> SOME
    3.90        | _ => K NONE
    3.91 @@ -1940,7 +1947,7 @@
    3.92    let
    3.93      val (T_arg_Ts, level) =
    3.94        case type_enc of
    3.95 -        Simple_Types (_, level) => ([], level)
    3.96 +        Simple_Types (_, _, level) => ([], level)
    3.97        | _ => (replicate (length T_args) homo_infinite_type, No_Types)
    3.98    in
    3.99      Decl (sym_decl_prefix ^ s, (s, s'),
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 30 16:07:45 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 30 16:07:45 2011 +0200
     4.3 @@ -148,8 +148,8 @@
     4.4                              | _ => value)
     4.5      | NONE => (name, value)
     4.6  
     4.7 -(* Ensure that type systems such as "simple!" and "mono_guards?" are handled
     4.8 -   correctly. *)
     4.9 +(* Ensure that type systems such as "mono_simple!" and "mono_guards?" are
    4.10 +   handled correctly. *)
    4.11  fun implode_param [s, "?"] = s ^ "?"
    4.12    | implode_param [s, "!"] = s ^ "!"
    4.13    | implode_param ss = space_implode " " ss