# HG changeset patch # User haftmann # Date 1311278184 -7200 # Node ID 3406cd754dd28a783d3a3c867312ae417e4a3ef5 # Parent 78a0a2ad91a387d9f1ab5d09f1a5f42e722c0c46# Parent 481566bc20e43078519660de5212f8843dd8482b merged diff -r 481566bc20e4 -r 3406cd754dd2 src/HOL/Predicate_Compile_Examples/Lambda_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Jul 21 18:40:31 2011 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Jul 21 21:56:24 2011 +0200 @@ -79,7 +79,7 @@ section {* Manual setup to find counterexample *} -setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} +setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *} setup {* Code_Prolog.map_code_options (K { ensure_groundness = true, diff -r 481566bc20e4 -r 3406cd754dd2 src/HOL/Predicate_Compile_Examples/List_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Jul 21 18:40:31 2011 +0200 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Jul 21 21:56:24 2011 +0200 @@ -5,7 +5,7 @@ "~~/src/HOL/Library/Code_Prolog" begin -setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} +setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *} setup {* Code_Prolog.map_code_options (K {ensure_groundness = true, diff -r 481566bc20e4 -r 3406cd754dd2 src/HOL/Predicate_Compile_Examples/ROOT.ML --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Jul 21 18:40:31 2011 +0200 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Jul 21 21:56:24 2011 +0200 @@ -2,11 +2,11 @@ "Examples", "Predicate_Compile_Tests", (* "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *) - "Specialisation_Examples", -(* "Hotel_Example_Small_Generator",*) + "Specialisation_Examples" +(* "Hotel_Example_Small_Generator", "IMP_1", "IMP_2" -(* "IMP_3", + "IMP_3", "IMP_4"*)]; if getenv "ISABELLE_SWIPL" = "" andalso getenv "ISABELLE_YAP" = "" then diff -r 481566bc20e4 -r 3406cd754dd2 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jul 21 18:40:31 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jul 21 21:56:24 2011 +0200 @@ -39,6 +39,7 @@ val const_prefix : string val type_const_prefix : string val class_prefix : string + val polymorphic_free_prefix : string val skolem_const_prefix : string val old_skolem_const_prefix : string val new_skolem_const_prefix : string @@ -125,8 +126,7 @@ val type_const_prefix = "tc_" val class_prefix = "cl_" -(* TODO: Use a more descriptive prefix in "SMT_Translate.lift_lambdas". *) -val lambda_lifted_prefix = Name.uu +val polymorphic_free_prefix = "poly_free" val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko" val old_skolem_const_prefix = skolem_const_prefix ^ "o" @@ -480,7 +480,7 @@ atyps_of T) | iterm_from_term _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, - if String.isPrefix lambda_lifted_prefix s then [T] else []), + if String.isPrefix polymorphic_free_prefix s then [T] else []), atyps_of T) | iterm_from_term _ _ (Var (v as (s, _), T)) = (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then @@ -1417,7 +1417,7 @@ if String.isPrefix skolem_const_prefix s then I else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert) | add (Free (s, T)) = - if String.isPrefix lambda_lifted_prefix s then + if String.isPrefix polymorphic_free_prefix s then T |> fold_type_constrs set_insert else I diff -r 481566bc20e4 -r 3406cd754dd2 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 21 18:40:31 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 21 21:56:24 2011 +0200 @@ -541,7 +541,8 @@ rpair [] o map (conceal_lambdas ctxt) else if trans = liftingN then map (close_form o Envir.eta_contract) #> rpair ctxt - #-> Lambda_Lifting.lift_lambdas NONE Lambda_Lifting.is_quantifier + #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix) + Lambda_Lifting.is_quantifier #> fst else if trans = combinatorsN then rpair [] o map (introduce_combinators ctxt)