# HG changeset patch # User haftmann # Date 1334855891 -7200 # Node ID b3dab1892cda48f67413f0c94e6ab27430014f79 # Parent 572d7e51de4d15f80b5655086149725e4242ff3b dropped dead code diff -r 572d7e51de4d -r b3dab1892cda src/Tools/Code/code_haskell.ML --- 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); diff -r 572d7e51de4d -r b3dab1892cda src/Tools/Code/code_ml.ML --- 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]] diff -r 572d7e51de4d -r b3dab1892cda src/Tools/Code/code_runtime.ML --- 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 diff -r 572d7e51de4d -r b3dab1892cda src/Tools/Code/code_scala.ML --- 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 []); diff -r 572d7e51de4d -r b3dab1892cda src/Tools/nbe.ML --- 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"; diff -r 572d7e51de4d -r b3dab1892cda src/Tools/quickcheck.ML --- 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