merged
authorAngeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
Tue Jan 22 21:16:48 2019 +0000 (5 months ago ago)
changeset 69737ce36bed06dee
parent 69736 be6634e99e09
parent 69735 331ef175a112
child 69738 b5163b2132c5
merged
     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 22 21:13:23 2019 +0000
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 22 21:16:48 2019 +0000
     1.3 @@ -32,7 +32,7 @@
     1.4       gen_simp : bool}
     1.5  
     1.6    datatype polymorphism = Monomorphic | Polymorphic
     1.7 -  datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
     1.8 +  datatype thf_choice = THF_Predicate_Free | THF_Without_Choice | THF_With_Choice
     1.9  
    1.10    datatype atp_format =
    1.11      CNF |
    1.12 @@ -188,7 +188,7 @@
    1.13     gen_simp : bool}
    1.14  
    1.15  datatype polymorphism = Monomorphic | Polymorphic
    1.16 -datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
    1.17 +datatype thf_choice = THF_Predicate_Free | THF_Without_Choice | THF_With_Choice
    1.18  
    1.19  datatype atp_format =
    1.20    CNF |
     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 22 21:13:23 2019 +0000
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 22 21:16:48 2019 +0000
     2.3 @@ -162,7 +162,7 @@
     2.4  
     2.5  fun is_type_enc_native (Native _) = true
     2.6    | is_type_enc_native _ = false
     2.7 -fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _)) = false
     2.8 +fun is_type_enc_full_higher_order (Native (Higher_Order THF_Predicate_Free, _, _)) = false
     2.9    | is_type_enc_full_higher_order (Native (Higher_Order _, _, _)) = true
    2.10    | is_type_enc_full_higher_order _ = false
    2.11  fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true
    2.12 @@ -671,8 +671,8 @@
    2.13          | _ => raise Same.SAME))
    2.14    handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
    2.15  
    2.16 -fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free
    2.17 -  | min_hologic _ THF_Lambda_Free = THF_Lambda_Free
    2.18 +fun min_hologic THF_Predicate_Free _ = THF_Predicate_Free
    2.19 +  | min_hologic _ THF_Predicate_Free = THF_Predicate_Free
    2.20    | min_hologic THF_Without_Choice _ = THF_Without_Choice
    2.21    | min_hologic _ THF_Without_Choice = THF_Without_Choice
    2.22    | min_hologic _ _ = THF_With_Choice
    2.23 @@ -2614,7 +2614,7 @@
    2.24        else
    2.25          Sufficient_App_Op_And_Predicator
    2.26      val lam_trans =
    2.27 -      if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN
    2.28 +      if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
    2.29        else lam_trans
    2.30      val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
    2.31        translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts
     3.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 22 21:13:23 2019 +0000
     3.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 22 21:16:48 2019 +0000
     3.3 @@ -354,7 +354,7 @@
     3.4  
     3.5  (* Ehoh *)
     3.6  
     3.7 -val ehoh_thf0 = THF (Monomorphic, THF_Lambda_Free)
     3.8 +val ehoh_thf0 = THF (Monomorphic, THF_Predicate_Free)
     3.9  
    3.10  val ehoh_config : atp_config =
    3.11    {exec = fn _ => (["E_HOME"], ["eprover"]),
    3.12 @@ -443,7 +443,7 @@
    3.13  
    3.14  (* Leo-III *)
    3.15  
    3.16 -(* include choice? Disabled now since its disabled for satallax as well. *)
    3.17 +(* Include choice? Disabled now since it's disabled for Satallax as well. *)
    3.18  val leo3_thf1 = THF (Polymorphic, THF_Without_Choice)
    3.19  
    3.20  val leo3_config : atp_config =
    3.21 @@ -627,7 +627,9 @@
    3.22  val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
    3.23  
    3.24  
    3.25 -(* Zipperposition*)
    3.26 +(* Zipperposition *)
    3.27 +
    3.28 +val zipperposition_thf1 = THF (Polymorphic, THF_Predicate_Free)
    3.29  
    3.30  val zipperposition_config : atp_config =
    3.31    {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
    3.32 @@ -639,7 +641,7 @@
    3.33     prem_role = Hypothesis,
    3.34     best_slices = fn _ =>
    3.35       (* FUDGE *)
    3.36 -     [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))],
    3.37 +     [(1.0, (((100, ""), zipperposition_thf1, "poly_native_higher", keep_lamsN, false), ""))],
    3.38     best_max_mono_iters = default_max_mono_iters,
    3.39     best_max_new_mono_instances = default_max_new_mono_instances}
    3.40  
     4.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jan 22 21:13:23 2019 +0000
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jan 22 21:16:48 2019 +0000
     4.3 @@ -749,6 +749,5 @@
     4.4  end;
     4.5  
     4.6  end;
     4.7 -(* FIXME
     4.8 +
     4.9  structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end;
    4.10 -*)