# HG changeset patch # User nipkow # Date 1334859564 -7200 # Node ID 540a5af9a01c41c899d8493cfdf8977b283ebd35 # Parent bc9c7b5c26fd1572ecbb38666ec66410120c7615# Parent e72e44cee6f2f726ce21e2c53a2b575faf718864 merged diff -r e72e44cee6f2 -r 540a5af9a01c Admin/contributed_components diff -r e72e44cee6f2 -r 540a5af9a01c src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Thu Apr 19 20:19:13 2012 +0200 +++ b/src/HOL/Library/Float.thy Thu Apr 19 20:19:24 2012 +0200 @@ -14,7 +14,7 @@ lemma type_definition_float': "type_definition real float_of float" using type_definition_float unfolding real_of_float_def . -setup_lifting (no_code) type_definition_float' +setup_lifting (no_abs_code) type_definition_float' lemmas float_of_inject[simp] diff -r e72e44cee6f2 -r 540a5af9a01c src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Thu Apr 19 20:19:24 2012 +0200 @@ -119,7 +119,8 @@ val thy = Proof_Context.theory_of ctxt val prob_file = File.tmp_path (Path.explode "prob") val atp = case format of DFG _ => spass_newN | _ => eN - val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp + val {exec, arguments, proof_delims, known_failures, ...} = + get_atp thy atp () val ord = effective_term_order ctxt atp val _ = problem |> lines_for_atp_problem format ord (K []) |> File.write_list prob_file diff -r e72e44cee6f2 -r 540a5af9a01c src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 19 20:19:24 2012 +0200 @@ -60,9 +60,9 @@ val remote_atp : string -> string -> string list -> (string * string) list -> (failure * string) list -> formula_kind -> formula_kind - -> (Proof.context -> slice_spec * string) -> string * atp_config - val add_atp : string * atp_config -> theory -> theory - val get_atp : theory -> string -> atp_config + -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config) + val add_atp : string * (unit -> atp_config) -> theory -> theory + val get_atp : theory -> string -> (unit -> atp_config) val supported_atps : theory -> string list val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit @@ -153,7 +153,7 @@ structure Data = Theory_Data ( - type T = (atp_config * stamp) Symtab.table + type T = ((unit -> atp_config) * stamp) Symtab.table val empty = Symtab.empty val extend = I fun merge data : T = @@ -202,7 +202,7 @@ (* FUDGE *) [(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))]} -val alt_ergo = (alt_ergoN, alt_ergo_config) +val alt_ergo = (alt_ergoN, K alt_ergo_config) (* E *) @@ -318,7 +318,7 @@ [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), heuristic)))] end} -val e = (eN, e_config) +val e = (eN, K e_config) (* LEO-II *) @@ -346,7 +346,7 @@ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} -val leo2 = (leo2N, leo2_config) +val leo2 = (leo2N, K leo2_config) (* Satallax *) @@ -368,7 +368,7 @@ (* FUDGE *) K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]} -val satallax = (satallaxN, satallax_config) +val satallax = (satallaxN, K satallax_config) (* SPASS *) @@ -405,7 +405,7 @@ (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} -val spass_old = (spass_oldN, spass_old_config) +val spass_old = (spass_oldN, K spass_old_config) val spass_new_H1SOS = "-Heuristic=1 -SOS" val spass_new_H2 = "-Heuristic=2" @@ -435,11 +435,11 @@ (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))), (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS)))]} -val spass_new = (spass_newN, spass_new_config) +val spass_new = (spass_newN, K spass_new_config) -fun spass () = - (spassN, if is_new_spass_version () then spass_new_config - else spass_old_config) +val spass = + (spassN, fn () => if is_new_spass_version () then spass_new_config + else spass_old_config) (* Vampire *) @@ -486,7 +486,7 @@ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} -val vampire = (vampireN, vampire_config) +val vampire = (vampireN, K vampire_config) (* Z3 with TPTP syntax *) @@ -509,7 +509,7 @@ (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))), (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))]} -val z3_tptp = (z3_tptpN, z3_tptp_config) +val z3_tptp = (z3_tptpN, K z3_tptp_config) (* Not really a prover: Experimental Polymorphic TFF and THF output *) @@ -529,7 +529,7 @@ val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice) val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher" -val dummy_thf = (dummy_thfN, dummy_thf_config) +val dummy_thf = (dummy_thfN, K dummy_thf_config) (* Remote ATP invocation via SystemOnTPTP *) @@ -595,11 +595,11 @@ fun remote_atp name system_name system_versions proof_delims known_failures conj_sym_kind prem_kind best_slice = (remote_prefix ^ name, - remote_config system_name system_versions proof_delims known_failures - conj_sym_kind prem_kind best_slice) + K (remote_config system_name system_versions proof_delims known_failures + conj_sym_kind prem_kind best_slice)) fun remotify_atp (name, config) system_name system_versions best_slice = (remote_prefix ^ name, - remotify_config system_name system_versions best_slice config) + remotify_config system_name system_versions best_slice o config) val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit) @@ -657,7 +657,7 @@ val supported_atps = Symtab.keys o Data.get fun is_atp_installed thy name = - let val {exec, required_vars, ...} = get_atp thy name in + let val {exec, required_vars, ...} = get_atp thy name () in forall (exists (fn var => getenv var <> "")) (fst exec :: required_vars) end @@ -682,12 +682,12 @@ end end -fun atps () = - [alt_ergo, e, leo2, dummy_thf, satallax, spass_old, spass_new, spass (), +val atps= + [alt_ergo, e, leo2, dummy_thf, satallax, spass_old, spass_new, spass, vampire, z3_tptp, remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark, remote_waldmeister] -fun setup thy = fold add_atp (atps ()) thy +val setup = fold add_atp atps end; diff -r e72e44cee6f2 -r 540a5af9a01c src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 19 20:19:24 2012 +0200 @@ -250,7 +250,20 @@ Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2) end +fun rename_to_tnames ctxt term = + let + fun all_typs (Const ("all", _) $ Abs (_, T, t)) = T :: all_typs t + | all_typs _ = [] + fun rename (Const ("all", T1) $ Abs (_, T2, t)) (new_name :: names) = + (Const ("all", T1) $ Abs (new_name, T2, rename t names)) + | rename t _ = t + + val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt + val new_names = Datatype_Prop.make_tnames (all_typs fixed_def_t) + in + rename term new_names + end fun lift_def_cmd (raw_var, rhs_raw) lthy = let @@ -279,7 +292,8 @@ val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy' val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq) - + val readable_rsp_tm_tnames = rename_to_tnames lthy' readable_rsp_tm + fun after_qed thm_list lthy = let val internal_rsp_thm = @@ -294,7 +308,7 @@ in case maybe_proven_rsp_thm of SOME _ => Proof.theorem NONE after_qed [] lthy' - | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy' + | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm_tnames,[])]] lthy' end fun quot_thm_err ctxt (rty, qty) pretty_msg = diff -r e72e44cee6f2 -r 540a5af9a01c src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Apr 19 20:19:24 2012 +0200 @@ -38,8 +38,8 @@ (def_thm, lthy'') end -fun define_abs_type no_code quot_thm lthy = - if not no_code andalso Lifting_Def.can_generate_code_cert quot_thm then +fun define_abs_type no_abs_code quot_thm lthy = + if not no_abs_code andalso Lifting_Def.can_generate_code_cert quot_thm then let val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep} val add_abstype_attribute = @@ -78,7 +78,7 @@ @ (map Pretty.string_of errs))) end -fun setup_lifting_infr no_code quot_thm lthy = +fun setup_lifting_infr no_abs_code quot_thm lthy = let val _ = quot_thm_sanity_check lthy quot_thm val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm @@ -89,10 +89,10 @@ lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) - |> define_abs_type no_code quot_thm + |> define_abs_type no_abs_code quot_thm end -fun setup_by_quotient no_code quot_thm maybe_reflp_thm lthy = +fun setup_by_quotient no_abs_code quot_thm maybe_reflp_thm lthy = let val transfer_attr = Attrib.internal (K Transfer.transfer_add) val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm @@ -124,10 +124,10 @@ [quot_thm RS @{thm Quotient_right_total}]) |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), [quot_thm RS @{thm Quotient_rel_eq_transfer}]) - |> setup_lifting_infr no_code quot_thm + |> setup_lifting_infr no_abs_code quot_thm end -fun setup_by_typedef_thm no_code typedef_thm lthy = +fun setup_by_typedef_thm no_abs_code typedef_thm lthy = let val transfer_attr = Attrib.internal (K Transfer.transfer_add) val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm @@ -174,10 +174,10 @@ [[quot_thm] MRSL @{thm Quotient_right_unique}]) |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), [[quot_thm] MRSL @{thm Quotient_right_total}]) - |> setup_lifting_infr no_code quot_thm + |> setup_lifting_infr no_abs_code quot_thm end -fun setup_lifting_cmd no_code xthm opt_reflp_xthm lthy = +fun setup_lifting_cmd no_abs_code xthm opt_reflp_xthm lthy = let val input_thm = singleton (Attrib.eval_thms lthy) xthm val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm @@ -200,14 +200,14 @@ val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm val _ = sanity_check_reflp_thm reflp_thm in - setup_by_quotient no_code input_thm (SOME reflp_thm) lthy + setup_by_quotient no_abs_code input_thm (SOME reflp_thm) lthy end - | NONE => setup_by_quotient no_code input_thm NONE lthy + | NONE => setup_by_quotient no_abs_code input_thm NONE lthy fun setup_typedef () = case opt_reflp_xthm of SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used." - | NONE => setup_by_typedef_thm no_code input_thm lthy + | NONE => setup_by_typedef_thm no_abs_code input_thm lthy in case input_term of (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient () @@ -215,12 +215,12 @@ | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." end -val opt_no_code = - Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K true) --| @{keyword ")"})) false +val opt_no_abs_code = + Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_abs_code" >> K true) --| @{keyword ")"})) false val _ = Outer_Syntax.local_theory @{command_spec "setup_lifting"} "Setup lifting infrastructure" - (opt_no_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> - (fn ((no_code, xthm), opt_reflp_xthm) => setup_lifting_cmd no_code xthm opt_reflp_xthm)) + (opt_no_abs_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> + (fn ((no_abs_code, xthm), opt_reflp_xthm) => setup_lifting_cmd no_abs_code xthm opt_reflp_xthm)) end; diff -r e72e44cee6f2 -r 540a5af9a01c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 19 20:19:24 2012 +0200 @@ -146,9 +146,9 @@ fun is_atp_for_format is_format ctxt name = let val thy = Proof_Context.theory_of ctxt in case try (get_atp thy) name of - SOME {best_slices, ...} => + SOME config => exists (fn (_, (_, ((_, format, _, _, _), _))) => is_format format) - (best_slices ctxt) + (#best_slices (config ()) ctxt) | NONE => false end @@ -175,7 +175,7 @@ reconstructor_default_max_relevant else if is_atp thy name then fold (Integer.max o #1 o fst o snd o snd o snd) - (get_slices slice (#best_slices (get_atp thy name) ctxt)) 0 + (get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0 else (* is_smt_prover ctxt name *) SMT_Solver.default_max_relevant ctxt name end @@ -1073,7 +1073,7 @@ fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in if is_reconstructor name then run_reconstructor mode name - else if is_atp thy name then run_atp mode name (get_atp thy name) + else if is_atp thy name then run_atp mode name (get_atp thy name ()) else if is_smt_prover ctxt name then run_smt_solver mode name else error ("No such prover: " ^ name ^ ".") end diff -r e72e44cee6f2 -r 540a5af9a01c src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Thu Apr 19 20:19:13 2012 +0200 +++ b/src/HOL/Transfer.thy Thu Apr 19 20:19:24 2012 +0200 @@ -234,6 +234,9 @@ lemma If_parametric [transfer_rule]: "(op = ===> A ===> A ===> A) If If" unfolding fun_rel_def by simp +lemma Let_parametric [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" + unfolding fun_rel_def by simp + lemma comp_parametric [transfer_rule]: "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \) (op \)" unfolding fun_rel_def by simp diff -r e72e44cee6f2 -r 540a5af9a01c src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Apr 19 20:19:13 2012 +0200 +++ b/src/HOL/Word/Word.thy Thu Apr 19 20:19:24 2012 +0200 @@ -294,7 +294,7 @@ text {* Legacy theorems: *} -lemma word_arith_wis: shows +lemma word_arith_wis [code]: shows word_add_def: "a + b = word_of_int (uint a + uint b)" and word_sub_wi: "a - b = word_of_int (uint a - uint b)" and word_mult_def: "a * b = word_of_int (uint a * uint b)" and @@ -416,7 +416,7 @@ end -lemma shows +lemma [code]: shows word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))" and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" and diff -r e72e44cee6f2 -r 540a5af9a01c src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/Tools/Code/code_haskell.ML Thu Apr 19 20:19:24 2012 +0200 @@ -34,7 +34,7 @@ (** Haskell serializer **) -fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax +fun print_haskell_stmt class_syntax tyco_syntax const_syntax reserved deresolve deriving_show = let fun class_name class = case class_syntax class @@ -52,9 +52,9 @@ (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; fun print_tyco_expr tyvars fxy (tyco, tys) = brackify fxy (str tyco :: map (print_typ tyvars BR) tys) - and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco + and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys) - | SOME (i, print) => print (print_typ tyvars) fxy tys) + | SOME (_, print) => print (print_typ tyvars) fxy tys) | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; fun print_typdecl tyvars (vs, tycoexpr) = Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr); @@ -101,7 +101,7 @@ and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); - fun print_match ((pat, ty), t) vars = + fun print_match ((pat, _), t) vars = vars |> print_bind tyvars some_thm BR pat |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t]) @@ -325,7 +325,7 @@ andalso forall (deriv' tycos) tys | deriv' _ (ITyVar _) = true in deriv [] tyco end; - fun print_stmt deresolve = print_haskell_stmt labelled_name + fun print_stmt deresolve = print_haskell_stmt class_syntax tyco_syntax const_syntax (make_vars reserved) deresolve (if string_classes then deriving_show else K false); diff -r e72e44cee6f2 -r 540a5af9a01c src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/Tools/Code/code_ml.ML Thu Apr 19 20:19:24 2012 +0200 @@ -39,9 +39,6 @@ | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list | ML_Class of string * (vname * ((class * string) list * (string * itype) list)); -fun stmt_name_of_binding (ML_Function (name, _)) = name - | stmt_name_of_binding (ML_Instance (name, _)) = name; - fun print_product _ [] = NONE | print_product print [x] = SOME (print x) | print_product print xs = (SOME o enum " *" "" "") (map print xs); @@ -55,16 +52,16 @@ fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve = let - fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco - | print_tyco_expr fxy (tyco, [ty]) = + fun print_tyco_expr (tyco, []) = (str o deresolve) tyco + | print_tyco_expr (tyco, [ty]) = concat [print_typ BR ty, (str o deresolve) tyco] - | print_tyco_expr fxy (tyco, tys) = + | print_tyco_expr (tyco, tys) = concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco - of NONE => print_tyco_expr fxy (tyco, tys) - | SOME (i, print) => print print_typ fxy tys) + of NONE => print_tyco_expr (tyco, tys) + | SOME (_, print) => print print_typ fxy tys) | print_typ fxy (ITyVar v) = str ("'" ^ v); - fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]); + fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]); fun print_typscheme_prefix (vs, p) = enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); @@ -129,7 +126,7 @@ and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); - fun print_match ((pat, ty), t) vars = + fun print_match ((pat, _), t) vars = vars |> print_bind is_pseudo_fun some_thm NOBR pat |>> (fn p => semicolon [str "val", p, str "=", @@ -170,7 +167,7 @@ in concat ( str definer - :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs) + :: print_tyco_expr (tyco, map (ITyVar o fst) vs) :: str "=" :: separate (str "|") (map print_co cos) ) @@ -236,7 +233,7 @@ (map print_super_instance super_instances @ map print_classparam_instance classparam_instances) :: str ":" - @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs]) + @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs]) )) end; fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair @@ -276,7 +273,7 @@ end | print_stmt (ML_Datas [(tyco, (vs, []))]) = let - val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs); + val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs); in pair [concat [str "type", ty_p]] @@ -359,16 +356,16 @@ fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve = let - fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco - | print_tyco_expr fxy (tyco, [ty]) = + fun print_tyco_expr (tyco, []) = (str o deresolve) tyco + | print_tyco_expr (tyco, [ty]) = concat [print_typ BR ty, (str o deresolve) tyco] - | print_tyco_expr fxy (tyco, tys) = + | print_tyco_expr (tyco, tys) = concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco - of NONE => print_tyco_expr fxy (tyco, tys) + of NONE => print_tyco_expr (tyco, tys) | SOME (_, print) => print print_typ fxy tys) | print_typ fxy (ITyVar v) = str ("'" ^ v); - fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]); + fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]); fun print_typscheme_prefix (vs, p) = enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); @@ -465,7 +462,7 @@ in concat ( str definer - :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs) + :: print_tyco_expr (tyco, map (ITyVar o fst) vs) :: str "=" :: separate (str "|") (map print_co cos) ) @@ -576,7 +573,7 @@ enum_default "()" ";" "{" "}" (map print_super_instance super_instances @ map print_classparam_instance classparam_instances), str ":", - print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs]) + print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs]) ] )) end; @@ -616,7 +613,7 @@ end | print_stmt (ML_Datas [(tyco, (vs, []))]) = let - val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs); + val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs); in pair [concat [str "type", ty_p]] diff -r e72e44cee6f2 -r 540a5af9a01c src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/Tools/Code/code_runtime.ML Thu Apr 19 20:19:24 2012 +0200 @@ -149,7 +149,7 @@ local -fun check_holds thy evaluator vs_t deps ct = +fun check_holds thy evaluator vs_t ct = let val t = Thm.term_of ct; val _ = if fastype_of t <> propT @@ -165,10 +165,10 @@ val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (@{binding holds_by_evaluation}, - fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct))); + fn (thy, evaluator, vs_t, ct) => check_holds thy evaluator vs_t ct))); fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct = - raw_check_holds_oracle (thy, evaluator, (vs_ty, t), deps, ct); + raw_check_holds_oracle (thy, evaluator, (vs_ty, t), ct); in diff -r e72e44cee6f2 -r 540a5af9a01c src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/Tools/Code/code_scala.ML Thu Apr 19 20:19:24 2012 +0200 @@ -24,7 +24,7 @@ (** Scala serializer **) -fun print_scala_stmt labelled_name tyco_syntax const_syntax reserved +fun print_scala_stmt tyco_syntax const_syntax reserved args_num is_singleton_constr (deresolve, deresolve_full) = let fun lookup_tyvar tyvars = lookup_var tyvars o first_upper; @@ -33,7 +33,7 @@ (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr tyvars fxy (tyco, tys) - | SOME (i, print) => print (print_typ tyvars) fxy tys) + | SOME (_, print) => print (print_typ tyvars) fxy tys) | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v; fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]); fun print_tupled_typ tyvars ([], ty) = @@ -362,7 +362,7 @@ fun is_singleton_constr c = case Graph.get_node program c of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c) | _ => false; - fun print_stmt prefix_fragments = print_scala_stmt labelled_name + fun print_stmt prefix_fragments = print_scala_stmt tyco_syntax const_syntax (make_vars reserved_syms) args_num is_singleton_constr (deresolver prefix_fragments, deresolver []); diff -r e72e44cee6f2 -r 540a5af9a01c src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Thu Apr 19 20:19:13 2012 +0200 +++ b/src/Tools/Code_Generator.thy Thu Apr 19 20:19:24 2012 +0200 @@ -20,7 +20,7 @@ "~~/src/Tools/solve_direct.ML" "~~/src/Tools/quickcheck.ML" "~~/src/Tools/value.ML" - "~~/src/Tools/Code/code_preproc.ML" + "~~/src/Tools/Code/code_preproc.ML" "~~/src/Tools/Code/code_thingol.ML" "~~/src/Tools/Code/code_simp.ML" "~~/src/Tools/Code/code_printer.ML" diff -r e72e44cee6f2 -r 540a5af9a01c src/Tools/nbe.ML --- a/src/Tools/nbe.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/Tools/nbe.ML Thu Apr 19 20:19:24 2012 +0200 @@ -119,7 +119,7 @@ in ct |> (Drule.cterm_fun o map_types o map_type_tfree) - (fn (v, sort) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v)) + (fn (v, _) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v)) |> conv |> Thm.strip_shyps |> Thm.varifyT_global @@ -240,7 +240,6 @@ local val prefix = "Nbe."; val name_put = prefix ^ "put_result"; - val name_ref = prefix ^ "univs_ref"; val name_const = prefix ^ "Const"; val name_abss = prefix ^ "abss"; val name_apps = prefix ^ "apps"; diff -r e72e44cee6f2 -r 540a5af9a01c src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Thu Apr 19 20:19:13 2012 +0200 +++ b/src/Tools/quickcheck.ML Thu Apr 19 20:19:24 2012 +0200 @@ -390,24 +390,6 @@ Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u]) (rev eval_terms)))); -fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors, - satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) = - let - fun pretty_stat s i = Pretty.block ([Pretty.str (s ^ ": " ^ string_of_int i)]) - in - ([pretty_stat "iterations" iterations, - pretty_stat "match exceptions" raised_match_errors] - @ map_index - (fn (i, n) => pretty_stat ("satisfied " ^ string_of_int (i + 1) ^ ". assumption") n) - satisfied_assms - @ [pretty_stat "positive conclusion tests" positive_concl_tests]) - end - -fun pretty_timings timings = - Pretty.chunks (Pretty.fbrk :: Pretty.str "timings:" :: - maps (fn (label, time) => - Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings)) - (* Isar commands *) fun read_nat s = case (Library.read_int o Symbol.explode) s