--- a/src/Tools/Code/code_haskell.ML Thu Apr 19 18:24:40 2012 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Apr 19 19:18:11 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 18:24:40 2012 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Apr 19 19:18:11 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 18:24:40 2012 +0200
+++ b/src/Tools/Code/code_runtime.ML Thu Apr 19 19:18:11 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 18:24:40 2012 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Apr 19 19:18:11 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/nbe.ML Thu Apr 19 18:24:40 2012 +0200
+++ b/src/Tools/nbe.ML Thu Apr 19 19:18:11 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 18:24:40 2012 +0200
+++ b/src/Tools/quickcheck.ML Thu Apr 19 19:18:11 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