removed legacy 'metisFT' method
authorblanchet
Tue Feb 04 01:35:48 2014 +0100 (2014-02-04)
changeset 5531554b0352fb46d
parent 55314 e0233567a8ef
child 55316 885500f4aa6a
removed legacy 'metisFT' method
NEWS
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
     1.1 --- a/NEWS	Tue Feb 04 01:03:28 2014 +0100
     1.2 +++ b/NEWS	Tue Feb 04 01:35:48 2014 +0100
     1.3 @@ -122,6 +122,10 @@
     1.4        isar_try0 ~> try0_isar
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 +* Metis:
     1.8 +  - Removed legacy proof method 'metisFT'. Use 'metis (full_types)' instead.
     1.9 +    INCOMPATIBILITY.
    1.10 +
    1.11  * Try0: Added 'algebra' and 'meson' to the set of proof methods.
    1.12  
    1.13  * The symbol "\<newline>" may be used within char or string literals
     2.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Feb 04 01:03:28 2014 +0100
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Feb 04 01:35:48 2014 +0100
     2.3 @@ -262,11 +262,9 @@
     2.4  fun generic_metis_tac type_encs lam_trans ctxt ths i st0 =
     2.5    let
     2.6      val _ = trace_msg ctxt (fn () =>
     2.7 -        "Metis called with theorems\n" ^
     2.8 -        cat_lines (map (Display.string_of_thm ctxt) ths))
     2.9 +      "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths))
    2.10      val type_encs = type_encs |> maps unalias_type_enc
    2.11 -    fun tac clause =
    2.12 -      resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1
    2.13 +    fun tac clause = resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1
    2.14    in
    2.15      Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0
    2.16    end
    2.17 @@ -282,15 +280,10 @@
    2.18  val has_tvar =
    2.19    exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
    2.20  
    2.21 -fun method default_type_encs ((override_type_encs, lam_trans), ths) ctxt facts =
    2.22 +fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts =
    2.23    let
    2.24 -    val _ =
    2.25 -      if default_type_encs = full_type_encs then
    2.26 -        legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
    2.27 -      else
    2.28 -        ()
    2.29      val (schem_facts, nonschem_facts) = List.partition has_tvar facts
    2.30 -    val type_encs = override_type_encs |> the_default default_type_encs
    2.31 +    val type_encs = override_type_encs |> the_default partial_type_encs
    2.32      val lam_trans = lam_trans |> the_default default_metis_lam_trans
    2.33    in
    2.34      HEADGOAL (Method.insert_tac nonschem_facts THEN'
    2.35 @@ -301,8 +294,7 @@
    2.36  
    2.37  fun set_opt _ x NONE = SOME x
    2.38    | set_opt get x (SOME x0) =
    2.39 -    error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^
    2.40 -           ".")
    2.41 +    error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^ ".")
    2.42  
    2.43  fun consider_opt s =
    2.44    if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s])
    2.45 @@ -316,15 +308,9 @@
    2.46                             |> (case s' of SOME s' => consider_opt s' | _ => I)))
    2.47        (NONE, NONE)
    2.48  
    2.49 -fun setup_method (binding, type_encs) =
    2.50 -  Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo method type_encs)
    2.51 -  |> Method.setup binding
    2.52 -
    2.53  val setup =
    2.54 -  [((@{binding metis}, partial_type_encs),
    2.55 -    "Metis for FOL and HOL problems"),
    2.56 -   ((@{binding metisFT}, full_type_encs),
    2.57 -    "Metis for FOL/HOL problems with fully-typed translation")]
    2.58 -  |> fold (uncurry setup_method)
    2.59 +  Method.setup @{binding metis}
    2.60 +    (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
    2.61 +    "Metis for FOL and HOL problems"
    2.62  
    2.63  end;
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 01:03:28 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 01:35:48 2014 +0100
     3.3 @@ -94,7 +94,7 @@
     3.4    Method.insert_tac local_facts THEN'
     3.5    (case meth of
     3.6      Metis_Method (type_enc_opt, lam_trans_opt) =>
     3.7 -    Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_typesN]
     3.8 +    Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
     3.9        (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
    3.10    | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
    3.11    | Meson_Method => Meson.meson_tac ctxt global_facts