# HG changeset patch # User haftmann # Date 1311629240 -7200 # Node ID 3d204d261903b2591e146a03fc36cb35a84b967c # Parent bb11faa6a79ed5c02f20159ce110858fb72ad0ce# Parent 8adc47768db06070bf6aab1c6dcf500282f39687 merged diff -r 8adc47768db0 -r 3d204d261903 NEWS --- a/NEWS Mon Jul 25 23:26:55 2011 +0200 +++ b/NEWS Mon Jul 25 23:27:20 2011 +0200 @@ -97,7 +97,10 @@ * Code generation: - theory Library/Code_Char_ord provides native ordering of characters in the target language. - + - commands code_module and code_library are legacy, use export_code instead. + - evaluator "SML" and method evaluation are legacy, use evaluator "code" + and method eval instead. + * Declare ext [intro] by default. Rare INCOMPATIBILITY. * Nitpick: @@ -136,6 +139,8 @@ It requires that the Glasgow Haskell compiler is installed and its location is known to Isabelle with the environment variable ISABELLE_GHC. + - Removed quickcheck tester "SML" based on the SML code generator + from HOL-Library * Function package: discontinued option "tailrec". INCOMPATIBILITY. Use partial_function instead. diff -r 8adc47768db0 -r 3d204d261903 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Jul 25 23:26:55 2011 +0200 +++ b/src/HOL/IsaMakefile Mon Jul 25 23:27:20 2011 +0200 @@ -476,7 +476,7 @@ Library/RBT.thy Library/RBT_Impl.thy Library/RBT_Mapping.thy \ Library/README.html \ Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \ - Library/Reflection.thy Library/SML_Quickcheck.thy \ + Library/Reflection.thy \ Library/Sublist_Order.thy Library/Sum_of_Squares.thy \ Library/Sum_of_Squares/sos_wrapper.ML \ Library/Sum_of_Squares/sum_of_squares.ML \ @@ -1062,7 +1062,7 @@ ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \ ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \ - ex/Quickcheck_Narrowing_Examples.thy ex/SML_Quickcheck_Examples.thy \ + ex/Quickcheck_Narrowing_Examples.thy \ ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \ ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \ ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \ diff -r 8adc47768db0 -r 3d204d261903 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon Jul 25 23:26:55 2011 +0200 +++ b/src/HOL/Library/Library.thy Mon Jul 25 23:27:20 2011 +0200 @@ -55,7 +55,6 @@ Reflection RBT_Mapping Set_Algebras - SML_Quickcheck State_Monad Sum_of_Squares Transitive_Closure_Table diff -r 8adc47768db0 -r 3d204d261903 src/HOL/Library/SML_Quickcheck.thy --- a/src/HOL/Library/SML_Quickcheck.thy Mon Jul 25 23:26:55 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ - -header {* Install quickcheck of SML code generator *} - -theory SML_Quickcheck -imports Main -begin - -ML {* -signature SML_QUICKCHECK = -sig - val active : bool Config.T - val setup : theory -> theory -end; - -structure SML_Quickcheck : SML_QUICKCHECK = -struct - -val active = Attrib.setup_config_bool @{binding quickcheck_SML_active} (K true); - -fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] = - let - val prop = list_abs_free (Term.add_frees t [], t) - val test_fun = Codegen.test_term ctxt prop - val iterations = Config.get ctxt Quickcheck.iterations - fun iterate size 0 = NONE - | iterate size j = - let - val result = test_fun size handle Match => - (if Config.get ctxt Quickcheck.quiet then () - else warning "Exception Match raised during quickcheck"; NONE) - in - case result of NONE => iterate size (j - 1) | SOME q => SOME q - end - in (iterate size iterations, NONE) end - -val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr - -val setup = - Inductive_Codegen.quickcheck_setup - #> Context.theory_map (Quickcheck.add_tester ("SML", (active, test_goals))) - -end; -*} - -setup {* SML_Quickcheck.setup *} - -end diff -r 8adc47768db0 -r 3d204d261903 src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Mon Jul 25 23:26:55 2011 +0200 +++ b/src/HOL/Library/reflection.ML Mon Jul 25 23:27:20 2011 +0200 @@ -305,14 +305,15 @@ in rtac th i end); (* Reflection calls reification and uses the correctness *) - (* theorem assumed to be the dead of the list *) + (* theorem assumed to be the head of the list *) fun gen_reflection_tac ctxt conv corr_thms raw_eqs to = SUBGOAL (fn (goal, i) => let val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x) val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst in rtac th i THEN TRY (rtac TrueI i) end); (* FIXME THEN_ALL_NEW !? *) -fun reflection_tac ctxt = gen_reflection_tac ctxt (Codegen.evaluation_conv ctxt); - (*FIXME why Codegen.evaluation_conv? very specific...*) +fun reflection_tac ctxt = gen_reflection_tac ctxt + (Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt)); + (*FIXME why Code_Evaluation.dynamic_conv? very specific...*) end diff -r 8adc47768db0 -r 3d204d261903 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jul 25 23:26:55 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jul 25 23:27:20 2011 +0200 @@ -1155,9 +1155,14 @@ fact_lift (formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply))) +val undefined_name = make_fixed_const @{const_name undefined} +val tvar_a = TVar (("'a", 0), HOLogic.typeS) + val default_sym_tab_entries : (string * sym_info) list = (prefixed_predicator_name, {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) :: + (undefined_name, + {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) :: ([tptp_false, tptp_true] |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @ ([tptp_equal, tptp_old_equal] @@ -1258,7 +1263,8 @@ fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2) | aux arity (IConst (name as (s, _), T, T_args)) = (case strip_prefix_and_unascii const_prefix s of - NONE => (name, T_args) + NONE => + (name, if level_of_type_enc type_enc = No_Types then [] else T_args) | SOME s'' => let val s'' = invert_const s'' @@ -1649,7 +1655,7 @@ fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) = let - fun add_iterm in_conj tm = + fun add_iterm_syms in_conj tm = let val (head, args) = strip_iterm_comb tm in (case head of IConst ((s, s'), T, T_args) => @@ -1661,15 +1667,31 @@ else I end - | IAbs (_, tm) => add_iterm in_conj tm + | IAbs (_, tm) => add_iterm_syms in_conj tm | _ => I) - #> fold (add_iterm in_conj) args + #> fold (add_iterm_syms in_conj) args end - fun add_fact in_conj = fact_lift (formula_fold NONE (K (add_iterm in_conj))) + fun add_fact_syms in_conj = + fact_lift (formula_fold NONE (K (add_iterm_syms in_conj))) + fun add_formula_var_types (AQuant (_, xs, phi)) = + fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs + #> add_formula_var_types phi + | add_formula_var_types (AConn (_, phis)) = + fold add_formula_var_types phis + | add_formula_var_types _ = I + fun var_types () = + if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a] + else fold (fact_lift add_formula_var_types) (conjs @ facts) [] + fun add_undefined_const T = + Symtab.map_default (undefined_name, []) + (insert_type ctxt #3 (@{const_name undefined}, [T], T, false, 0, + false)) in Symtab.empty |> is_type_enc_fairly_sound type_enc - ? (fold (add_fact true) conjs #> fold (add_fact false) facts) + ? (fold (add_fact_syms true) conjs + #> fold (add_fact_syms false) facts + #> fold add_undefined_const (var_types ())) end (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it @@ -1896,7 +1918,7 @@ polymorphism_of_type_enc type_enc <> Polymorphic then nonmono_Ts else - [TVar (("'a", 0), HOLogic.typeS)] + [tvar_a] val sym_decl_lines = (conjs, helpers @ facts) |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab diff -r 8adc47768db0 -r 3d204d261903 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Mon Jul 25 23:26:55 2011 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Mon Jul 25 23:27:20 2011 +0200 @@ -14,7 +14,9 @@ val term_pair_of: indexname * (typ * 'a) -> term * 'a val size_of_subgoals: thm -> int val has_too_many_clauses: Proof.context -> term -> bool - val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context + val make_cnf: + thm list -> thm -> Proof.context + -> Proof.context -> thm list * Proof.context val finish_cnf: thm list -> thm list val unfold_set_const_simps : Proof.context -> thm list val presimplified_consts : Proof.context -> string list @@ -26,8 +28,8 @@ val extensionalize_conv : Proof.context -> conv val extensionalize_theorem : Proof.context -> thm -> thm val is_fol_term: theory -> term -> bool - val make_clauses_unsorted: thm list -> thm list - val make_clauses: thm list -> thm list + val make_clauses_unsorted: Proof.context -> thm list -> thm list + val make_clauses: Proof.context -> thm list -> thm list val make_horns: thm list -> thm list val best_prolog_tac: (thm -> int) -> thm list -> tactic val depth_prolog_tac: thm list -> tactic @@ -366,18 +368,18 @@ (* Conjunctive normal form, adding clauses from th in front of ths (for foldr). Strips universal quantifiers and breaks up conjunctions. Eliminates existential quantifiers using Skolemization theorems. *) -fun cnf old_skolem_ths ctxt (th, ths) = - let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *) +fun cnf old_skolem_ths ctxt ctxt0 (th, ths) = + let val ctxt0r = Unsynchronized.ref ctxt0 (* FIXME ??? *) fun cnf_aux (th,ths) = if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th)) - then nodups ctxt th :: ths (*no work to do, terminate*) + then nodups ctxt0 th :: ths (*no work to do, terminate*) else case head_of (HOLogic.dest_Trueprop (concl_of th)) of Const (@{const_name HOL.conj}, _) => (*conjunction*) cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) | Const (@{const_name All}, _) => (*universal quantifier*) - let val (th',ctxt') = freeze_spec th (!ctxtr) - in ctxtr := ctxt'; cnf_aux (th', ths) end + let val (th',ctxt0') = freeze_spec th (!ctxt0r) + in ctxt0r := ctxt0'; cnf_aux (th', ths) end | Const (@{const_name Ex}, _) => (*existential quantifier: Insert Skolem functions*) cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths) @@ -388,15 +390,17 @@ Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1) in Seq.list_of (tac (th RS disj_forward)) @ ths end - | _ => nodups ctxt th :: ths (*no work to do*) + | _ => nodups ctxt0 th :: ths (*no work to do*) and cnf_nil th = cnf_aux (th,[]) val cls = - if has_too_many_clauses ctxt (concl_of th) - then (trace_msg ctxt (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths) - else cnf_aux (th,ths) - in (cls, !ctxtr) end; - -fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, []) + if has_too_many_clauses ctxt (concl_of th) then + (trace_msg ctxt (fn () => + "cnf is ignoring: " ^ Display.string_of_thm ctxt0 th); ths) + else + cnf_aux (th, ths) + in (cls, !ctxt0r) end +fun make_cnf old_skolem_ths th ctxt ctxt0 = + cnf old_skolem_ths ctxt ctxt0 (th, []) (*Generalization, removal of redundant equalities, removal of tautologies.*) fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths); @@ -657,15 +661,15 @@ Display.string_of_thm ctxt th) | _ => ())) -fun add_clauses th cls = +fun add_clauses ctxt th cls = let val ctxt0 = Variable.global_thm_context th - val (cnfs, ctxt) = make_cnf [] th ctxt0 + val (cnfs, ctxt) = make_cnf [] th ctxt ctxt0 in Variable.export ctxt ctxt0 cnfs @ cls end; (*Make clauses from a list of theorems, previously Skolemized and put into nnf. The resulting clauses are HOL disjunctions.*) -fun make_clauses_unsorted ths = fold_rev add_clauses ths []; -val make_clauses = sort_clauses o make_clauses_unsorted; +fun make_clauses_unsorted ctxt ths = fold_rev (add_clauses ctxt) ths []; +val make_clauses = sort_clauses oo make_clauses_unsorted; (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*) fun make_horns ths = @@ -703,12 +707,13 @@ (** Best-first search versions **) (*ths is a list of additional clauses (HOL disjunctions) to use.*) -fun best_meson_tac sizef = - MESON all_tac make_clauses +fun best_meson_tac sizef ctxt = + MESON all_tac (make_clauses ctxt) (fn cls => THEN_BEST_FIRST (resolve_tac (gocls cls) 1) (has_fewer_prems 1, sizef) - (prolog_step_tac (make_horns cls) 1)); + (prolog_step_tac (make_horns cls) 1)) + ctxt (*First, breaks the goal into independent units*) fun safe_best_meson_tac ctxt = @@ -716,10 +721,10 @@ (** Depth-first search version **) -val depth_meson_tac = - MESON all_tac make_clauses - (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]); - +fun depth_meson_tac ctxt = + MESON all_tac (make_clauses ctxt) + (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]) + ctxt (** Iterative deepening version **) @@ -737,7 +742,7 @@ fun iter_deepen_prolog_tac horns = ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns); -fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac make_clauses +fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt) (fn cls => (case (gocls (cls @ ths)) of [] => no_tac (*no goal clauses*) diff -r 8adc47768db0 -r 3d204d261903 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Mon Jul 25 23:26:55 2011 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Jul 25 23:27:20 2011 +0200 @@ -373,7 +373,7 @@ fun clausify th = make_cnf (if new_skolemizer orelse null choice_ths then [] else map (old_skolem_theorem_from_def thy) (old_skolem_defs th)) - th ctxt + th ctxt ctxt val (cnf_ths, ctxt) = clausify nnf_th fun intr_imp ct th = Thm.instantiate ([], map (pairself (cterm_of thy)) diff -r 8adc47768db0 -r 3d204d261903 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jul 25 23:26:55 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jul 25 23:27:20 2011 +0200 @@ -189,9 +189,9 @@ quote (method_call_for_type_enc fallback_type_syss) ^ "..."); FOL_SOLVE fallback_type_syss ctxt cls ths0) -val neg_clausify = +fun neg_clausify ctxt = single - #> Meson.make_clauses_unsorted + #> Meson.make_clauses_unsorted ctxt #> map Meson_Clausify.introduce_combinators_in_theorem #> Meson.finish_cnf @@ -217,7 +217,7 @@ verbose_warning ctxt "Proof state contains the universal sort {}" else (); - Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0 + Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0 end fun metis_tac [] = generic_metis_tac partial_type_syss @@ -249,9 +249,7 @@ fun setup_method (binding, type_syss) = ((Args.parens (Scan.repeat Parse.short_ident) - >> maps (fn s => case AList.lookup (op =) type_enc_aliases s of - SOME tss => tss - | NONE => [s])) + >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s])) |> Scan.option |> Scan.lift) -- Attrib.thms >> (METHOD oo method type_syss) |> Method.setup binding diff -r 8adc47768db0 -r 3d204d261903 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jul 25 23:26:55 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jul 25 23:27:20 2011 +0200 @@ -63,6 +63,7 @@ val concealedN : string val liftingN : string val combinatorsN : string + val hybridN : string val lambdasN : string val smartN : string val dest_dir : string Config.T @@ -337,6 +338,7 @@ val concealedN = "concealed" val liftingN = "lifting" val combinatorsN = "combinators" +val hybridN = "hybrid" val lambdasN = "lambdas" val smartN = "smart" @@ -525,12 +527,29 @@ | NONE => type_enc_from_string best_type_enc) |> choose_format formats -fun lift_lambdas ctxt = +fun lift_lambdas ctxt type_enc = map (close_form o Envir.eta_contract) #> rpair ctxt - #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix) - Lambda_Lifting.is_quantifier + #-> Lambda_Lifting.lift_lambdas + (if polymorphism_of_type_enc type_enc = Polymorphic then + SOME polymorphic_free_prefix + else + NONE) + Lambda_Lifting.is_quantifier #> fst +fun intentionalize_def (Const (@{const_name All}, _) $ Abs (s, T, t)) = + intentionalize_def t + | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) = + let + fun lam T t = Abs (Name.uu, T, t) + val (head, args) = strip_comb t ||> rev + val head_T = fastype_of head + val n = length args + val arg_Ts = head_T |> binder_types |> take n |> rev + val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1)) + in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end + | intentionalize_def t = t + fun translate_atp_lambdas ctxt type_enc = Config.get ctxt atp_lambda_translation |> (fn trans => @@ -544,11 +563,15 @@ trans) |> (fn trans => if trans = concealedN then - lift_lambdas ctxt ##> K [] + lift_lambdas ctxt type_enc ##> K [] else if trans = liftingN then - lift_lambdas ctxt + lift_lambdas ctxt type_enc else if trans = combinatorsN then map (introduce_combinators ctxt) #> rpair [] + else if trans = hybridN then + lift_lambdas ctxt type_enc + ##> maps (fn t => [t, introduce_combinators ctxt + (intentionalize_def t)]) else if trans = lambdasN then map (Envir.eta_contract) #> rpair [] else diff -r 8adc47768db0 -r 3d204d261903 src/HOL/ex/Meson_Test.thy --- a/src/HOL/ex/Meson_Test.thy Mon Jul 25 23:26:55 2011 +0200 +++ b/src/HOL/ex/Meson_Test.thy Mon Jul 25 23:27:20 2011 +0200 @@ -10,7 +10,7 @@ below and constants declared in HOL! *} -hide_const (open) implies union inter subset sum quotient +hide_const (open) implies union inter subset sum quotient text {* Test data for the MESON proof procedure @@ -31,7 +31,7 @@ apply (tactic {* cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1) *}) ML_val {* val [_, sko25] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal}))); - val clauses25 = Meson.make_clauses [sko25]; (*7 clauses*) + val clauses25 = Meson.make_clauses @{context} [sko25]; (*7 clauses*) val horns25 = Meson.make_horns clauses25; (*16 Horn clauses*) val go25 :: _ = Meson.gocls clauses25; @@ -52,7 +52,7 @@ apply (tactic {* cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1) *}) ML_val {* val [_, sko26] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal}))); - val clauses26 = Meson.make_clauses [sko26]; (*9 clauses*) + val clauses26 = Meson.make_clauses @{context} [sko26]; (*9 clauses*) val horns26 = Meson.make_horns clauses26; (*24 Horn clauses*) val go26 :: _ = Meson.gocls clauses26; @@ -74,7 +74,7 @@ apply (tactic {* cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1) *}) ML_val {* val [_, sko43] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal}))); - val clauses43 = Meson.make_clauses [sko43]; (*6*) + val clauses43 = Meson.make_clauses @{context} [sko43]; (*6*) val horns43 = Meson.make_horns clauses43; (*16*) val go43 :: _ = Meson.gocls clauses43; diff -r 8adc47768db0 -r 3d204d261903 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Mon Jul 25 23:26:55 2011 +0200 +++ b/src/HOL/ex/ROOT.ML Mon Jul 25 23:27:20 2011 +0200 @@ -64,7 +64,6 @@ "HarmonicSeries", "Refute_Examples", "Quickcheck_Examples", - "SML_Quickcheck_Examples", "Quickcheck_Lattice_Examples", "Landau", "Execute_Choice", diff -r 8adc47768db0 -r 3d204d261903 src/HOL/ex/SML_Quickcheck_Examples.thy --- a/src/HOL/ex/SML_Quickcheck_Examples.thy Mon Jul 25 23:26:55 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,143 +0,0 @@ -(* Title: HOL/ex/SML_Quickcheck_Examples.thy - Author: Stefan Berghofer, Lukas Bulwahn - Copyright 2011 TU Muenchen -*) - -theory SML_Quickcheck_Examples -imports "~~/src/HOL/Library/SML_Quickcheck" -begin - -text {* -This is a regression test for the 'quickcheck' counterexample generator based on the -SML code generator. - -The counterexample generator has been superseded by counterexample generators based on -the generic code generator. -*} - -declare [[quickcheck_finite_types = false]] -declare [[quickcheck_timeout = 600.0]] - -subsection {* Lists *} - -theorem "map g (map f xs) = map (g o f) xs" - quickcheck[SML, expect = no_counterexample] - oops - -theorem "map g (map f xs) = map (f o g) xs" - quickcheck[SML, expect = counterexample] - oops - -theorem "rev (xs @ ys) = rev ys @ rev xs" - quickcheck[SML, expect = no_counterexample] - oops - -theorem "rev (xs @ ys) = rev xs @ rev ys" - quickcheck[SML, expect = counterexample] - oops - -theorem "rev (rev xs) = xs" - quickcheck[SML, expect = no_counterexample] - oops - -theorem "rev xs = xs" - quickcheck[tester = SML, expect = counterexample] -oops - - -text {* An example involving functions inside other data structures *} - -primrec app :: "('a \ 'a) list \ 'a \ 'a" where - "app [] x = x" - | "app (f # fs) x = app fs (f x)" - -lemma "app (fs @ gs) x = app gs (app fs x)" - quickcheck[SML, expect = no_counterexample] - by (induct fs arbitrary: x) simp_all - -lemma "app (fs @ gs) x = app fs (app gs x)" - quickcheck[SML, expect = counterexample] - oops - -primrec occurs :: "'a \ 'a list \ nat" where - "occurs a [] = 0" - | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" - -primrec del1 :: "'a \ 'a list \ 'a list" where - "del1 a [] = []" - | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" - -text {* A lemma, you'd think to be true from our experience with delAll *} -lemma "Suc (occurs a (del1 a xs)) = occurs a xs" - -- {* Wrong. Precondition needed.*} - quickcheck[SML, expect = counterexample] - oops - -lemma "xs ~= [] \ Suc (occurs a (del1 a xs)) = occurs a xs" - quickcheck[SML, expect = counterexample] - -- {* Also wrong.*} - oops - -lemma "0 < occurs a xs \ Suc (occurs a (del1 a xs)) = occurs a xs" - quickcheck[SML, expect = no_counterexample] - by (induct xs) auto - -primrec replace :: "'a \ 'a \ 'a list \ 'a list" where - "replace a b [] = []" - | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) - else (x#(replace a b xs)))" - -lemma "occurs a xs = occurs b (replace a b xs)" - quickcheck[SML, expect = counterexample] - -- {* Wrong. Precondition needed.*} - oops - -lemma "occurs b xs = 0 \ a=b \ occurs a xs = occurs b (replace a b xs)" - quickcheck[SML, expect = no_counterexample] - by (induct xs) simp_all - - -subsection {* Trees *} - -datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree" - -primrec leaves :: "'a tree \ 'a list" where - "leaves Twig = []" - | "leaves (Leaf a) = [a]" - | "leaves (Branch l r) = (leaves l) @ (leaves r)" - -primrec plant :: "'a list \ 'a tree" where - "plant [] = Twig " - | "plant (x#xs) = Branch (Leaf x) (plant xs)" - -primrec mirror :: "'a tree \ 'a tree" where - "mirror (Twig) = Twig " - | "mirror (Leaf a) = Leaf a " - | "mirror (Branch l r) = Branch (mirror r) (mirror l)" - -theorem "plant (rev (leaves xt)) = mirror xt" - quickcheck[SML, expect = counterexample] - --{* Wrong! *} - oops - -theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt" - quickcheck[SML, expect = counterexample] - --{* Wrong! *} - oops - -datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree" - -primrec inOrder :: "'a ntree \ 'a list" where - "inOrder (Tip a)= [a]" - | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)" - -primrec root :: "'a ntree \ 'a" where - "root (Tip a) = a" - | "root (Node f x y) = f" - -theorem "hd (inOrder xt) = root xt" - quickcheck[SML, expect = counterexample] - --{* Wrong! *} - oops - -end diff -r 8adc47768db0 -r 3d204d261903 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Mon Jul 25 23:26:55 2011 +0200 +++ b/src/Pure/codegen.ML Mon Jul 25 23:27:20 2011 +0200 @@ -916,6 +916,7 @@ fun eval_term ctxt t = let + val _ = legacy_feature "Old evaluation mechanism -- use evaluator 'code' or method eval instead"; val thy = Proof_Context.theory_of ctxt; val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse error "Term to be evaluated contains type variables"; @@ -1012,6 +1013,7 @@ || Scan.repeat1 (Parse.term >> pair "")) >> (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy => let + val _ = legacy_feature "Old code generation command -- use export_code instead"; val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode); val (code, gr) = generate_code thy mode' modules module xs; val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>