--- 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]
--- 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
--- 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;
--- 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 =
--- 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;
--- 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
--- 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 \<circ>) (op \<circ>)"
unfolding fun_rel_def by simp
--- 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
--- 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);
--- 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]]
--- 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
--- 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 []);
--- 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"
--- 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";
--- 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